Overture Tool
Formal Modelling in VDM
SAFERPP
Author: Sten Agerholm and Peter Gorm Larsen
This specification is a VDM++ model of the SAFER (Simplified Aid for EVA Rescue) example presented in the second volume of the NASA guidebook on formal methods.
Here Appendix C contains a complete listing of the SAFER system using PVS. We have translated this PVS specification rather directly into VDM-SL previously and here that model is again moved to VDM++. In the VDM++ model we have abstracted away form a number of parts which has been left as uninterpreted functions in the PVS model. This has been done because we have defined the purpose of the model to clarify the functionality of the thruster selection logic and the protocol for the automatic attitude hold functionality. Otherwise we have on purpose varied as little as possible from the given PVS model. In order to visualise this example the dynamic link feature is illustrated as well. In the test class Test there are a few examples of using the traces primitives used for test automation.
More explanation about this work can be found in the papers: *Sten Agerholm and Peter Gorm Larsen, Modeling and Validating SAFER in VDM-SL, ed: Michael Holloway, in “Fourth NASA Langley Formal Methods Workshop”, NASA, September 1997. *Sten Agerholm and Wendy Schafer, Analyzing SAFER using UML and VDM++, ed: John Fitzgerald and Peter Gorm Larsen, in “VDM Workshop at the Formal Methods 1999 conference, Toulouse
| Properties | Values |
|---|---|
| Language Version: | vdm10 |
| Entry point : | new Test().BigTest() |
IntegratedCommand.vdmpp
class IntegratedCommand is subclass of SixDOfCommand
instance variables
aah : AAH;
operations
public
SetAAHLink : AAH ==> ()
SetAAHLink(a) ==
aah := a;
public
IntegrateCmds : () ==> ()
IntegrateCmds() ==
if aah.AllAxesOff()
then (if rotcmd.RotCmdsPresent()
then trancmd.SuppressAllAxes()
else trancmd.Prioritize())
else (if rotcmd.RotCmdsPresent()
then (trancmd.SuppressAllAxes();
CombineRotCmds())
else (trancmd.Prioritize();
rotcmd.SetAxesdir(aah.GetRotcmd())));
CombineRotCmds : () ==> ()
CombineRotCmds() ==
let aah_axes =
aah.GetIgnore_hcm() union
{a | a in set Command`allaxes & rotcmd.GetAxesdir()(a) = <Zero>}
in rotcmd.SetAxesdir
({a |-> aah.GetRotcmd()(a) | a in set aah_axes} munion
{a |-> rotcmd.GetAxesdir()(a) | a in set Command`allaxes\aah_axes});
end IntegratedCommand
HandControlUnit.vdmpp
class HandControlUnit
types
public Button = <Up> | <Down>;
public Mode = <Tran> | <Rot>;
instance variables
x : Command`Direction;
pitch : Command`Direction;
yaw_y : Command`Direction;
roll_z : Command`Direction;
aahbutton : Button;
modeswitch : Mode;
operations
public
SetAAH : Button ==> ()
SetAAH(aahbuttonarg) ==
aahbutton := aahbuttonarg;
public
ReadAAH : () ==> Button
ReadAAH() ==
return aahbutton;
public
SetGrip : Command`Direction * Command`Direction * Command`Direction *
Command`Direction ==> ()
SetGrip(xarg, pitcharg, yaw_yarg, roll_zarg) ==
(x := xarg;
pitch := pitcharg;
yaw_y := yaw_yarg;
roll_z := roll_zarg);
public
SetMode : Mode ==> ()
SetMode(m) ==
modeswitch := m;
public
ReadGrip : () ==> Command`Direction * Command`Direction *
Command`Direction * Command`Direction * Mode
ReadGrip() ==
return mk_(x, pitch, yaw_y, roll_z, modeswitch);
end HandControlUnit
Test.vdmpp
class Test is subclass of WorkSpace
values
DirectionSet : set of Command`Direction = {<Neg>, <Pos>, <Zero>};
ModeSet : set of HandControlUnit`Mode = {<Tran>, <Rot>};
AAHButtonSet : set of HandControlUnit`Button = {<Up>, <Down>};
RotCmdSet : set of Command`AxisMap =
{{<axis1> |-> a, <axis2> |-> b, <axis3> |-> c}
| a,b,c in set {<Zero>,<Pos>,<Neg>}}
instance variables
w : WorkSpace := new WorkSpace();
operations
public BigTest: () ==> nat
BigTest() ==
(SetupTopology();
return
(card dom
{mk_(x, pitch, yaw_y, roll_z, modeswitch, <Up>) |->
ControlCycle(x, pitch, yaw_y, roll_z, modeswitch, <Up>,
Command`nullaxesdir)
| x, pitch, yaw_y, roll_z in set DirectionSet,
modeswitch in set ModeSet}));
public HugeTest: () ==> nat
HugeTest() ==
(SetupTopology();
return
(card dom
{mk_(x, pitch, yaw_y, roll_z, modeswitch, aahbutton, aahcmd) |->
ControlCycle(x, pitch, yaw_y, roll_z, modeswitch, aahbutton,
aahcmd)
| x, pitch, yaw_y, roll_z in set DirectionSet,
modeswitch in set ModeSet, aahbutton in set AAHButtonSet,
aahcmd in set RotCmdSet}));
traces
BT : w.SetupTopology(); let x, pitch, yaw_y, roll_z in set DirectionSet in
let modeswitch in set ModeSet in
w.ControlCycle(x, pitch, yaw_y, roll_z, modeswitch, <Up>,
Command`nullaxesdir)
HT: w.SetupTopology();
let x, pitch, yaw_y, roll_z in set DirectionSet in
let modeswitch in set ModeSet in
let aahbutton in set AAHButtonSet in
let aahcmd in set RotCmdSet in
w.ControlCycle(x, pitch, yaw_y, roll_z, modeswitch, aahbutton, aahcmd)
end Test
Command.vdmpp
class Command
types
public
Axis = <axis1> | <axis2> | <axis3>;
public
Direction = <Neg> | <Pos> | <Zero>;
public
AxisMap = map Axis to Direction
inv dir == dom dir = {<axis1>, <axis2>, <axis3>};
values
public allaxes : set of Axis = {<axis1>, <axis2>, <axis3>};
public X = <axis1>;
public Y = <axis2>;
public Z = <axis3>;
public PITCH = <axis1>;
public YAW = <axis2>;
public ROLL = <axis3>;
public nullaxesdir : AxisMap = {a |-> <Zero> | a in set allaxes};
instance variables
protected axesdir : AxisMap := nullaxesdir;
operations
public
GetAxesdir : () ==> AxisMap
GetAxesdir() ==
return axesdir;
public
SetAxesdir : AxisMap ==> ()
SetAxesdir(a) ==
axesdir := a;
public
GetDirection : Axis ==> Direction
GetDirection(a) ==
return axesdir(a);
public
SetDirection : Axis * Direction ==> ()
SetDirection(a, d) ==
axesdir := axesdir ++ {a |-> d};
public
SuppressAllAxes : () ==> ()
SuppressAllAxes() ==
axesdir := nullaxesdir;
end Command
ThrusterSelectionTable.vdmpp
class ThrusterSelectionTable
types
public
ThrSelMap = map (Command`Direction * Command`Direction *
Command`Direction)
to ThrusterControl`ThrSel;
instance variables
selections : ThrSelMap := {|->};
operations
public
Lookup : Command`Direction * Command`Direction * Command`Direction ==>
ThrusterControl`ThrSel
Lookup(dir1, dir2, dir3) ==
return selections(mk_(dir1, dir2, dir3));
public
MakeTable : ThrSelMap ==> ()
MakeTable(m) ==
selections:= m;
end ThrusterSelectionTable
WorkSpace.vdmpp
class WorkSpace
values
check : bool = true;
instance variables
hcu: HandControlUnit := new HandControlUnit();
aah: AAH := new AAH();
intcmd: IntegratedCommand := new IntegratedCommand();
thrcontrol: ThrusterControl := new ThrusterControl();
vda: ValveDriveAssembly := new ValveDriveAssembly();
clock: Clock := new Clock();
operations
public
SetupTopology() ==
(aah.SetHCULink(hcu);
aah.SetSixDOfLink(intcmd);
aah.SetClockLink(clock);
intcmd.SetHCULink(hcu);
intcmd.SetAAHLink(aah);
thrcontrol.SetIntCmdLink(intcmd);
thrcontrol.SetVDALink(vda));
public
ControlCycle : Command`Direction * Command`Direction * Command`Direction *
Command`Direction *
HandControlUnit`Mode * HandControlUnit`Button *
Command`AxisMap ==>
set of ThrusterControl`ThrusterPosition
ControlCycle(x,pitch,yaw_y,roll_z,modeswitch,aahbutton,aahcmd) ==
(clock.IncrTime();
hcu.SetAAH(aahbutton);
hcu.SetGrip(x, pitch, yaw_y, roll_z);
hcu.SetMode(modeswitch);
aah.SetRotcmd(aahcmd);
intcmd.ConvertGrip();
aah.Update();
intcmd.IntegrateCmds();
thrcontrol.SelectThrusters();
thrcontrol.SignalThrusters();
vda.ThrustersOn())
post card RESULT <= 4 and ThrusterConsistency(RESULT);
pure ThrusterConsistency : set of ThrusterControl`ThrusterPosition ==> bool
ThrusterConsistency(thrusters) ==
return
(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 WorkSpace
SixDOfCommand.vdmpp
class SixDOfCommand
instance variables
protected
hcu : HandControlUnit;
protected
rotcmd : RotationCommand := new RotationCommand();
protected
trancmd : TranslationCommand := new TranslationCommand();
operations
public
GetCommand : () ==> Command`AxisMap * Command`AxisMap
GetCommand() ==
return(mk_(trancmd.GetAxesdir(), rotcmd.GetAxesdir()));
public
SetHCULink : HandControlUnit ==> ()
SetHCULink(h) ==
hcu := h;
public
ConvertGrip : () ==> ()
ConvertGrip() ==
let mk_(x, pitch, yaw_y, roll_z, modeswitch) = hcu.ReadGrip(),
tran = {Command`X |-> x,
Command`Y |-> if modeswitch = <Tran>
then yaw_y else <Zero>,
Command`Z |-> if modeswitch = <Tran>
then roll_z else <Zero>},
rot = {Command`ROLL |-> if modeswitch = <Rot>
then roll_z else <Zero>,
Command`PITCH |->pitch,
Command`YAW |-> if modeswitch = <Rot>
then yaw_y else <Zero>}
in (trancmd.SetAxesdir(tran);
rotcmd.SetAxesdir(rot));
-- Alternative formulation of ConvertGrip
-- let mk_(x, pitch, yaw_y, roll_z, modeswitch) = hcu.ReadGrip(),
-- in (trancmd.SuppressAllAxes();
-- rotcmd.SuppressAllAxes();
-- trancmd.SetDirection(Command`X, x);
-- rotcmd.SetDirection(Command`PITCH, pitch);
-- if modeswitch = <Tran>
-- then (trancmd.SetDirection(Command`Y, yaw_y);
-- trancmd.SetDirection(Command`Z, roll_z))
-- else (rotcmd.SetDirection(Command`YAW, yaw_y);
-- rotcmd.SetDirection(Command`ROLL, roll_z)));
end SixDOfCommand
RotationCommand.vdmpp
class RotationCommand is subclass of Command
operations
public
RotCmdsPresent : () ==> bool
RotCmdsPresent() ==
return (exists a in set dom axesdir & axesdir(a) <> <Zero>);
end RotationCommand
ValveDriveAssembly.vdmpp
class ValveDriveAssembly
instance variables
thrusters : map ThrusterControl`ThrusterPosition to Thruster :=
{thr |-> new Thruster() | thr in set ThrusterControl`ThrusterSet};
operations
public
UpdateThrusters : set of ThrusterControl`ThrusterPosition ==> ()
UpdateThrusters(selected) ==
(for all a in set selected
do thrusters(a).SetOn();
for all a in set ThrusterControl`ThrusterSet\selected
do thrusters(a).SetOff());
public
ThrustersOn : () ==> set of ThrusterControl`ThrusterPosition
ThrustersOn() ==
return {thr | thr in set ThrusterControl`ThrusterSet &
thrusters(thr).GetState() = <On>}
end ValveDriveAssembly
ThrusterControl.vdmpp
class ThrusterControl
values -- two thruster selection tables...
bf_thrusters : ThrusterSelectionTable`ThrSelMap = {|->};
bf_thrusters1 : ThrusterSelectionTable`ThrSelMap =
{mk_(<Neg>, <Neg>, <Neg>) |-> mk_ThrSel({<B4>}, {<B2>, <B3>}),
mk_(<Neg>,<Neg>,<Zero>) |-> mk_ThrSel({<B3>,<B4>},{}),
mk_(<Neg>,<Neg>,<Pos>) |-> mk_ThrSel({<B3>},{<B1>,<B4>}),
--
mk_(<Neg>,<Zero>,<Neg>) |-> mk_ThrSel({<B2>,<B4>},{}),
mk_(<Neg>,<Zero>,<Zero>) |-> mk_ThrSel({<B1>,<B4>},{<B2>,<B3>}),
mk_(<Neg>,<Zero>,<Pos>) |-> mk_ThrSel({<B1>,<B3>},{}),
----
mk_(<Neg>,<Pos>,<Neg>) |-> mk_ThrSel({<B2>},{<B1>,<B4>}),
mk_(<Neg>,<Pos>,<Zero>) |-> mk_ThrSel({<B1>,<B2>},{}),
mk_(<Neg>,<Pos>,<Pos>) |-> mk_ThrSel({<B1>},{<B2>,<B3>}),
------
mk_(<Zero>,<Neg>,<Neg>) |-> mk_ThrSel({<B4>,<F1>},{}),
mk_(<Zero>,<Neg>,<Zero>) |-> mk_ThrSel({<B4>,<F2>},{}),
mk_(<Zero>,<Neg>,<Pos>) |-> mk_ThrSel({<B3>,<F2>},{}),
--
mk_(<Zero>,<Zero>,<Neg>) |-> mk_ThrSel({<B2>,<F1>},{}),
mk_(<Zero>,<Zero>,<Zero>) |-> mk_ThrSel({},{}),
mk_(<Zero>,<Zero>,<Pos>) |-> mk_ThrSel({<B3>,<F4>},{}),
----
mk_(<Zero>,<Pos>,<Neg>) |-> mk_ThrSel({<B2>,<F3>},{}),
mk_(<Zero>,<Pos>,<Zero>) |-> mk_ThrSel({<B1>,<F3>},{}),
mk_(<Zero>,<Pos>,<Pos>) |-> mk_ThrSel({<B1>,<F4>},{}),
------
mk_(<Pos>,<Neg>,<Neg>) |-> mk_ThrSel({<F1>},{<F2>,<F3>}),
mk_(<Pos>,<Neg>,<Zero>) |-> mk_ThrSel({<F1>,<F2>},{}),
mk_(<Pos>,<Neg>,<Pos>) |-> mk_ThrSel({<F2>},{<F1>,<F4>}),
--
mk_(<Pos>,<Zero>,<Neg>) |-> mk_ThrSel({<F1>,<F3>},{}),
mk_(<Pos>,<Zero>,<Zero>) |-> mk_ThrSel({<F2>,<F3>},{<F1>,<F4>}),
mk_(<Pos>,<Zero>,<Pos>) |-> mk_ThrSel({<F2>,<F4>},{}),
----
mk_(<Pos>,<Pos>,<Neg>) |-> mk_ThrSel({<F3>},{<F1>,<F4>}),
mk_(<Pos>,<Pos>,<Zero>) |-> mk_ThrSel({<F3>,<F4>},{}),
mk_(<Pos>,<Pos>,<Pos>) |-> mk_ThrSel({<F4>},{<F2>,<F3>})};
lrud_thrusters : ThrusterSelectionTable`ThrSelMap = {|->};
lrud_thrusters1 : ThrusterSelectionTable`ThrSelMap =
{mk_(<Neg>,<Neg>,<Neg>) |-> mk_ThrSel({},{}),
mk_(<Neg>,<Neg>,<Zero>) |-> mk_ThrSel({},{}),
mk_(<Neg>,<Neg>,<Pos>) |-> mk_ThrSel({},{}),
--
mk_(<Neg>,<Zero>,<Neg>) |-> mk_ThrSel({<L1R>},{<L1F>,<L3F>}),
mk_(<Neg>,<Zero>,<Zero>) |-> mk_ThrSel({<L1R>,<L3R>},{<L1F>,<L3F>}),
mk_(<Neg>,<Zero>,<Pos>) |-> mk_ThrSel({<L3R>},{<L1F>,<L3F>}),
----
mk_(<Neg>,<Pos>,<Neg>) |-> mk_ThrSel({},{}),
mk_(<Neg>,<Pos>,<Zero>) |-> mk_ThrSel({},{}),
mk_(<Neg>,<Pos>,<Pos>) |-> mk_ThrSel({},{}),
------
mk_(<Zero>,<Neg>,<Neg>) |-> mk_ThrSel({<U3R>},{<U3F>,<U4F>}),
mk_(<Zero>,<Neg>,<Zero>) |-> mk_ThrSel({<U3R>,<U4R>},{<U3F>,<U4F>}),
mk_(<Zero>,<Neg>,<Pos>) |-> mk_ThrSel({<U4R>},{<U3F>,<U4F>}),
--
mk_(<Zero>,<Zero>,<Neg>) |-> mk_ThrSel({<L1R>,<R4R>},{}),
mk_(<Zero>,<Zero>,<Zero>) |-> mk_ThrSel({},{}),
mk_(<Zero>,<Zero>,<Pos>) |-> mk_ThrSel({<R2R>,<L3R>},{}),
----
mk_(<Zero>,<Pos>,<Neg>) |-> mk_ThrSel({<D2R>},{<D1F>,<D2F>}),
mk_(<Zero>,<Pos>,<Zero>) |-> mk_ThrSel({<D1R>,<D2R>},{<D1F>,<D2F>}),
mk_(<Zero>,<Pos>,<Pos>) |-> mk_ThrSel({<D1R>},{<D1F>,<D2F>}),
------
mk_(<Pos>,<Neg>,<Neg>) |-> mk_ThrSel({},{}),
mk_(<Pos>,<Neg>,<Zero>) |-> mk_ThrSel({},{}),
mk_(<Pos>,<Neg>,<Pos>) |-> mk_ThrSel({},{}),
--
mk_(<Pos>,<Zero>,<Neg>) |-> mk_ThrSel({<R4R>},{<R2F>,<R4F>}),
mk_(<Pos>,<Zero>,<Zero>) |-> mk_ThrSel({<R2R>,<R4R>},{<R2F>,<R4F>}),
mk_(<Pos>,<Zero>,<Pos>) |-> mk_ThrSel({<R2R>},{<R2F>,<R4F>}),
----
mk_(<Pos>,<Pos>,<Neg>) |-> mk_ThrSel({},{}),
mk_(<Pos>,<Pos>,<Zero>) |-> mk_ThrSel({},{}),
mk_(<Pos>,<Pos>,<Pos>) |-> mk_ThrSel({},{})};
public ThrusterSet : set of ThrusterPosition =
{<B1>, <B2>, <B3>, <B4>, <F1>, <F2>, <F3>, <F4>, <L1R>, <L1F>, <R2R>,
<R2F>, <L3R>, <L3F>, <R4R>, <R4F>, <D1R>, <D1F>, <D2R>, <D2F>, <U3R>,
<U3F>, <U4R>, <U4F>};
types
public
ThrusterPosition = <B1> | <B2> | <B3> | <B4> | <F1> | <F2> | <F3> | <F4> |
<L1R>| <L1F>| <R2R>| <R2F>| <L3R>| <L3F>| <R4R>| <R4F>|
<D1R>| <D1F>| <D2R>| <D2F>| <U3R>| <U3F>| <U4R>| <U4F>;
public
ThrSel :: always_on : set of ThrusterPosition
optional : set of ThrusterPosition;
instance variables
vda : ValveDriveAssembly;
intcmd : IntegratedCommand;
selected : set of ThrusterPosition := {};
tslogic1 : ThrusterSelectionTable := InitTable(bf_thrusters1);
tslogic2 : ThrusterSelectionTable := InitTable(lrud_thrusters1);
-- tslogic1 : ThrusterSelectionTable := new ThrusterSelectionTable();
-- tslogic2 : ThrusterSelectionTable := new ThrusterSelectionTable();
operations
public
InitTable : ThrusterSelectionTable`ThrSelMap ==>
ThrusterSelectionTable
InitTable(table) ==
(dcl tmp:ThrusterSelectionTable := new ThrusterSelectionTable();
tmp.MakeTable(table); return tmp);
PrintSelected : () ==> set of ThrusterPosition
PrintSelected() ==
return selected;
public
SetIntCmdLink : IntegratedCommand ==> ()
SetIntCmdLink(i) ==
intcmd := i;
public
SetVDALink : ValveDriveAssembly ==> ()
SetVDALink(v) ==
vda := v;
public
SelectThrusters : () ==> ()
SelectThrusters() ==
let mk_(tran, rot) = intcmd.GetCommand(),
lookup1 = tslogic1.Lookup(tran(Command`X), rot(Command`PITCH),
rot(Command`YAW)),
lookup2 = tslogic2.Lookup(tran(Command`Y), tran(Command`Z),
rot(Command`ROLL)),
bf_thr = if rot(Command`ROLL) = <Zero>
then lookup1.always_on union lookup1.optional
else lookup1.always_on,
lrud_thr = if rot(Command`PITCH) = <Zero> and
rot(Command`YAW) = <Zero>
then lookup2.optional union lookup2.always_on
else lookup2.always_on
in selected := bf_thr union lrud_thr;
public
SignalThrusters : () ==> ()
SignalThrusters() ==
vda.UpdateThrusters(selected);
InitializeTables : () ==> ()
InitializeTables() ==
(tslogic1.MakeTable(bf_thrusters);
tslogic2.MakeTable(lrud_thrusters));
end ThrusterControl
AAH.vdmpp
class AAH
types
public
EngageState = <AAH_off> | <AAH_started> | <AAH_on> | <pressed_once> |
<AAH_closing> | <pressed_twice>;
values
click_timeout : nat = 10;
instance variables
hcu : HandControlUnit;
clock : Clock;
rotcmd : RotationCommand := new RotationCommand();
toggle : EngageState := <AAH_off>;
gripcmd : SixDOfCommand;
timeout : nat := 0;
ignore_hcm_rot : set of Command`Axis := {};
active_rot_axes : set of Command`Axis := {};
operations
public
Update : () ==> ()
Update() ==
let engage = ButtonTransition(hcu.ReadAAH(), clock.ReadTime()),
starting = (toggle = <AAH_off>) and (engage = <AAH_started>),
mk_(-, rot) = gripcmd.GetCommand()
in (active_rot_axes := {a | a in set Command`allaxes & starting or
(engage <> <AAH_off> and
a in set active_rot_axes and
(rot(a) = <Zero> or
a in set ignore_hcm_rot))};
ignore_hcm_rot := {a | a in set Command`allaxes &
(starting and rot(a) <> <Zero>) or
(not starting and a in set ignore_hcm_rot)};
timeout := if toggle = <AAH_on> and engage = <pressed_once>
then clock.ReadTime() + click_timeout
else timeout;
toggle := engage);
public
GetRotcmd : () ==> Command`AxisMap
GetRotcmd() ==
return rotcmd.GetAxesdir();
public
SetRotcmd : Command`AxisMap ==> ()
SetRotcmd(m) ==
rotcmd.SetAxesdir(m);
public
AllAxesOff : () ==> bool
AllAxesOff() ==
return (active_rot_axes = {});
public
SetHCULink : HandControlUnit ==> ()
SetHCULink(h) ==
hcu := h;
public
SetClockLink : Clock ==> ()
SetClockLink(c) ==
clock := c;
public
GetIgnore_hcm : () ==> set of Command`Axis
GetIgnore_hcm() ==
return ignore_hcm_rot;
public
SetSixDOfLink : SixDOfCommand ==> ()
SetSixDOfLink(s) ==
gripcmd := s;
public
GetActive_axes : () ==> set of Command`Axis
GetActive_axes() ==
return active_rot_axes;
ButtonTransition : HandControlUnit`Button * nat ==> EngageState
ButtonTransition(button_pos, count) ==
return
(cases mk_(toggle,button_pos) :
mk_(<AAH_off>,<Up>) -> <AAH_off>,
mk_(<AAH_off>,<Down>) -> <AAH_started>,
mk_(<AAH_started>,<Up>) -> <AAH_on>,
mk_(<AAH_started>,<Down>) -> <AAH_started>,
mk_(<AAH_on>,<Up>) -> if AllAxesOff()
then <AAH_off>
else <AAH_on>,
mk_(<AAH_on>,<Down>) -> <pressed_once>,
mk_(<pressed_once>,<Up>) -> <AAH_closing>,
mk_(<pressed_once>,<Down>) -> <pressed_once>,
mk_(<AAH_closing>,<Up>) -> if AllAxesOff()
then <AAH_off>
elseif count > timeout
then <AAH_on>
else <AAH_closing>,
mk_(<AAH_closing>,<Down>) -> <pressed_twice>,
mk_(<pressed_twice>,<Up>) -> <AAH_off>,
mk_(<pressed_twice>,<Down>) -> <pressed_twice>
end);
end AAH
Thruster.vdmpp
class Thruster
types
public On_Off = <On> | <Off>;
instance variables
state : On_Off := <Off>;
operations
public
SetOn : () ==> ()
SetOn() ==
state := <On>;
public
SetOff : () ==> ()
SetOff() ==
state := <Off>;
public
GetState : () ==> On_Off
GetState() ==
return state;
end Thruster
TranslationCommand.vdmpp
class TranslationCommand is subclass of Command
operations
public
Prioritize : () ==> ()
Prioritize() ==
axesdir := if axesdir(X) <> <Zero>
then axesdir ++ {Y |-> <Zero>, Z |-> <Zero>}
elseif axesdir(Y) <> <Zero>
then axesdir ++ {Z |-> <Zero>}
else axesdir;
end TranslationCommand
Interface.vdmpp
class Interface
instance variables
ws : WorkSpace := new WorkSpace()
types
public
Input = seq of nat
inv inp == len inp = 9;
public
ThrusterMatrix = seq of seq of bool
inv tm == len tm = 4 and forall i in set inds tm & len tm(i) = 6
operations
public
SetupTopology: () ==> ()
SetupTopology () ==
ws.SetupTopology();
public
RunControlCycle: Input ==> ThrusterMatrix
RunControlCycle (inp) ==
let mk_(x,p,y,z,m,ab,ah) = TransformInput (inp) in
let ts = ws.ControlCycle (x,p,y,z,m,ab,ah) in
return GenerateThrusterMatrix (ts);
functions
TransformInput: Input -> Command`Direction * Command`Direction *
Command`Direction * Command`Direction *
HandControlUnit`Mode * HandControlUnit`Button *
Command`AxisMap
TransformInput (inp) ==
let [mode,aah,horiz,trans,vert,twist,roll,pitch,yaw] = inp in
mk_( ConvertAxisCmd(horiz),
ConvertAxisCmd(twist),
ConvertAxisCmd(trans),
ConvertAxisCmd(vert),
if mode = 1 then <Tran> else <Rot>,
if aah = 0 then <Up> else <Down>,
{ <axis3> |-> ConvertAxisCmd(roll),
<axis1> |-> ConvertAxisCmd(pitch),
<axis2> |-> ConvertAxisCmd(yaw) } );
ConvertAxisCmd: nat -> Command`Direction
ConvertAxisCmd(n) ==
cases n:
0 -> <Neg>,
1 -> <Pos>,
2 -> <Zero>,
others -> undefined
end;
GenerateThrusterMatrix: set of ThrusterControl`ThrusterPosition +>
ThrusterMatrix
GenerateThrusterMatrix (ts) ==
let tson = { GenerateThrusterLabel (t) | t in set ts } in
[ [ mk_(j,i) in set tson | i in set {1,...,6} ]
| j in set {1,...,4} ];
GenerateThrusterLabel: ThrusterControl`ThrusterPosition +> nat * nat
GenerateThrusterLabel (tnm) ==
cases tnm:
<B1> -> mk_(1,4),
<B2> -> mk_(2,4),
<B3> -> mk_(4,4),
<B4> -> mk_(3,4),
<F1> -> mk_(1,1),
<F2> -> mk_(2,1),
<F3> -> mk_(4,1),
<F4> -> mk_(3,1),
<L1R> -> mk_(1,2),
<L1F> -> mk_(1,3),
<R2R> -> mk_(2,2),
<R2F> -> mk_(2,3),
<L3R> -> mk_(4,2),
<L3F> -> mk_(4,3),
<R4R> -> mk_(3,2),
<R4F> -> mk_(3,3),
<D1R> -> mk_(1,6),
<D1F> -> mk_(1,5),
<D2R> -> mk_(2,6),
<D2F> -> mk_(2,5),
<U3R> -> mk_(4,6),
<U3F> -> mk_(4,5),
<U4R> -> mk_(3,6),
<U4F> -> mk_(3,5)
end;
values
thrusters = mk_(<Pos>,<Zero>,<Zero>,<Zero>,<Tran>,<Down>,
{ <Roll> |-> <Zero>, <Pitch> |-> <Zero>, <Yaw> |-> <Zero> })
end Interface
Clock.vdmpp
class Clock
instance variables
count : nat := 0;
operations
public
SetTime : nat ==> ()
SetTime(t) ==
count := t;
public
IncrTime : () ==> ()
IncrTime() ==
count := count + 1;
public
ReadTime : () ==> nat
ReadTime() ==
return count;
end Clock