Stuff

MODULE main
VAR
    event_queue_idle: boolean;
    event_queue_insert: array 0..1 of boolean;
    event_queue_inserted: array 0..1 of boolean;
    event_queue_consume: array 0..1 of boolean;
    event_queue_consumed: array 0..1 of boolean;

    q: event_queue(event_queue_idle, event_queue_insert, event_queue_inserted, event_queue_consume, event_queue_consumed);
    sc_nameless_id324: nameless_id324(event_queue_idle, event_queue_insert, event_queue_inserted, event_queue_consume, event_queue_consumed);
    sc_nameless_id325: nameless_id325(event_queue_idle, event_queue_insert, event_queue_inserted, event_queue_consume, event_queue_consumed);

MODULE nameless_id324(event_queue_idle, event_queue_insert, event_queue_inserted, event_queue_consume, event_queue_consumed)
VAR
    state : {State19_id354, State18_id353, State17_id352, InitialState_id351, insert_event_event2, consume_event_event1};
ASSIGN
    init(state) := InitialState_id351;
    next(state) :=
        case
            state = State18_id353 & event_queue_idle & event_queue_insert[1]: insert_event_event2;
            state = insert_event_event2 & !event_queue_insert[1]: State19_id354;
            state = State17_id352 & event_queue_idle & event_queue_consume[0]: consume_event_event1;
            state = consume_event_event1 & !event_queue_consume[0]: State18_id353;
            state = InitialState_id351 : State17_id352;
            1: state;
        esac;

    next(event_queue_insert[1]) :=
        case
            !event_queue_insert[1] & state = State18_id353: 1;
            event_queue_insert[1] & event_queue_inserted[1]: 0;
            1: event_queue_insert[1];
        esac;

    next(event_queue_consume[0]) :=
        case
            !event_queue_consume[0] & state = State17_id352: 1;
            event_queue_consume[0] & event_queue_consumed[0]: 0;
            1: event_queue_consume[0];
        esac;

MODULE nameless_id325(event_queue_idle, event_queue_insert, event_queue_inserted, event_queue_consume, event_queue_consumed)
VAR
    state : {State22_id363, State21_id362, State20_id361, InitialState_id360, consume_event_event2, insert_event_event1};
ASSIGN
    init(state) := InitialState_id360;
    next(state) :=
        case
            state = State21_id362 & event_queue_idle & event_queue_consume[1]: consume_event_event2;
            state = consume_event_event2 & !event_queue_consume[1]: State22_id363;
            state = State20_id361 & event_queue_idle & event_queue_insert[0]: insert_event_event1;
            state = insert_event_event1 & !event_queue_insert[0]: State21_id362;
            state = InitialState_id360 : State20_id361;
            1: state;
        esac;

    next(event_queue_consume[1]) :=
        case
            !event_queue_consume[1] & state = State21_id362: 1;
            event_queue_consume[1] & event_queue_consumed[1]: 0;
            1: event_queue_consume[1];
        esac;

    next(event_queue_insert[0]) :=
        case
            !event_queue_insert[0] & state = State20_id361: 1;
            event_queue_insert[0] & event_queue_inserted[0]: 0;
            1: event_queue_insert[0];
        esac;

MODULE event_queue(event_queue_idle, event_queue_insert, event_queue_inserted, event_queue_consume, event_queue_consumed)
VAR
    event_queue_events: array 0..1 of 0..5;
ASSIGN
    init(event_queue_idle) := 1;
    init(event_queue_events[0]) := 0;
    init(event_queue_insert[0]) := 0;
    init(event_queue_inserted[0]) := 0;
    init(event_queue_consume[0]) := 0;
    init(event_queue_consumed[0]) := 0;
    init(event_queue_events[1]) := 0;
    init(event_queue_insert[1]) := 0;
    init(event_queue_inserted[1]) := 0;
    init(event_queue_consume[1]) := 0;
    init(event_queue_consumed[1]) := 0;

    next(event_queue_events[0]) :=
        case
            !event_queue_idle & event_queue_insert[0] & event_queue_consume[0]: event_queue_events[0];
            !event_queue_idle & event_queue_events[0] < 5 & event_queue_insert[0]: event_queue_events[0] + 1;
            !event_queue_idle & event_queue_events[0] > 0 & event_queue_consume[0]: event_queue_events[0] - 1;
            1: event_queue_events[0];
        esac;

    next(event_queue_events[1]) :=
        case
            !event_queue_idle & event_queue_insert[1] & event_queue_consume[1]: event_queue_events[1];
            !event_queue_idle & event_queue_events[1] < 5 & event_queue_insert[1]: event_queue_events[1] + 1;
            !event_queue_idle & event_queue_events[1] > 0 & event_queue_consume[1]: event_queue_events[1] - 1;
            1: event_queue_events[1];
        esac;

    next(event_queue_idle) :=
        case
            event_queue_idle & (event_queue_insert[0] | event_queue_insert[1]): 0;
            event_queue_idle & ((event_queue_events[0] = 0 & event_queue_consume[0]) | (event_queue_events[1] = 0 & event_queue_consume[1])): 1;
            event_queue_idle & (event_queue_consume[0] | event_queue_consume[1]): 0;
            !event_queue_idle & !(event_queue_inserted[0] | event_queue_consumed[0] | event_queue_inserted[1] | event_queue_consumed[1]): 1;
            1: event_queue_idle;
        esac;

    next(event_queue_inserted[0]) :=
        case
            !event_queue_idle & event_queue_insert[0]: 1;
            1: 0;
        esac;

    next(event_queue_inserted[1]) :=
        case
            !event_queue_idle & event_queue_insert[1]: 1;
            1: 0;
        esac;

    next(event_queue_consumed[0]) :=
        case
            !event_queue_idle & event_queue_consume[0]: 1;
            1: 0;
        esac;

    next(event_queue_consumed[1]) :=
        case
            !event_queue_idle & event_queue_consume[1]: 1;
            1: 0;
        esac;