interface ITest
{
  in void test();
  out void pass();
  out void fail();
  
  behaviour
  {
    bool is_testing = false;
    
    [!is_testing] on test: is_testing = true;
    [is_testing] on test: illegal;
    
    [is_testing] on inevitable: {is_testing = false; pass;}
    [is_testing] on inevitable: {is_testing = false; fail;}
  }
}

component silent_fail
{
  provides ITest pp;
  requires IConsole rp;
  
  behaviour
  {
    bool is_opening = false;
    bool is_closing = false;
    
    [!is_opening][!is_closing]
    on pp.test(): { rp.Init(); rp.BridgeOpen(); is_opening = true;}
    
    [is_opening]
    {
      on rp.BarDown(): {}
      on rp.BridgeUp(): {is_opening = false; rp.BridgeClose(); is_closing = true;}
    }
    [is_closing]
    {
      on rp.BridgeDown(): {is_closing = false; rp.Term(); pp.pass();}
    }
  }
}

interface IConsole
{
  in void Init();
  in void Term();
  in void BridgeOpen(); // Automatically opens bridge
  in void BridgeClose();// Automatically closes bridge
  
  out void BarUp();
  out void BarDown();
  out void BridgeUp();
  out void BridgeDown();

  behaviour
  {
    enum UpDown {UP,DOWN,UNKNOWN};
    enum LState {ENGAGE,DISENGAGE};
    enum PrevState {UP,DOWN};
    enum SysState {Uninitialized, Automatic};
    
    SysState sys = SysState.Uninitialized;
    
    PrevState prevstate= PrevState.DOWN;
    PrevState prevBarState= PrevState.UP;
    
    UpDown barState = UpDown.UP;
    UpDown bridgeState = UpDown.DOWN;
    LState lockState = LState.ENGAGE;
    
    [sys.Uninitialized]
    {
      on Term:illegal;
      on Init: sys = SysState.Automatic;
      on BridgeOpen,BridgeClose: illegal;
    }
    [sys.Automatic]
    {
      on Init: illegal;
      on Term:
      {
        [!bridgeState.UNKNOWN && !barState.UNKNOWN] { sys = SysState.Uninitialized; }
        [otherwise] illegal;
      }
      [bridgeState.DOWN]
      {
        on BridgeClose:illegal;
        on BridgeOpen: 
        { 
          [barState.UP] barState = UpDown.UNKNOWN;
          [otherwise] illegal;
        }
        [barState.UNKNOWN]
        {
          on inevitable:
          {
            [prevBarState.UP] { BarDown; barState = UpDown.DOWN; prevBarState = PrevState.DOWN; }
            [prevBarState.DOWN] { BarUp; barState = UpDown.UP; prevBarState = PrevState.UP; }
          }
        }
        
        [barState.DOWN]
        {
          [lockState.ENGAGE] on optional: lockState = LState.DISENGAGE;
          [lockState.DISENGAGE] on optional: bridgeState = UpDown.UNKNOWN;
        }
      }
      
      [bridgeState.UP]
      {
        on BridgeClose:
        {
          [barState.DOWN] bridgeState = UpDown.UNKNOWN;
          [otherwise] illegal;
        }
        on BridgeOpen: illegal;
      }
      [bridgeState.UNKNOWN]
      {
        on BridgeClose:illegal;
        on BridgeOpen: illegal;
        on inevitable:
        {
          [prevstate.DOWN] { BridgeUp; prevstate = PrevState.UP; bridgeState = UpDown.UP; }
          [prevstate.UP] { BridgeDown; prevstate = PrevState.DOWN; bridgeState = UpDown.DOWN; }
        }
      }
    } 
  }
}