runtime verification test failure: test case 273 of scenario normal_4

[kiniry]

On my system, this test run takes nearly three hours to get to this case if you are running the whole suite.

scenarios/normal_4 (../src/rts.no_self_test)
Opening scenarios/normal_4.cases...
Running case 0
...
Running case 271
Running case 272
Test 273 failed
Traceback (most recent call last):
  File "/HARDENS/tests/./run_all.py", line 35, in <module>
    subprocess.run(["./test.py", fn, fn + ".cases"],check=True)
  File "/usr/lib/python3.9/subprocess.py", line 528, in run
    raise CalledProcessError(retcode, process.args,
subprocess.CalledProcessError: Command '['./test.py', 'scenarios/normal_4', 'scenarios/normal_4.cases']' returned non-zero exit status 1.
make: *** [Makefile:12: test] Error 1

[kiniry]

Interesting enough, test 273 also fails for scenario 5a.

[podhrmic]

scenario 273 for normal_4 is incorrect - here is my annotated sequence

Scenario 272

Running case 272
SENDING: 
CHECKING: #A 0 \[0 0\]
CHECKING: #A 0 \[0 0\] succeeded
CHECKING: #A 1 \[0 0\]
CHECKING: #A 1 \[0 0\] succeeded
SENDING: 
SENDING: B 0 0 0
SENDING: B 1 0 0
SENDING: B 2 0 0
SENDING: B 3 0 2
SENDING: B 0 1 0
SENDING: B 1 1 0
SENDING: B 2 1 0 // last cmd identical for 272 and 273
// division 3 setpoint for channel 1 is bypass
SENDING: B 3 1 0 
// division 0, setpoint for channel 2 is trip
SENDING: B 0 2 2
// division 1, setpoint for channel 2 is trip
SENDING: B 1 2 2
// division 2, setpoint for channel 2 is trip
SENDING: B 2 2 2
// division 3, setpoint for channel 2 is trip
SENDING: B 3 2 2
SENDING: 
CHECKING: #A 0 \[0 1\]
CHECKING: #A 0 \[0 1\] succeeded
CHECKING: #A 1 \[0 1\]
CHECKING: #A 1 \[0 1\] succeeded

Scenario 273

Running case 273
SENDING: 
CHECKING: #A 0 \[0 0\]
CHECKING: #A 0 \[0 0\] succeeded
CHECKING: #A 1 \[0 0\]
CHECKING: #A 1 \[0 0\] succeeded
SENDING: 
SENDING: B 0 0 0
SENDING: B 1 0 0
SENDING: B 2 0 0
SENDING: B 3 0 2
SENDING: B 0 1 0
SENDING: B 1 1 0
SENDING: B 2 1 0
SENDING: B 3 1 2 // this one is different
// division 0 setpoint for channel 2 is bypass
SENDING: B 0 2 0
// division 1, setpoint for channel 2 is bypass
SENDING: B 1 2 0
// division 2, setpoint for channel 2 is bypass
SENDING: B 2 2 0
// division 3, setpoint for channel 2 is bypass
SENDING: B 3 2 0
SENDING: 
CHECKING: #A 0 \[1 0\]
CHECKING: #A 0 \[1 0\] failed

It fails because the expected result is a tripped actuator, but we don't have enough tripped channels for that to happen

[podhrmic]

I am not quite sure how Alex generated all the cases, but there are 4096 cases for each scenario - @kiniry is it even practical to run all those cases? Wouldn't it be better to use symbolic checking rather than running so many tests?

EDIT: For scenario_4 the cases after 273 seem to have a similar bug, scnario_5a appear to have the same problem - i.e. not enough instrumentation trips to trigger the actuator to engage.