In file "formal-methods-workbench\models\regression_tests\agree\models\OM1\OM1.aadl"
and file "formal-methods-workbench\models\agree\OM1\OM1.aadl"
line 111 reads "not_faulty_event_input exclusively occurs during [OM1.relay_low, OM1.relay_high];".
I believe it should read "output2_event exclusively occurs during [OM1.relay_low, OM1.relay_high];".
This model seems to be the only model using RSL patterns in the repo. Unfortunately, after correcting the error, I cannot complete the proof anymore. It stuck at checking component "patterns 1 in bound".
In file "formal-methods-workbench\models\regression_tests\agree\models\OM1\OM1.aadl" and file "formal-methods-workbench\models\agree\OM1\OM1.aadl"
line 111 reads "not_faulty_event_input exclusively occurs during [OM1.relay_low, OM1.relay_high];". I believe it should read "output2_event exclusively occurs during [OM1.relay_low, OM1.relay_high];".
This model seems to be the only model using RSL patterns in the repo. Unfortunately, after correcting the error, I cannot complete the proof anymore. It stuck at checking component "patterns 1 in bound".