fact: Definition PaintballMonitorSpec : RADLM_ADT Landshark_Topics PaintballMonitorNode unit := let _ := {| NetworkTopicNames := LandsharkTopicNames |} in let _ := {| NetworkTopicTypes := LandsharkTopicTypes |} in ADTRep unit { Def Constructor RADL_Init (_ : unit) : rep := ret tt, Def Method RADL_Start_Step (r : rep, msg : RADLM_start_msg_t NetworkTopicTypes NetworkTopicNames PaintballMonitorNode) : _ := msg' <- { msg' | IF Word.wlt (GetMessageTopicS (radlm_monitor_in msg) turret_tilt "data") (Word.natToWord _ 45) then msg' = (UpdateMessageTopicS (radlm_in msg) trigger "data" O_8, radlm_in_flags msg) else msg' = (radlm_in msg, radlm_in_flags msg) }; ret (r, msg'), Def Method RADL_Finish_Step (r : rep, msg : RADLM_finish_msg_t NetworkTopicTypes NetworkTopicNames PaintballMonitorNode) : _ := ret (r, (radlm_out msg, radlm_out_flags msg, ConstructMessage NetworkTopicTypes NetworkTopicNames (Vector.nil _) (ilist2.inil2)))}.
imports: Coq.Strings.String Coq.Bool.Bool Coq.Lists.List Coq.Program.Program Coq.Arith.Arith Fiat.ADT Fiat.ADT.ComputationalADT Fiat.ADTNotation Fiat.ADTRefinement Fiat.ADTRefinement.BuildADTRefinements Fiat.Fiat4Monitors.RADL_Topics Fiat.Fiat4Monitors.RADL_Messages Fiat.Fiat4Monitors.RADL_Flags Fiat.Fiat4Monitors.RADL_Nodes Fiat.Fiat4Monitors.RADLNodeADTs Fiat.Fiat4Monitors.LandsharkTopics Fiat.Fiat4Monitors.LandsharkNodes Fiat.Fiat4Monitors.RADL_Notations