Untitled

import random

atoms = ['door_closed', 'door_opening', 'door_open', 'door_closing']

events = ['button_pressed', 'limit_tripped']

states = ['closed', 'opening', 'open', 'closing']


def transition(current_state):
    if current_state == 'closed':
        return 'opening'
    elif current_state == 'opening':
        if random.random() < 0.8:
            return 'closing'
        else:
            return 'open'
    elif current_state == 'open':
        return 'closing'
    elif current_state == 'closing':
        return 'closed'


def labeling(state):
    return state


def get_event(current_state):
    if current_state in ['closed', 'open']:
        return 'button_pressed'
    elif current_state in ['opening', 'closing']:
        return 'limit_tripped'


def hold_properties(state, next_state):
    if state == 'opening' and next_state == 'closing':
        return False
    return True


def simulate(initial_state, num_steps):
    current_state = initial_state
    path = [current_state]

    for step in range(num_steps):
        next_state = transition(current_state)
        if not hold_properties(current_state, next_state):
            print(
                f"Counter-example found at step {step}: {current_state} -> {next_state}"
            )
            return path + [next_state]
        current_state = next_state
        path.append(current_state)

    print("Simulation completed without counter-examples.")
    return path


trace = simulate('closed', 10)
print("Trace:", trace)