Project

General

Profile

Bug #2123

[Analyses] Counter-example coming from NuSMV does not fill in all the values

Added by Anonymous about 6 years ago. Updated over 5 years ago.

Status:
Closed
Priority:
Normal
Assignee:
-
Category:
-
Start date:
09/04/2014
Due date:
% Done:

100%

Estimated time:

Description

To reproduce:
- open the attached model
- go to the "A/G Contracts Patterns" part of "Component0"
- check the only specification atom ("Check Selected")
- in the counter-example view which just got filled in, click on the button "Open Simulator"
- in the simulator, open Component1
- run one step of the simulation

Expected:
- the left channel (from Component1.Input to Component2.Input) should get the value "2"

What actually happens:
- the left channel (from Component1.Input to Component2.Input) gets "NoVal"

Remark:
- By observing Component0 instead of Component1 during the simulation, one can see how the input indeed gets "2".
- This can be observed even more directly by looking at the counter-example in the Counter-example view

So the problem is that some values are set to NoVal when they actually have a value.
However NuSMV does not provide directly this value so a lil bit more work than just parsing has to be achieved.

Issue.af3_23 (16.4 KB) Issue.af3_23 Anonymous, 09/04/2014 05:50 PM

Related issues

Related to Bug #2071: Simulation out of MSC Conformity Check shows not expected thingsClosed07/28/2014

History

#1 Updated by Anonymous over 5 years ago

  • Status changed from New to Resolved
  • Assignee changed from Anonymous to Andreas Bayha
  • % Done changed from 0 to 100

Resolved.

At least for channels. Might be some other situations where similar problems happen though.
An ideal solution would be to rethink the way components' behaviour is implemented, but ok for now.

#2 Updated by Anonymous over 5 years ago

  • Related to Bug #2071: Simulation out of MSC Conformity Check shows not expected things added

#3 Updated by Andreas Bayha over 5 years ago

  • Status changed from Resolved to Closed
  • Assignee deleted (Andreas Bayha)

Expected bahaviour can now be observed.

Closed...

Also available in: Atom PDF