statemachine.tla

---------------------------- MODULE statemachine ----------------------------
EXTENDS TLC, Sequences, Integers

(* --algorithm statemachine


fair process webProcess = 1
variables
    machineState = "Starting",
    run = TRUE;
    accessAttemptState = "NULL";
begin P: 
  while run do
  
      Start: 
        if machineState = "Starting" then
            machineState := "LoginScreen";
        else
            skip;       
        end if;        
    
      LoginScreen:
        if machineState = "LoginScreen" then
            machineState := "TotpScreen";
            accessAttemptState := "Undecided";
        else 
            skip;        
        end if;

      TotpScreen:
        if machineState = "TotpScreen" then
            either
               machineState := "LoggedInScreen";
            or
               machineState := "SmsScreen";
               accessAttemptState := "Cancelled";
            end either;
        else
            skip;
        end if;                            
                
    
      SmsScreen:
        if machineState = "SmsScreen" then
            machineState := "LoggedInScreen";       
        else
            skip;
        end if;
    
      LoggedInScreen:
        if machineState = "LoggedInScreen" then
            machineState := "Stop";
        else
            skip;
        end if;                            
    
      Stop:
        if machineState = "Stop" then
                assert accessAttemptState = "Undecided" \/ accessAttemptState = "Cancelled";
                run := FALSE;
        else
            skip;        
        end if;
  end while;
end process;  
end algorithm; *)