diff --git a/test/known-good/C/src/GenDelayTest.html b/test/known-good/C/src/GenDelayTest.html new file mode 100644 index 000000000..67305d149 --- /dev/null +++ b/test/known-good/C/src/GenDelayTest.html @@ -0,0 +1,194 @@ + +/** + + + + * Test that types used in delayed connections do not need to be in scope for the parent reactor in + + + + * order to compile. + + + + + + +*/ + + + +target + + + + + +C + + + + + + + +import + + + + + +Source + + +, + + +Sink + + + + + +from + + + + + +" + + +lib/GenDelay.lf + + +" + + + + + + + +main + + + + + +reactor + + + { + + + + + + +source + + + + + += + + + + + +new + + + + + +Source + + +() + + + + + + +sink + + + + + += + + + + + +new + + + + + +Sink + + +() + + + + + + +source + + +. + + +out + + + + + +-> + + + + + +sink + + +. + + +in + + + + + +after + + + + + +10 + + + ms + + + +} + + + + + + diff --git a/test/known-good/C/src/federated/SpuriousDependency.html b/test/known-good/C/src/federated/SpuriousDependency.html new file mode 100644 index 000000000..7b1645d39 --- /dev/null +++ b/test/known-good/C/src/federated/SpuriousDependency.html @@ -0,0 +1,1008 @@ + +/** + + + + * This checks that a federated program does not deadlock when it is ambiguous, given the structure + + + + * of a federate, whether it is permissible to require certain network sender/receiver reactions to + + + + * precede others in the execution of a given tag. + + + + + + +*/ + + + +target + + + + + +C + + + { + + + + timeout + + +: + + +1 + + + + + +sec + + + +} + + + + + + + +reactor + + + + + +Passthrough + + +(id: + + +int + + + + + += + + + + + +0 + + +) { + + + + + + +input + + + + + +in + + +: + + + + + +int + + + + + + +output + + + + + +out + + +: + + + + + +int + + + + + + + + + + +reaction + + +( + + +in) + + +-> + + + out { + + += + + + + lf_print( + + +" + + +Hello from passthrough %d + + +" + + +, self + + +-> + + +id); + + + + lf_set(out, in + + +-> + + +value); + + + + + + += + + +} + + + +} + + + + + + + +reactor + + + + + +Twisty + + + { + + + + + + +input + + + + + +in0 + + +: + + + + + +int + + + + + + +input + + + + + +in1 + + +: + + + + + +int + + + + + + +output + + + + + +out0 + + +: + + + + + +int + + + + + + +output + + + + + +out1 + + +: + + + + + +int + + + + + + +p0 + + + + + += + + + + + +new + + + + + +Passthrough + + +(id + + += + + +0 + + +) + + + + + + +p1 + + + + + += + + + + + +new + + + + + +Passthrough + + +(id + + += + + +1 + + +) + + + + in0 + + +-> + + + + + +p0 + + +. + + +in + + + + + + +p0 + + +. + + +out + + + + + +-> + + + out0 + + + + in1 + + +-> + + + + + +p1 + + +. + + +in + + + + + + +p1 + + +. + + +out + + + + + +-> + + + out1 + + + +} + + + + + + + +reactor + + + + + +Check + + + { + + + + + + +input + + + + + +in + + +: + + + + + +int + + + + + + + + + + +state + + + + + +count + + +: + + + + + +int + + + + + += + + + + + +0 + + + + + + + + + + +reaction + + +( + + +in) { + + += + + + lf_print( + + +" + + +count is now %d + + +" + + +, + + ++ + + ++ + + +self + + +-> + + +count); + + += + + +} + + + + + + + + + + +reaction + + +( + + +shutdown + + +) { + + += + + + + lf_print( + + +" + + +******* Shutdown invoked. + + +" + + +); + + + + if (self + + +-> + + +count ! + + += + + + + + +1 + + +) { + + + + lf_print_error_and_exit( + + +" + + +Failed to receive expected input. + + +" + + +); + + + + } + + + + + + += + + +} + + + +} + + + + + + + +federated + + + + + +reactor + + + { + + + + + + +t0 + + + + + += + + + + + +new + + + + + +Twisty + + +() + + + + + + +t1 + + + + + += + + + + + +new + + + + + +Twisty + + +() + + + + + + +check + + + + + += + + + + + +new + + + + + +Check + + +() + + + + + + +t0 + + +. + + +out1 + + + + + +-> + + + + + +t1 + + +. + + +in0 + + + + + + +t1 + + +. + + +out1 + + + + + +-> + + + + + +t0 + + +. + + +in0 + + + + + + +state + + + + + +count + + +: + + + + + +int + + + + + += + + + + + +0 + + + + + + + + + + +t1 + + +. + + +out0 + + + + + +-> + + + + + +check + + +. + + +in + + + + + + + + + + +reaction + + +( + + +startup + + +) + + +-> + + + + + +t0 + + +. + + +in1 + + + { + + += + + + lf_set( + + +t0 + + +. + + +in1 + + +, + + +0 + + +); + + += + + +} + + + +} + + + + + + diff --git a/test/known-good/C/src/lib/GenDelay.html b/test/known-good/C/src/lib/GenDelay.html new file mode 100644 index 000000000..beeeadae2 --- /dev/null +++ b/test/known-good/C/src/lib/GenDelay.html @@ -0,0 +1,214 @@ + +target + + + + + +C + + + + + + + +preamble + + + { + + += + + + typedef int message_t; + + += + + +} + + + + + + + +reactor + + + + + +Source + + + { + + + + + + +output + + + + + +out + + +: + + + + + +message_t + + + + + + + + + + +reaction + + +( + + +startup + + +) + + +-> + + + out { + + += + + + lf_set(out, + + +42 + + +); + + += + + +} + + + +} + + + + + + + +reactor + + + + + +Sink + + + { + + + + + + +input + + + + + +in + + +: + + + + + +message_t + + + + + + + + + + +reaction + + +( + + +in) { + + += + + + lf_print( + + +" + + +Received %d at time %lld + + +" + + +, in + + +-> + + +value, lf_time_logical_elapsed()); + + += + + +} + + + +} + + + + + + diff --git a/test/known-good/C/src/verifier/ADASModel.html b/test/known-good/C/src/verifier/ADASModel.html new file mode 100644 index 000000000..62064edd4 --- /dev/null +++ b/test/known-good/C/src/verifier/ADASModel.html @@ -0,0 +1,1618 @@ + +target + + + + + +C + + + + + + + +preamble + + + { + + += + + + + typedef int c_frame_t; + + + + typedef int l_frame_t; + + + += + + +} + + + + + + + +reactor + + + + + +Camera + + + { + + + + + + +output + + + + + +out + + +: + + + + + +{ + + += + + + c_frame_t + + += + + +} + + + + + + +state + + + + + +frame + + +: + + + + + +{ + + += + + + c_frame_t + + += + + +} + + + + + + +timer + + + t( + + +0 + + +, + + +17 + + + + + +msec + + +) + + +// 60 fps + + + + + + + + + + +reaction + + +( + + +t) + + +-> + + + out { + + += + + + + + + +// Capture a frame. + + + + self + + +-> + + +frame + + += + + + + + +1 + + +; + + + + lf_set(out, self + + +-> + + +frame); + + + + + + += + + +} + + + +} + + + + + + + +reactor + + + + + +LiDAR + + + { + + + + + + +output + + + + + +out + + +: + + + + + +{ + + += + + + l_frame_t + + += + + +} + + + + + + +state + + + + + +frame + + +: + + + + + +{ + + += + + + l_frame_t + + += + + +} + + + + + + +timer + + + t( + + +0 + + +, + + +34 + + + + + +msec + + +) + + +// 30 fps + + + + + + + + + + +reaction + + +( + + +t) + + +-> + + + out { + + += + + + + + + +// Capture a frame. + + + + self + + +-> + + +frame + + += + + + + + +2 + + +; + + + + lf_set(out, self + + +-> + + +frame); + + + + + + += + + +} + + + +} + + + + + + + +reactor + + + + + +Pedal + + + { + + + + + + +output + + + + + +out + + +: + + + + + +int + + + + + + +physical + + + + + +action + + + + + +a + + + + + + + + + + +reaction + + +( + + +a) + + +-> + + + out { + + += + + + lf_set(out, + + +1 + + +); + + += + + +} + + + +} + + + + + + + +reactor + + + + + +Brakes + + + { + + + + + + +input + + + + + +inADAS + + +: + + + + + +int + + + + + + +input + + + + + +inPedal + + +: + + + + + +int + + + + + + +state + + + + + +brakesApplied + + +: + + + + + +int + + + + + += + + + + + +0 + + + + + + + + + + +reaction + + +( + + +inADAS, inPedal) { + + += + + + + + + +// Actuate brakes. + + + + self + + +-> + + +brakesApplied + + += + + + + + +1 + + +; + + + + + + += + + +} + + +deadline + + +( + + +10 + + + + + +msec + + +) { + + += + + + + + += + + +} + + + +} + + + + + + + +reactor + + + + + +ADASProcessor + + + { + + + + + + +input + + + + + +in1 + + +: + + + + + +{ + + += + + + l_frame_t + + += + + +} + + + + + + +input + + + + + +in2 + + +: + + + + + +{ + + += + + + c_frame_t + + += + + +} + + + + + + +output + + + + + +out1 + + +: + + + + + +int + + + + + + +output + + + + + +out2 + + +: + + + + + +int + + + + + + +logical + + + + + +action + + + + + +a + + +( + + +50 + + + + + +msec + + +) + + + + + + +state + + + + + +requestStop + + +: + + + + + +int + + + + + + + + + + +reaction + + +( + + +in1, in2) + + +-> + + + a { + + += + + + + + + +// ... Detect danger + + + + + + +// and request stop. + + + + lf_schedule(a, + + +0 + + +); + + + + self + + +-> + + +requestStop + + += + + + + + +1 + + +; + + + + + + += + + +} + + + + + + + + + + +reaction + + +( + + +a) + + +-> + + + out1, out2 { + + += + + + + if (self + + +-> + + +requestStop + + += + + += + + + + + +1 + + +) + + + + lf_set(out1, + + +1 + + +); + + + + + + += + + +} + + +deadline + + +( + + +20 + + + + + +msec + + +) { + + += + + + + + += + + +} + + + +} + + + + + + + +reactor + + + + + +Dashboard + + + { + + + + + + +input + + + + + +in + + +: + + + + + +int + + + + + + +state + + + + + +received + + +: + + + + + +int + + + + + + + + + + +reaction + + +( + + +in) { + + += + + + self + + +-> + + +received + + += + + + + + +1 + + +; + + += + + +} + + + +} + + + + + + + +@ + + +property( + + + + name + + += + + + + + +" + + +responsive + + +" + + +, + + + + tactic + + += + + + + + +" + + +bmc + + +" + + +, + + + + spec + + += + + + + + +" + + +G[0, 10 ms]((ADASModel_l_reaction_0 && (F[0](ADASModel_p_requestStop == 1))) ==> (F[0, 55 ms]( ADASModel_b_brakesApplied == 1 ))) + + +" + + +, + + + + expect + + += + + + + + +true + + +) + + + +main + + + + + +reactor + + + + + +ADASModel + + + { + + + + + + +c + + + + + += + + + + + +new + + + + + +Camera + + +() + + + + + + +l + + + + + += + + + + + +new + + + + + +LiDAR + + +() + + + + + + +p + + + + + += + + + + + +new + + + + + +ADASProcessor + + +() + + + + + + +b + + + + + += + + + + + +new + + + + + +Brakes + + +() + + + + + + +d + + + + + += + + + + + +new + + + + + +Dashboard + + +() + + + + + + +l + + +. + + +out + + + + + +-> + + + + + +p + + +. + + +in1 + + + + + +// p = new Pedal(); + + + + + + +c + + +. + + +out + + + + + +-> + + + + + +p + + +. + + +in2 + + + + + + +p + + +. + + +out2 + + + + + +-> + + + + + +d + + +. + + +in + + + + + + +p + + +. + + +out1 + + + + + +-> + + + + + +b + + +. + + +inADAS + + + + + +after + + + + + +5 + + + + + +msec + + + + + +// p.out -> b.inPedal; + + + +} + + + + + + diff --git a/test/known-good/C/src/verifier/AircraftDoor.html b/test/known-good/C/src/verifier/AircraftDoor.html new file mode 100644 index 000000000..527d76027 --- /dev/null +++ b/test/known-good/C/src/verifier/AircraftDoor.html @@ -0,0 +1,752 @@ + +target + + + + + +C + + + + + + + +reactor + + + + + +Controller + + + { + + + + + + +output + + + + + +out + + +: + + + + + +int + + + + + + + + + + +reaction + + +( + + +startup + + +) + + +-> + + + out { + + += + + + lf_set(out, + + +1 + + +); + + += + + +} + + + +} + + + + + + + +reactor + + + + + +Vision + + + { + + + + + + +input + + + + + +in + + +: + + + + + +int + + + + + + +output + + + + + +out + + +: + + + + + +int + + + + + + +state + + + + + +ramp + + +: + + + + + +int + + + + + += + + + + + +0 + + + + + + + + + + +reaction + + +( + + +in) + + +-> + + + out { + + += + + + + if (self + + +-> + + +ramp + + += + + += + + + + + +1 + + +) { + + + + lf_set(out, + + +0 + + +); + + +// 0 = Do not open. + + + + } else { + + + + lf_set(out, + + +1 + + +); + + +// 1 = Open. + + + + } + + + + + + += + + +} + + + +} + + + + + + + +reactor + + + + + +Door + + + { + + + + + + +input + + + + + +in + + +: + + + + + +int + + + + + + +state + + + + + +doorOpen + + +: + + + + + +int + + + + + + + + + + +reaction + + +( + + +in) { + + += + + + + if (in + + +-> + + +value + + += + + += + + + + + +1 + + +) + + + + self + + +-> + + +doorOpen + + += + + + + + +1 + + +; + + +// Open + + + + else if (in + + +-> + + +value + + += + + += + + + + + +0 + + +) + + + + self + + +-> + + +doorOpen + + += + + + + + +0 + + +; + + +// Closed + + + + + + += + + +} + + + +} + + + + + + + +@ + + +property( + + + + name + + += + + + + + +" + + +vision_works + + +" + + +, + + + + tactic + + += + + + + + +" + + +bmc + + +" + + +, + + + + spec + + += + + + + + +" + + +((AircraftDoor_vision_ramp == 0) ==> (G[0 sec](AircraftDoor_door_reaction_0 ==> (AircraftDoor_door_doorOpen == 1)))) + + +" + + +, + + + + expect + + += + + + + + +true + + +) + + + +main + + + + + +reactor + + + + + +AircraftDoor + + + { + + + + + + +controller + + + + + += + + + + + +new + + + + + +Controller + + +() + + + + + + +vision + + + + + += + + + + + +new + + + + + +Vision + + +() + + + + + + +door + + + + + += + + + + + +new + + + + + +Door + + +() + + + + + + +controller + + +. + + +out + + + + + +-> + + + + + +vision + + +. + + +in + + + + + + +vision + + +. + + +out + + + + + +-> + + + + + +door + + +. + + +in + + + +} + + + + + + diff --git a/test/known-good/C/src/verifier/Alarm.html b/test/known-good/C/src/verifier/Alarm.html new file mode 100644 index 000000000..2b0492788 --- /dev/null +++ b/test/known-good/C/src/verifier/Alarm.html @@ -0,0 +1,552 @@ + +target + + + + + +C + + + + + + + +reactor + + + + + +Controller + + + { + + + + + + +output + + + + + +out + + +: + + + + + +int + + + + + + +output + + + + + +out2 + + +: + + + + + +int + + + + + + +state + + + + + +fault + + +: + + + + + +int + + + + + + + + + + +logical + + + + + +action + + + + + +turnOff + + +( + + +1 + + + + + +sec + + +): + + +int + + + + + + + + + + +@ + + +label( + + +" + + +Computation + + +" + + +) + + + + + + +reaction + + +( + + +startup + + +) + + +-> + + + out, out2, turnOff { + + += + + + + + + +// ... Operation + + + + self + + +-> + + +fault + + += + + + + + +1 + + +; + + +// Fault occurs + + + + + + + + + + +// Fault handling + + + + if (self + + +-> + + +fault + + += + + += + + + + + +1 + + +) { + + + + lf_schedule(turnOff, + + +0 + + +); + + +// Wrong action value. Should be 1. + + + + lf_set(out, + + +5 + + +); + + + + lf_set(out2, + + +10 + + +); + + + + } + + + + + + += + + +} + + + + + + + + + + +@ + + +label( + + +" + + +Stop + + +" + + +) + + + + + + +reaction + + +( + + +turnOff) { + + += + + + + + + +// Trigger the alarm and reset fault. + + + + if (turnOff + + +-> + + +value + + += + + += + + + + + +1 + + +) + + + + self + + +-> + + +fault + + += + + + + + +0 + + +; + + + + + + += + + +} + + + +} + + + + + + + +@ + + +property( + + + + name + + += + + + + + +" + + +machine_stops_within_1_sec + + +" + + +, + + + + tactic + + += + + + + + +" + + +bmc + + +" + + +, + + + + spec + + += + + + + + +" + + +G[0, 1 sec]((Alarm_c_reaction_0) ==> F(0, 1 sec](Alarm_c_reaction_1))) + + +" + + +, + + + + expect + + += + + + + + +true + + +) + + + +main + + + + + +reactor + + + { + + + + + + +c + + + + + += + + + + + +new + + + + + +Controller + + +() + + + +} + + + + + + diff --git a/test/known-good/C/src/verifier/CoopSchedule.html b/test/known-good/C/src/verifier/CoopSchedule.html new file mode 100644 index 000000000..7931cce76 --- /dev/null +++ b/test/known-good/C/src/verifier/CoopSchedule.html @@ -0,0 +1,697 @@ + +target + + + + + +C + + + + + + + +reactor + + + + + +Trigger + + + { + + + + + + +output + + + + + +out + + +: + + + + + +int + + + + + + +timer + + + t( + + +0 + + +, + + +1 + + + + + +usec + + +) + + + + + + + + + + +reaction + + +( + + +t) + + +-> + + + out { + + += + + + lf_set(out, + + +1 + + +); + + += + + +} + + + +} + + + + + + + +reactor + + + + + +Task + + + { + + + + + + +input + + + + + +cnt + + +: + + + + + +int + + + + + + +state + + + + + +counter + + +: + + + + + +int + + + + + += + + + + + +0 + + + + + + + + + + +reaction + + +( + + +cnt) { + + += + + + + self + + +-> + + +counter + + ++ + + += + + + + + +2 + + +; + + +// Should be 1. + + + + + + += + + +} + + + +} + + + + + + + +@ + + +property( + + + + name + + += + + + + + +" + + +upperbound + + +" + + +, + + + + tactic + + += + + + + + +" + + +bmc + + +" + + +, + + + + spec + + += + + + + + +" + + +G[0, 1 usec]((CoopSchedule_task1_counter + CoopSchedule_task2_counter + CoopSchedule_task3_counter + CoopSchedule_task4_counter + CoopSchedule_task5_counter) < 15) + + +" + + +, + + + + expect + + += + + + + + +false + + +) + + + +main + + + + + +reactor + + + { + + + + + + +trigger + + + + + += + + + + + +new + + + + + +Trigger + + +() + + + + + + +task1 + + + + + += + + + + + +new + + + + + +Task + + +() + + +// TODO: Put these reactors in a bank. + + + + + + +task2 + + + + + += + + + + + +new + + + + + +Task + + +() + + + + + + +task3 + + + + + += + + + + + +new + + + + + +Task + + +() + + + + + + +task4 + + + + + += + + + + + +new + + + + + +Task + + +() + + + + + + +task5 + + + + + += + + + + + +new + + + + + +Task + + +() + + + + + + +trigger + + +. + + +out + + + + + +-> + + + + + +task1 + + +. + + +cnt + + + + + + +trigger + + +. + + +out + + + + + +-> + + + + + +task2 + + +. + + +cnt + + + + + + +trigger + + +. + + +out + + + + + +-> + + + + + +task3 + + +. + + +cnt + + + + + + +trigger + + +. + + +out + + + + + +-> + + + + + +task4 + + +. + + +cnt + + + + + + +trigger + + +. + + +out + + + + + +-> + + + + + +task5 + + +. + + +cnt + + + +} + + + + + + diff --git a/test/known-good/C/src/verifier/Election2.html b/test/known-good/C/src/verifier/Election2.html new file mode 100644 index 000000000..54fc588c4 --- /dev/null +++ b/test/known-good/C/src/verifier/Election2.html @@ -0,0 +1,1274 @@ + +target + + + + + +C + + + + + + + +reactor + + + + + +Node0 + + + { + + + + + + +input + + + + + +in + + +: + + + + + +int + + + + + + +output + + + + + +out + + +: + + + + + +int + + + + + + +state + + + + + +id + + +: + + + + + +int + + + + + + +state + + + + + +elected + + +: + + + + + +int + + + + + += + + + + + +0 + + + + + + + + + + +reaction + + +( + + +startup + + +) + + +-> + + + out { + + += + + + + self + + +-> + + +id + + += + + + + + +0 + + +; + + + + lf_set(out, self + + +-> + + +id); + + + + + + += + + +} + + + + + + + + + + +reaction + + +( + + +in) + + +-> + + + out { + + += + + + + if (in + + +-> + + +value > self + + +-> + + +id) { + + + + lf_set(out, in + + +-> + + +value); + + + + } else if (in + + +-> + + +value + + += + + += + + + self + + +-> + + +id) { + + + + self + + +-> + + +elected + + += + + + + + +1 + + +; + + + + } + + + + + + += + + +} + + + +} + + + + + + + +reactor + + + + + +Node1 + + + { + + + + + + +input + + + + + +in + + +: + + + + + +int + + + + + + +output + + + + + +out + + +: + + + + + +int + + + + + + +state + + + + + +id + + +: + + + + + +int + + + + + + +state + + + + + +elected + + +: + + + + + +int + + + + + += + + + + + +0 + + + + + + + + + + +reaction + + +( + + +startup + + +) + + +-> + + + out { + + += + + + + self + + +-> + + +id + + += + + + + + +1 + + +; + + + + lf_set(out, self + + +-> + + +id); + + + + + + += + + +} + + + + + + + + + + +reaction + + +( + + +in) + + +-> + + + out { + + += + + + + if (in + + +-> + + +value > self + + +-> + + +id) { + + + + lf_set(out, in + + +-> + + +value); + + + + } else if (in + + +-> + + +value + + += + + += + + + self + + +-> + + +id) { + + + + self + + +-> + + +elected + + += + + + + + +1 + + +; + + + + } + + + + + + += + + +} + + + +} + + + + + + + +reactor + + + + + +Node2 + + + { + + + + + + +input + + + + + +in + + +: + + + + + +int + + + + + + +output + + + + + +out + + +: + + + + + +int + + + + + + +state + + + + + +id + + +: + + + + + +int + + + + + + +state + + + + + +elected + + +: + + + + + +int + + + + + += + + + + + +0 + + + + + + + + + + +reaction + + +( + + +startup + + +) + + +-> + + + out { + + += + + + + self + + +-> + + +id + + += + + + + + +2 + + +; + + + + lf_set(out, self + + +-> + + +id); + + + + + + += + + +} + + + + + + + + + + +reaction + + +( + + +in) + + +-> + + + out { + + += + + + + if (in + + +-> + + +value > self + + +-> + + +id) { + + + + lf_set(out, in + + +-> + + +value); + + + + } else if (in + + +-> + + +value + + += + + += + + + self + + +-> + + +id) { + + + + self + + +-> + + +elected + + += + + + + + +1 + + +; + + + + } + + + + + + += + + +} + + + +} + + + + + + + +// This property being checked does not hold. A valid property is F[0, 30 msec]((Election2_i0_elected + Election2_i1_elected + Election2_i2_elected) == 1) + + + +@ + + +property( + + + + name + + += + + + + + +" + + +exactly_one_elected + + +" + + +, + + + + tactic + + += + + + + + +" + + +bmc + + +" + + +, + + + + spec + + += + + + + + +" + + +F[0, 20 msec]((Election2_i0_elected + Election2_i1_elected + Election2_i2_elected) == 1) + + +" + + +, + + + + expect + + += + + + + + +false + + +) + + + +main + + + + + +reactor + + + { + + + + + + +i0 + + + + + += + + + + + +new + + + + + +Node0 + + +() + + + + + + +i1 + + + + + += + + + + + +new + + + + + +Node1 + + +() + + + + + + +i2 + + + + + += + + + + + +new + + + + + +Node2 + + +() + + + + + + +i0 + + +. + + +out + + + + + +-> + + + + + +i1 + + +. + + +in + + + + + +after + + + + + +10 + + + + + +msec + + + + + + +i1 + + +. + + +out + + + + + +-> + + + + + +i2 + + +. + + +in + + + + + +after + + + + + +10 + + + + + +msec + + + + + + +i2 + + +. + + +out + + + + + +-> + + + + + +i0 + + +. + + +in + + + + + +after + + + + + +10 + + + + + +msec + + + +} + + + + + + diff --git a/test/known-good/C/src/verifier/PingPongVerifier.html b/test/known-good/C/src/verifier/PingPongVerifier.html new file mode 100644 index 000000000..18a817eec --- /dev/null +++ b/test/known-good/C/src/verifier/PingPongVerifier.html @@ -0,0 +1,885 @@ + +/** + + + + * Basic benchmark from the Savina benchmark suite that is intended to measure message-passing + + + + * overhead. This is based on https://www.scala-lang.org/old/node/54 See + + + + * https://shamsimam.github.io/papers/2014-agere-savina.pdf. + + + + * + + + + * Ping introduces a microstep delay using a logical action to break the causality loop. + + + + * + + + + * To get a sense, some (informal) results for 1,000,000 ping-pongs on my Mac: + + + + * + + + + * - Unthreaded: 97 msec + + + + * - Threaded: 265 msec + + + + * + + + + * There is no parallelism in this application, so it does not benefit from being being threaded, + + + + * just some additional overhead. + + + + * + + + + * These measurements are total execution time, including startup and shutdown. These are about an + + + + * order of magnitude faster than anything reported in the paper. + + + + + + +*/ + + + +target + + + + + +C + + + { + + + + fast + + +: + + +true + + + +} + + + + + + + +reactor + + + + + +Ping + + + { + + + + + + +input + + + + + +receive + + +: + + + + + +int + + + + + + +output + + + + + +send + + +: + + + + + +int + + + + + + +state + + + + + +pingsLeft + + +: + + + + + +int + + + + + += + + + + + +10 + + + + + + +logical + + + + + +action + + + + + +serve + + +( + + +1 + + + + + +nsec + + +) + + + + + + + + + + +reaction + + +( + + +startup + + +) + + +-> + + + serve { + + += + + + + self + + +-> + + +pingsLeft + + += + + + + + +10 + + +; + + + + lf_schedule(serve, + + +0 + + +); + + + + + + += + + +} + + + + + + + + + + +reaction + + +( + + +serve) + + +-> + + + send { + + += + + + + lf_set(send, self + + +-> + + +pingsLeft); + + + + self + + +-> + + +pingsLeft + + +- + + += + + + + + +1 + + +; + + + + + + += + + +} + + + + + + + + + + +reaction + + +( + + +receive) + + +-> + + + serve { + + += + + + + if (self + + +-> + + +pingsLeft > + + +0 + + +) { + + + + lf_schedule(serve, + + +0 + + +); + + + + } + + + + + + += + + +} + + + +} + + + + + + + +reactor + + + + + +Pong + + + { + + + + + + +input + + + + + +receive + + +: + + + + + +int + + + + + + +output + + + + + +send + + +: + + + + + +int + + + + + + +state + + + + + +count + + +: + + + + + +int + + + + + += + + + + + +0 + + + + + + +state + + + + + +expected + + +: + + + + + +int + + + + + += + + + + + +10 + + + + + + + + + + +reaction + + +( + + +receive) + + +-> + + + send { + + += + + + + self + + +-> + + +count + + ++ + + += + + + + + +1 + + +; + + + + lf_set(send, receive + + +-> + + +value); + + + + + + += + + +} + + + +} + + + + + + + +@ + + +property( + + + + name + + += + + + + + +" + + +no_two_consecutive_pings + + +" + + +, + + + + tactic + + += + + + + + +" + + +bmc + + +" + + +, + + + + spec + + += + + + + + +" + + +G[0, 4 nsec](PingPongVerifier_ping_reaction_1 ==> X(!PingPongVerifier_ping_reaction_1)) + + +" + + +, + + + + expect + + += + + + + + +false + + +) + + + +main + + + + + +reactor + + + + + +PingPongVerifier + + + { + + + + + + +ping + + + + + += + + + + + +new + + + + + +Ping + + +() + + + + + + +pong + + + + + += + + + + + +new + + + + + +Pong + + +() + + + + + + +ping + + +. + + +send + + + + + +-> + + + + + +pong + + +. + + +receive + + + + + + +pong + + +. + + +send + + + + + +-> + + + + + +ping + + +. + + +receive + + + +} + + + + + + diff --git a/test/known-good/C/src/verifier/ProcessMsg.html b/test/known-good/C/src/verifier/ProcessMsg.html new file mode 100644 index 000000000..cf05e9223 --- /dev/null +++ b/test/known-good/C/src/verifier/ProcessMsg.html @@ -0,0 +1,688 @@ + +target + + + + + +C + + + + + + + +reactor + + + + + +Task + + + { + + + + + + +input + + + + + +in + + +: + + + + + +int + + + + + + +output + + + + + +out + + +: + + + + + +int + + + + + + + + + + +state + + + + + +messageSent + + +: + + + + + +int + + + + + + +state + + + + + +counter + + +: + + + + + +int + + + + + += + + + + + +0 + + + + + + +state + + + + + +panic + + +: + + + + + +int + + + + + += + + + + + +0 + + + + + + + + + + +timer + + + t( + + +0 + + +, + + +1 + + + + + +nsec + + +) + + + + + + + + + + +logical + + + + + +action + + + + + +updateMessage + + + + + + + + + + +reaction + + +( + + +startup + + +) { + + += + + + self + + +-> + + +messageSent + + += + + + + + +0 + + +; + + += + + +} + + + + + + + + + + +reaction + + +( + + +t) + + +-> + + + out { + + += + + + lf_set(out, self + + +-> + + +messageSent); + + += + + +} + + + + + + + + + + +reaction + + +( + + +in) + + +-> + + + updateMessage { + + += + + + + + + +/* + + + Check for invalid message. + + +*/ + + + + if (in + + +-> + + +value ! + + += + + + self + + +-> + + +messageSent) { + + + + self + + +-> + + +panic + + += + + + + + +1 + + +; + + + + } + + + + lf_schedule(updateMessage, + + +0 + + +); + + + + self + + +-> + + +counter + + ++ + + += + + + + + +1 + + +; + + + + + + += + + +} + + + + + + + + + + +reaction + + +( + + +updateMessage) { + + += + + + + + + +/* + + + Increment the last word of the 16-byte message. + + +*/ + + + + self + + +-> + + +messageSent + + ++ + + += + + + + + +1 + + +; + + + + + + += + + +} + + + +} + + + + + + + +@ + + +property( + + + + name + + += + + + + + +" + + +panic_free + + +" + + +, + + + + tactic + + += + + + + + +" + + +bmc + + +" + + +, + + + + spec + + += + + + + + +" + + +G[5 nsec](ProcessMsg_task_panic != 1) + + +" + + +, + + + + expect + + += + + + + + +true + + +) + + + +main + + + + + +reactor + + + { + + + + + + +task + + + + + += + + + + + +new + + + + + +Task + + +() + + + + + + +task + + +. + + +out + + + + + +-> + + + + + +task + + +. + + +in + + + +} + + + + + + diff --git a/test/known-good/C/src/verifier/ProcessSync.html b/test/known-good/C/src/verifier/ProcessSync.html new file mode 100644 index 000000000..652a4e806 --- /dev/null +++ b/test/known-good/C/src/verifier/ProcessSync.html @@ -0,0 +1,316 @@ + +target + + + + + +C + + + + + + + +reactor + + + + + +Task + + + { + + + + + + +/** + + + Define the counters used in the demo application... + + +*/ + + + + + + +state + + + + + +tm_synchronization_processing_counter + + +: + + + + + +int + + + + + += + + + + + +0 + + + + + + +timer + + + t( + + +0 + + +, + + +1 + + + + + +nsec + + +) + + + + + + + + + + +reaction + + +( + + +t) { + + += + + + + + + +/* + + + Increment the counter. + + +*/ + + + + self + + +-> + + +tm_synchronization_processing_counter + + ++ + + += + + + + + +1 + + +; + + + + + + += + + +} + + + +} + + + + + + + +@ + + +property( + + + + name + + += + + + + + +" + + +correctness + + +" + + +, + + + + tactic + + += + + + + + +" + + +bmc + + +" + + +, + + + + spec + + += + + + + + +" + + +G[2 nsec](ProcessSync_task_tm_synchronization_processing_counter == 3) + + +" + + +, + + + + expect + + += + + + + + +true + + +) + + + +main + + + + + +reactor + + + { + + + + + + +task + + + + + += + + + + + +new + + + + + +Task + + +() + + + +} + + + + + + diff --git a/test/known-good/C/src/verifier/Ring.html b/test/known-good/C/src/verifier/Ring.html new file mode 100644 index 000000000..fed90e607 --- /dev/null +++ b/test/known-good/C/src/verifier/Ring.html @@ -0,0 +1,1026 @@ + +/** + + + There seems to be some problem with infinite feedback loops. + + +*/ + + + +target + + + + + +C + + + + + + + +reactor + + + + + +Source + + + { + + + + + + +input + + + + + +in + + +: + + + + + +int + + + + + + +output + + + + + +out + + +: + + + + + +int + + + + + + +logical + + + + + +action + + + + + +start + + +( + + +1 + + + + + +nsec + + +) + + + + + + +state + + + + + +received + + +: + + + + + +int + + + + + + + + + + +reaction + + +( + + +startup + + +) + + +-> + + + start { + + += + + + + self + + +-> + + +received + + += + + + + + +0 + + +; + + + + lf_schedule(start, + + +0 + + +); + + + + + + += + + +} + + + + + + + + + + +reaction + + +( + + +start) + + +-> + + + out { + + += + + + lf_set(out, self + + +-> + + +received); + + += + + +} + + + + + + + + + + +/** + + + Uncomment the following to debug feedback loops. + + +*/ + + + + + + +// reaction(in) -> start {= + + + + + + +reaction + + +( + + +in) { + + += + + + + self + + +-> + + +received + + += + + + in + + +-> + + +value; + + + + + + +// lf_schedule(start, 0); + + + + + + += + + +} + + + +} + + + + + + + +reactor + + + + + +Node + + + { + + + + + + +input + + + + + +in + + +: + + + + + +int + + + + + + +output + + + + + +out + + +: + + + + + +int + + + + + + + + + + +reaction + + +( + + +in) + + +-> + + + out { + + += + + + lf_set(out, in + + +-> + + +value + + ++ + + + + + +1 + + +); + + += + + +} + + + +} + + + + + + + +@ + + +property( + + + + name + + += + + + + + +" + + +full_circle + + +" + + +, + + + + tactic + + += + + + + + +" + + +bmc + + +" + + +, + + + + spec + + += + + + + + +" + + +F[0, 10 nsec](Ring_s_reaction_2) + + +" + + +, + + + + expect + + += + + + + + +true + + +) + + + +main + + + + + +reactor + + + { + + + + + + +s + + + + + += + + + + + +new + + + + + +Source + + +() + + + + + + +n1 + + + + + += + + + + + +new + + + + + +Node + + +() + + + + + + +n2 + + + + + += + + + + + +new + + + + + +Node + + +() + + + + + + +n3 + + + + + += + + + + + +new + + + + + +Node + + +() + + + + + + +n4 + + + + + += + + + + + +new + + + + + +Node + + +() + + + + + + +n5 + + + + + += + + + + + +new + + + + + +Node + + +() + + + + + + +s + + +. + + +out + + + + + +-> + + + + + +n1 + + +. + + +in + + + + + +after + + + + + +1 + + + + + +nsec + + + + + + +n1 + + +. + + +out + + + + + +-> + + + + + +n2 + + +. + + +in + + + + + +after + + + + + +1 + + + + + +nsec + + + + + + +n2 + + +. + + +out + + + + + +-> + + + + + +n3 + + +. + + +in + + + + + +after + + + + + +1 + + + + + +nsec + + + + + + +n3 + + +. + + +out + + + + + +-> + + + + + +n4 + + +. + + +in + + + + + +after + + + + + +1 + + + + + +nsec + + + + + + +n4 + + +. + + +out + + + + + +-> + + + + + +n5 + + +. + + +in + + + + + +after + + + + + +1 + + + + + +nsec + + + + + + +n5 + + +. + + +out + + + + + +-> + + + + + +s + + +. + + +in + + + + + +after + + + + + +1 + + + + + +nsec + + + +} + + + + + + diff --git a/test/known-good/C/src/verifier/SafeSend.html b/test/known-good/C/src/verifier/SafeSend.html new file mode 100644 index 000000000..36f8fa54a --- /dev/null +++ b/test/known-good/C/src/verifier/SafeSend.html @@ -0,0 +1,787 @@ + +/** + + + + * (Original) Description: This example illustrates the "Verify Absence-of-Errors" mode. The server + + + + * expects a tuple `{REQUEST,PID-OF-SENDER}` but the main sends to it an atom instead of its pid, + + + + * then generating an exception when the server tries to send back a response to what he assumes to + + + + * be a pid. + + + + * + + + + * The verification step discovers a *genuine* counter-example. To inspect the error trace run bfc + + + + * on the generated model and look at the trace alongside the dot model of the ACS. + + + + + + +*/ + + + +target + + + + + +C + + + + + + + +reactor + + + + + +Client + + + { + + + + + + +input + + + + + +in + + +: + + + + + +int + + + + + + +output + + + + + +out + + +: + + + + + +int + + + + + + +state + + + + + +req + + +: + + + + + +int + + + + + += + + + + + +0 + + + + + + + + + + +reaction + + +( + + +startup + + +) + + +-> + + + out { + + += + + + + + + +// Sends a query + + + + self + + +-> + + +req + + += + + + + + +1 + + +; + + +// 1 is valid. 0 is invalid. + + + + lf_set(out, self + + +-> + + +req); + + + + + + += + + +} + + + + + + + + + + +reaction + + +( + + +in) { + + += + + + + + + +// Should not be invoked. + + + + self + + +-> + + +req + + += + + + + + +0 + + +; + + + + + + += + + +} + + + +} + + + + + + + +reactor + + + + + +Server + + + { + + + + + + +input + + + + + +in + + +: + + + + + +int + + + + + + +output + + + + + +out + + +: + + + + + +int + + + + + + +state + + + + + +error + + +: + + + + + +int + + + + + + +logical + + + + + +action + + + + + +err + + + + + + + + + + +reaction + + +( + + +in) + + +-> + + + out, err { + + += + + + + if (in + + +-> + + +value + + += + + += + + + + + +0 + + +) { + + + + lf_schedule(err, + + +0 + + +); + + + + } + + + + else { + + + + lf_set(out, in + + +-> + + +value); + + + + } + + + + + + += + + +} + + + + + + + + + + +reaction + + +( + + +err) { + + += + + + self + + +-> + + +error + + += + + + + + +1 + + +; + + += + + +} + + +// Error handling logic. + + + +} + + + + + + + +@ + + +property( + + + + name + + += + + + + + +" + + +success + + +" + + +, + + + + tactic + + += + + + + + +" + + +bmc + + +" + + +, + + + + spec + + += + + + + + +" + + +(F[0, 1 sec](SafeSend_c_reaction_1)) + + +" + + +, + + + + expect + + += + + + + + +true + + +) + + + +main + + + + + +reactor + + + { + + + + + + +c + + + + + += + + + + + +new + + + + + +Client + + +() + + + + + + +s + + + + + += + + + + + +new + + + + + +Server + + +() + + + + + + +c + + +. + + +out + + + + + +-> + + + + + +s + + +. + + +in + + + + + +after + + + + + +1 + + + + + +nsec + + + + + + +s + + +. + + +out + + + + + +-> + + + + + +c + + +. + + +in + + + +} + + + + + + diff --git a/test/known-good/C/src/verifier/Thermostat.html b/test/known-good/C/src/verifier/Thermostat.html new file mode 100644 index 000000000..13d1d62f7 --- /dev/null +++ b/test/known-good/C/src/verifier/Thermostat.html @@ -0,0 +1,1109 @@ + +/** + + + A thermostat model based on Lee & Seshia Chapter 3, Example 3.5. + + +*/ + + + +target + + + + + +C + + + + + + + +reactor + + + + + +Environment + + + { + + + + + + +input + + + + + +heatOn + + +: + + + + + +int + + + + + + +output + + + + + +temperature + + +: + + + + + +int + + + + + + +timer + + + t( + + +1 + + + + + +nsec + + +, + + +10 + + + + + +sec + + +) + + + + + + +state + + + + + +_heatOn + + +: + + + + + +int + + + + + + +state + + + + + +_temperature + + +: + + + + + +int + + + + + + + + + + +reaction + + +( + + +startup + + +) { + + += + + + self + + +-> + + +_temperature + + += + + + + + +19 + + +; + + += + + +} + + + + + + + + + + +reaction + + +( + + +t) + + +-> + + + temperature { + + += + + + + if (self + + +-> + + +_heatOn + + += + + += + + + + + +0 + + +) { + + + + self + + +-> + + +_temperature + + +- + + += + + + + + +1 + + +; + + + + } + + + + else { + + + + self + + +-> + + +_temperature + + ++ + + += + + + + + +1 + + +; + + + + } + + + + lf_set(temperature, self + + +-> + + +_temperature); + + + + + + += + + +} + + + + + + + + + + +reaction + + +( + + +heatOn) { + + += + + + self + + +-> + + +_heatOn + + += + + + heatOn + + +-> + + +value; + + += + + +} + + + +} + + + + + + + +reactor + + + + + +_Thermostat + + + { + + + + + + +input + + + + + +temperature + + +: + + + + + +int + + + + + + +output + + + + + +heatOn + + +: + + + + + +int + + + // + + +0 + + + + + += OFF, 1 = ON + + + + + + +state + + + + + +_mode + + +: + + + + + +int + + + // + + +0 + + + + + += + + + COOLING, + + +1 + + + + + += + + + HEATING + + + + + + +logical + + + + + +action + + + + + +changeMode + + + + + + + + + + +reaction + + +( + + +startup + + +) { + + += + + + self + + +-> + + +_mode + + += + + + + + +0 + + +; + + += + + +} + + + + + + + + + + +reaction + + +( + + +temperature) + + +-> + + + heatOn, changeMode { + + += + + + + if (self + + +-> + + +_mode + + += + + += + + + + + +0 + + +) { + + + + if (temperature + + +-> + + +value < + + += + + + + + +18 + + +) { + + + + lf_set(heatOn, + + +1 + + +); + + + + lf_schedule(changeMode, + + +0 + + +); + + + + } + + + + } + + + + else if (self + + +-> + + +_mode + + += + + += + + + + + +0 + + +) { + + + + if (temperature + + +-> + + +value > + + += + + + + + +22 + + +) { + + + + lf_set(heatOn, + + +0 + + +); + + + + lf_schedule(changeMode, + + +0 + + +); + + + + } + + + + } + + + + + + += + + +} + + + + + + + + + + +reaction + + +( + + +changeMode) { + + += + + + + if (self + + +-> + + +_mode + + += + + += + + + + + +0 + + +) + + + + self + + +-> + + +_mode + + += + + + + + +1 + + +; + + + + else + + + + self + + +-> + + +_mode + + += + + + + + +0 + + +; + + + + + + += + + +} + + + +} + + + + + + + +@ + + +property( + + + + name + + += + + + + + +" + + +correctness + + +" + + +, + + + + tactic + + += + + + + + +" + + +bmc + + +" + + +, + + + + spec + + += + + + + + +" + + +G[0, 20 sec](((Thermostat_t_temperature <= 18) ==> F[0](Thermostat_t__mode == 1)) && ((Thermostat_t_temperature >= 22) ==> F[0](Thermostat_t__mode == 0))) + + +" + + +, + + + + expect + + += + + + + + +true + + +) + + + +main + + + + + +reactor + + + { + + + + + + +e + + + + + += + + + + + +new + + + + + +Environment + + +() + + + + + + +t + + + + + += + + + + + +new + + + + + +_Thermostat + + +() + + + + + + +e + + +. + + +temperature + + + + + +-> + + + + + +t + + +. + + +temperature + + + + + + +t + + +. + + +heatOn + + + + + +-> + + + + + +e + + +. + + +heatOn + + + +} + + + + + + diff --git a/test/known-good/C/src/verifier/TrainDoor.html b/test/known-good/C/src/verifier/TrainDoor.html new file mode 100644 index 000000000..6add8d53d --- /dev/null +++ b/test/known-good/C/src/verifier/TrainDoor.html @@ -0,0 +1,654 @@ + +target + + + + + +C + + + + + + + +reactor + + + + + +Controller + + + { + + + + + + +output + + + + + +out1 + + +: + + + + + +int + + + + + + +output + + + + + +out2 + + +: + + + + + +int + + + + + + + + + + +reaction + + +( + + +startup + + +) + + +-> + + + out1, out2 { + + += + + + + lf_set(out1, + + +1 + + +); + + + + lf_set(out2, + + +2 + + +); + + + + + + += + + +} + + + +} + + + + + + + +reactor + + + + + +Train + + + { + + + + + + +input + + + + + +in + + +: + + + + + +int + + + + + + +state + + + + + +received + + +: + + + + + +int + + + + + + + + + + +reaction + + +( + + +in) { + + += + + + self + + +-> + + +received + + += + + + in + + +-> + + +value; + + += + + +} + + + +} + + + + + + + +reactor + + + + + +Door + + + { + + + + + + +input + + + + + +in + + +: + + + + + +int + + + + + + +state + + + + + +received + + +: + + + + + +int + + + + + + + + + + +reaction + + +( + + +in) { + + += + + + self + + +-> + + +received + + += + + + in + + +-> + + +value; + + += + + +} + + + +} + + + + + + + +@ + + +property( + + + + name + + += + + + + + +" + + +train_does_not_move_until_door_closes + + +" + + +, + + + + tactic + + += + + + + + +" + + +bmc + + +" + + +, + + + + spec + + += + + + + + +" + + +(!TrainDoor_t_reaction_0)U[0, 1 sec](TrainDoor_d_reaction_0) + + +" + + +, + + + + expect + + += + + + + + +false + + +) + + + +main + + + + + +reactor + + + { + + + + + + +c + + + + + += + + + + + +new + + + + + +Controller + + +() + + + + + + +t + + + + + += + + + + + +new + + + + + +Train + + +() + + + + + + +d + + + + + += + + + + + +new + + + + + +Door + + +() + + + + + + +c + + +. + + +out1 + + + + + +-> + + + + + +t + + +. + + +in + + + + + +after + + + + + +1 + + + + + +sec + + + + + + +c + + +. + + +out2 + + + + + +-> + + + + + +d + + +. + + +in + + + + + +after + + + + + +1 + + + + + +sec + + + +} + + + + + + diff --git a/test/known-good/C/src/verifier/UnsafeSend.html b/test/known-good/C/src/verifier/UnsafeSend.html new file mode 100644 index 000000000..87eadb209 --- /dev/null +++ b/test/known-good/C/src/verifier/UnsafeSend.html @@ -0,0 +1,820 @@ + +/** + + + + * (Original) Description: This example illustrates the "Verify Absence-of-Errors" mode. The server + + + + * expects a tuple `{REQUEST,PID-OF-SENDER}` but the main sends to it an atom instead of its pid, + + + + * then generating an exception when the server tries to send back a response to what he assumes to + + + + * be a pid. + + + + * + + + + * The verification step discovers a *genuine* counter-example. To inspect the error trace run bfc + + + + * on the generated model and look at the trace alongside the dot model of the ACS. + + + + + + +*/ + + + +target + + + + + +C + + + + + + + +reactor + + + + + +Client + + + { + + + + + + +input + + + + + +in + + +: + + + + + +int + + + + + + +output + + + + + +out + + +: + + + + + +int + + + + + + +state + + + + + +req + + +: + + + + + +int + + + + + += + + + + + +0 + + + + + + + + + + +reaction + + +( + + +startup + + +) + + +-> + + + out { + + += + + + + + + +// Sends a query + + + + self + + +-> + + +req + + += + + + + + +0 + + +; + + +// 1 is valid. 0 is invalid. + + + + lf_set(out, self + + +-> + + +req); + + + + + + += + + +} + + + + + + + + + + +reaction + + +( + + +in) { + + += + + + + + + +// Should not be invoked. + + + + self + + +-> + + +req + + += + + + + + +0 + + +; + + + + + + += + + +} + + + +} + + + + + + + +reactor + + + + + +Server + + + { + + + + + + +input + + + + + +in + + +: + + + + + +int + + + + + + +output + + + + + +out + + +: + + + + + +int + + + + + + +state + + + + + +error + + +: + + + + + +int + + + + + + +logical + + + + + +action + + + + + +err + + +( + + +1 + + + + + +nsec + + +) + + + + + + + + + + +reaction + + +( + + +in) + + +-> + + + out, err { + + += + + + + if (in + + +-> + + +value + + += + + += + + + + + +0 + + +) { + + + + lf_schedule(err, + + +0 + + +); + + + + } + + + + else { + + + + lf_set(out, in + + +-> + + +value); + + + + } + + + + + + += + + +} + + + + + + + + + + +reaction + + +( + + +err) { + + += + + + self + + +-> + + +error + + += + + + + + +1 + + +; + + += + + +} + + +// Error handling logic. + + + +} + + + + + + + +@ + + +property( + + + + name + + += + + + + + +" + + +success + + +" + + +, + + + + tactic + + += + + + + + +" + + +bmc + + +" + + +, + + + + spec + + += + + + + + +" + + +(F[0, 5 nsec](UnsafeSend_c_reaction_1)) + + +" + + +, + + + + expect + + += + + + + + +false + + +) + + + +main + + + + + +reactor + + + { + + + + + + +c + + + + + += + + + + + +new + + + + + +Client + + +() + + + + + + +s + + + + + += + + + + + +new + + + + + +Server + + +() + + + + + + +c + + +. + + +out + + + + + +-> + + + + + +s + + +. + + +in + + + + + +after + + + + + +2 + + + + + +nsec + + + + + + +s + + +. + + +out + + + + + +-> + + + + + +c + + +. + + +in + + + + + +after + + + + + +2 + + + + + +nsec + + + +} + + + + + + diff --git a/test/known-good/TypeScript/src/federated/failing/SpuriousDependency.html b/test/known-good/TypeScript/src/federated/failing/SpuriousDependency.html new file mode 100644 index 000000000..fd5721e3d --- /dev/null +++ b/test/known-good/TypeScript/src/federated/failing/SpuriousDependency.html @@ -0,0 +1,1096 @@ + +/** + + + + * This checks that a federated program does not deadlock when it is ambiguous, given the structure + + + + * of a federate, whether it is permissible to require certain network sender/receiver reactions to + + + + * precede others inp the execution of a given tag. The version of LFC that was inp the master branch + + + + * on 4/15/2023 resolved the ambiguity inp a way that does appear to result inp deadlock. + + + + + + +*/ + + + +target + + + + + +TypeScript + + + { + + + + timeout + + +: + + +1 + + + + + +sec + + + +} + + + + + + + +reactor + + + + + +Passthrough + + +(id: + + +number + + + + + += + + + + + +0 + + +) { + + + + + + +input + + + + + +inp + + +: + + + + + +number + + + + + + +output + + + + + +out + + +: + + + + + +number + + + + + + + + + + +reaction + + +(inp) + + +-> + + + out { + + += + + + + + + +//lf_print("Hello from passthrough %d", self->id); + + + + + + +console + + +. + + +log + + +( + + +" + + +Hello from passthrough + + +" + + + + + ++ + + + id); + + + + + + +//lf_set(out, inp->value); + + + + out + + += + + + inp; + + + + + + += + + +} + + + +} + + + + + + + +reactor + + + + + +Twisty + + + { + + + + + + +input + + + + + +in0 + + +: + + + + + +number + + + + + + +input + + + + + +in1 + + +: + + + + + +number + + + + + + +output + + + + + +out0 + + +: + + + + + +number + + + + + + +output + + + + + +out1 + + +: + + + + + +number + + + + + + +p0 + + + + + += + + + + + +new + + + + + +Passthrough + + +(id + + += + + +0 + + +) + + + + + + +p1 + + + + + += + + + + + +new + + + + + +Passthrough + + +(id + + += + + +1 + + +) + + + + in0 + + +-> + + + + + +p0 + + +. + + +inp + + + + + + +p0 + + +. + + +out + + + + + +-> + + + out0 + + + + in1 + + +-> + + + + + +p1 + + +. + + +inp + + + + + + +p1 + + +. + + +out + + + + + +-> + + + out1 + + + +} + + + + + + + +reactor + + + + + +Check + + + { + + + + + + +input + + + + + +inp + + +: + + + + + +number + + + + + + + + + + +state + + + + + +count + + +: + + + + + +number + + + + + += + + + + + +0 + + + + + + + + + + +reaction + + +(inp) { + + += + + + + + +console + + +. + + +log + + +( + + +" + + +count is now + + +" + + + + + ++ + + + + + ++ + + ++ + + +count); + + += + + +} + + + + + + + + + + +reaction + + +( + + +shutdown + + +) { + + += + + + + + + +// lf_print("******* Shutdown invoked."); + + + + + + +console + + +. + + +log + + +( + + +" + + +******* Shutdown invoked. + + +" + + +); + + + + + + +// if (self->count != 1) { + + + + + + +// lf_print_error_and_exit("Failed to receive expected input."); + + + + + + +// } + + + + if (count ! + + += + + + + + +1 + + +) { + + + + + + +util + + +. + + +reportError + + +( + + +" + + +Failed to receieve expected input. + + +" + + +); + + + + } + + + + + + += + + +} + + + +} + + + + + + + +federated + + + + + +reactor + + + { + + + + + + +t0 + + + + + += + + + + + +new + + + + + +Twisty + + +() + + + + + + +t1 + + + + + += + + + + + +new + + + + + +Twisty + + +() + + + + + + +check + + + + + += + + + + + +new + + + + + +Check + + +() + + + + + + +t0 + + +. + + +out1 + + + + + +-> + + + + + +t1 + + +. + + +in0 + + + + + + +t1 + + +. + + +out1 + + + + + +-> + + + + + +t0 + + +. + + +in0 + + + + + + +state + + + + + +count + + +: + + + + + +number + + + + + += + + + + + +0 + + + + + + + + + + +t1 + + +. + + +out0 + + + + + +-> + + + + + +check + + +. + + +inp + + + + + + + + + + +reaction + + +( + + +startup + + +) + + +-> + + + + + +t0 + + +. + + +in1 + + + { + + += + + + + + +t0 + + +. + + +in1 + + + + + += + + + + + +0 + + +; + + += + + +} + + + +} + + + + + +