ModelCheckerEquivalenceTest test[11] fails, but simulator is correct w.r.t. model semantics
I tracked the following test failure:
java.lang.AssertionError: Error with step 2 in component TL-Architecture
of project: SimpleTrafficLightsExample expected:<On( )>but
was:<Off( )>
at org.junit.Assert.fail(Assert.java:91)
at org.junit.Assert.failNotEquals(Assert.java:645)
at org.junit.Assert.assertEquals(Assert.java:126)
at
test.org.fortiss.af3.rcapplication.semantic.alignment.nusmv.ModelCheckerEquivalenceTest.testSemanticsAlignment(ModelCheckerEquivalenceTest.java:137)
with some Sysouts in TestCaseSimulator (out comparison is simulator=MC expected value).
Step 2 fails because simulator takes transition with input NoVal
(resulting in indicator OFF), while
MC seems to take transition with input Present() (resulting in indicator
ON). However, the underlying
model’s initial transition states, that simulator is correct (since
input is NoVal until step 3 in the trace below).
TEST CASE null
Step 0:
>>>>>>INPUTS >>>>>>>
NoVal;
<<<<<< OUTPUTS <<<<<<<<<
NoVal = NoVal;
NoVal = NoVal;
NoVal = NoVal;
NoVal = NoVal;
Step 1:
>>>>>>INPUTS >>>>>>>
NoVal;
<<<<<< OUTPUTS <<<<<<<<<
Green( ) = Green( );
Stop( ) = Stop( );
Off( ) = On( );Halt:
Off( ) = On( );Halt:
Step 2:
>>>>>>INPUTS >>>>>>>
NoVal;
<<<<<< OUTPUTS <<<<<<<<<
NoVal = NoVal;
NoVal = NoVal;
NoVal = NoVal;
NoVal = NoVal;
Step 3:
>>>>>>INPUTS >>>>>>>
Present();
<<<<<< OUTPUTS <<<<<<<<<
NoVal = NoVal;
NoVal = NoVal;
NoVal = NoVal;
NoVal = NoVal;
Step 4:
>>>>>>INPUTS >>>>>>>
Present();
<<<<<< OUTPUTS <<<<<<<<<
Green( ) = Yellow( );Halt:
Stop( ) = Stop( );
On( ) = On( );
On( ) = On( );
Step 5:
>>>>>>INPUTS >>>>>>>
Present();
<<<<<< OUTPUTS <<<<<<<<<
NoVal = NoVal;
NoVal = NoVal;
NoVal = NoVal;
NoVal = NoVal;
Step 6:
>>>>>>INPUTS >>>>>>>
NoVal;
<<<<<< OUTPUTS <<<<<<<<<
NoVal = Red( );Halt:
NoVal = Walk( );
(from redmine: issue id 1708, created on 2013-09-13, closed on 2020-03-09)