\begin{vdm_al}


module SAFER

imports from AUX all,
        from HCM all,
        from TS all,
        from AAH all


exports all

definitions

state SAFER of
  clock      : nat
init s == 
  s = mk_SAFER(0)
end

operations

  ControlCycle: HCM`SwitchPositions * HCM`HandGripPosition * AUX`RotCommand ==> 
                TS`ThrusterSet
  ControlCycle(mk_HCM`SwitchPositions(mode,aah),raw_grip,aah_cmd) ==
    let grip_cmd  = HCM`GripCommand(raw_grip,mode),
        thrusters = TS`SelectedThrusters(grip_cmd,aah_cmd,AAH`ActiveAxes(),
                                         AAH`IgnoreHcm())
    in
       (AAH`Transition(aah,grip_cmd,clock);
        clock := clock + 1;
        return thrusters)
  post card RESULT <= 4 and 
       ThrusterConsistency(RESULT)

functions

  ThrusterConsistency: set of TS`ThrusterName +> bool
  ThrusterConsistency(thrusters) ==
    not ({<B1>,<F1>} subset thrusters) and 
    not ({<B2>,<F2>} subset thrusters) and 
    not ({<B3>,<F3>} subset thrusters) and 
    not ({<B4>,<F4>} subset thrusters) and 
    not (thrusters inter {<L1R>,<L1F>} <> {} and 
    thrusters inter {<R2R>,<R2F>} <> {}) and
    not (thrusters inter {<L3R>,<L3F>} <> {} and 
    thrusters inter {<R4R>,<R4F>} <> {}) and
    not (thrusters inter {<D1R>,<D1F>} <> {} and 
    thrusters inter {<U3R>,<U3F>} <> {}) and
    not (thrusters inter {<D2R>,<D2F>} <> {} and 
    thrusters inter {<U4R>,<U4F>} <> {}) 


end SAFER

\end{vdm_al}