module seqdet
Title 'seqdet'

Declarations
"clocks
CLK PIN;

"input ports
RST PIN;
X PIN;

"output ports
Z PIN;

Equations
"diagram ACTIONS
Declarations

"******** SYMBOLIC state machine: Sreg0 ******

Sreg0 STATE_REGISTER;
S0, S1, S2, S3 STATE;

"************* state machine: Sreg0 *************

Equations
" clock signals definitions
    Sreg0.clk = CLK;
State_diagram Sreg0
    ASYNC_RESET S0 : RST;

State S0:
    IF (X&!RST) THEN
    S1 WITH Z=^b0;
    ENDWITH
    ELSE IF (!X#RST) THEN
        S0 WITH Z=^b0;
    ENDWITH;

State S1:
    IF (X&!RST) THEN
        S1 WITH Z=^b0;
    ENDWITH
    ELSE IF (!X&!RST) THEN
        S2 WITH Z=^b0;
    ENDWITH;

State S2:
    IF (X&!RST) THEN
        S3 WITH Z=^b0;
    ENDWITH
    ELSE IF (!X&!RST) THEN
        S0 WITH Z=^b0;
     ENDWITH;

State S3:
    IF (X&!RST) THEN
        S1 WITH Z=^b1;
    ENDWITH
    ELSE IF (!X&!RST) THEN
        S2 WITH Z=^b0;
    ENDWITH;

" end of state machine - Sreg0
end seqdet