module SMEX5 
title 'Combination-Lock State Machine' 

" Input and output pins 
CLOCK, X                        pin;
Q1..Q3                          pin istype 'reg';
UNLK, HINT                      pin istype 'reg';

" Definitions 
S        = [Q1,Q2,Q3];          " State variables 
ZIP      = [ 0, 0, 0];          " State encodings 
X0       = [ 0, 0, 1]; 
X01      = [ 0, 1, 0]; 
X011     = [ 0, 1, 1]; 
X0110    = [ 1, 0, 0]; 
X01101   = [ 1, 0, 1]; 
X011011  = [ 1, 1, 0]; 
X0110111 = [ 1, 1, 1]; 

state_diagram S

state ZIP:      IF X==0 THEN X0    WITH {UNLK := 0; HINT := 1}
                ELSE ZIP           WITH {UNLK := 0; HINT := 0}
                
state X0:       IF X==0 THEN X0    WITH {UNLK := 0; HINT := 1}
                ELSE X01           WITH {UNLK := 0; HINT := 1}
                
state X01:      IF X==0 THEN X0    WITH {UNLK := 0; HINT := 1}
                ELSE X011          WITH {UNLK := 0; HINT := 0}
                
state X011:     IF X==0 THEN X0110 WITH {UNLK := 0; HINT := 1}
                ELSE ZIP           WITH {UNLK := 0; HINT := 0}
                
state X0110:    IF X==0 THEN X0    WITH {UNLK := 0; HINT := 1}
                ELSE X01101        WITH {UNLK := 0; HINT := 1}
                
state X01101:   IF X==0 THEN X0    WITH {UNLK := 0; HINT := 1}
                ELSE X011011       WITH {UNLK := 0; HINT := 1}
                
state X011011:  IF X==0 THEN X0110 WITH {UNLK := 0; HINT := 1}
                ELSE X0110111      WITH {UNLK := 1; HINT := 0}
                
state X0110111: IF X==0 THEN X0    WITH {UNLK := 0; HINT := 1}
                ELSE ZIP           WITH {UNLK := 0; HINT := 0}

equations
S.CLK = CLOCK; UNLK.CLK = CLOCK; HINT.CLK = CLOCK;

END SMEX5
