ROSCOQ.icreateConcrete
Require Export iCreateMoveToLoc.
Definition rotSpeedRadPerSec : Qpos := QposMake 1 2.
Definition speedMetresPerSec : Qpos := QposMake 1 10.
Definition delResSecInv : positive := (1000)%positive.
Definition delEpsSec : Qpos := QposMake 1 10000.
Definition initDelayLin : Qpos := QposMake 1 1.
Definition robotProgramInstance (delayLinSec : Qpos) : PureProcWDelay TARGETPOS VELOCITY :=
robotPureProgam
rotSpeedRadPerSec
speedMetresPerSec
delayLinSec
delEpsSec
delResSecInv.
To ensure that the Java shim maintains the state correctly,
we make this process whose state is non-trivial and
stores the delay between the "stop-turning" and
the "start-moving" message.
At each update, this value is doubled.
Definition SwProcessInstance : Process Message (list Message):=
{|
State := Q;
curState := initDelayLin;
handler := λ (ins : Q) (inm : Message),
(ins × 2,
delayedLift2Mesg (robotProgramInstance (QabsQpos ins)) inm) |}.
Definition target1Metres : Cart2D Q
:= {|X:= - Qmake 1 1 ; Y:= Qmake 1 1|}.
Definition mkInpMsg (mp : Cart2D Q) : Message := mkTargetMsg mp.
Definition StateType : Type.
let t := eval vm_compute in (State SwProcessInstance) in exact t.
Defined.
Definition state0 := curState SwProcessInstance.
Definition nthMsgPayload (lm : list Message)
(tp : Topic) (n:nat) : option (topicType tp) :=
getPayloadOp tp (nth_error lm n).
Definition nthVelMsgPayload (lm : list Message)
(n:nat) : option (Polar2D Q) :=
nthMsgPayload lm VELOCITY n.
Definition nthDelay (resp : list Message) (n:nat) : option Q :=
option_map (delay ∘ snd) (nth_error resp n).
Definition nthLinVel (resp : list Message) (n:nat) : option Q :=
option_map ((@rad _)) (nthVelMsgPayload resp n).
Definition nthTheta (resp : list Message) (n:nat) : option Q :=
option_map ((@θ _)) (nthVelMsgPayload resp n).
Definition QNumOp : option Q → option Z :=
option_map Qnum.
Definition QDenOp : option Q → option positive :=
option_map Qden.