process env_Regulator = { integer Regulator_fifo_size, Speed_fifo_size; } ( ? boolean Bms; boolean BCarStarter, BOnOffReg, BpressBrakePedal, BpressAcceleratorPedal, BreleaseAcceleratorPedal; ! ) (| Bms ^= BCarStarter ^= BOnOffReg ^= BpressBrakePedal ^= BpressAcceleratorPedal ^= BreleaseAcceleratorPedal ^= Tick | ms := when Bms | CarStarter := when BCarStarter | OnOffReg := when BOnOffReg | pressBrakePedal := when BpressBrakePedal | pressAcceleratorPedal := when BpressAcceleratorPedal | releaseAcceleratorPedal := when BreleaseAcceleratorPedal | Tick := ms ^+ CarStarter ^+ OnOffReg ^+ pressBrakePedal ^+ pressAcceleratorPedal ^+ releaseAcceleratorPedal | main_Regulator{Regulator_fifo_size, Speed_fifo_size} (Tick, ms, CarStarter, OnOffReg, pressBrakePedal, pressAcceleratorPedal, releaseAcceleratorPedal) |) where event Tick, ms, CarStarter, OnOffReg, pressBrakePedal, pressAcceleratorPedal, releaseAcceleratorPedal; process main_Regulator = { integer Regulator_fifo_size, Speed_fifo_size; } ( ? event Tick; event ms; event CarStarter, OnOffReg, pressBrakePedal, pressAcceleratorPedal, releaseAcceleratorPedal; ! ) (| sub_main_Regulator{Regulator_fifo_size, Speed_fifo_size} (Tick, ms, CarStarter, OnOffReg, pressBrakePedal, pressAcceleratorPedal, releaseAcceleratorPedal) |) where statevar integer Speed_value; statevar dreal ControlEquation_regulatingCoefficient init 0.6; statevar integer ControlEquation_orderedSpeed; constant integer code_Regulator = 1; constant integer code_Speed = 2; constant integer nb_inserted = 8; type code_sender = enum (dummy, startRegulating, maintainSpeed); process sub_main_Regulator = { integer Regulator_fifo_size, Speed_fifo_size; } ( ? event input_Tick; event ms; event CarStarter, OnOffReg, pressBrakePedal, pressAcceleratorPedal, releaseAcceleratorPedal; ! ) (| (counter, zcounter) := upsample(nb_inserted when input_Tick, input_Tick) | upsample_clk := ^counter | (trigger_giveSpeed, giveSpeed_caller) := exec_Regulator_chart{Regulator_fifo_size} (upsample_clk, zcounter, ms, CarStarter, OnOffReg, speedTooLow, pressBrakePedal, pressAcceleratorPedal, releaseAcceleratorPedal, speed, transmitted_giveSpeed_caller) | (speedTooLow, speed, transmitted_giveSpeed_caller) := exec_Speed_chart{Speed_fifo_size} (upsample_clk, zcounter, ms, CarStarter, trigger_giveSpeed, giveSpeed_caller) |) where integer counter, zcounter; event upsample_clk; event trigger_giveSpeed, speedTooLow; code_sender giveSpeed_caller, transmitted_giveSpeed_caller; integer speed; use Interface; use Speed; use ControlEquation; use Regulator; end; end; end;