search

luisandresilva / reprotool

Automatically exported from code.google.com/p/reprotool
0 stars 0 forks source link

Check CTL using SMV #61

Closed GoogleCodeExporter closed 8 years ago

GoogleCodeExporter commented 8 years ago 
What steps will reproduce the problem?
1. Convert project to Nusmv
2. Check CTL using SMV
3. Error is printed in console:

file C:\Documents and 
Settings\jvinarek\runtime-EclipseApplication\zzz\project.swproj.nusmv: line 67: 
"xTest_use_case.null" undefined
Executing NuSMV command: check_ctlspec -o counterexample.xml
A model must be read before. Use the "read_model" command.

Original issue reported on code.google.com by jiri.vin...@gmail.com on 17 Nov 2011 at 11:15

Attachments:

GoogleCodeExporter commented 8 years ago 
There seem to be the following problems (try my attached project file and 
generated nusmv file):

1. CTL specification cannot be checked because NuSMV code for "use" annotations 
has not been generated. The verification fails with message such as "ERROR: 
Property "A [ !use_zoom U (create_zoom | !(AF use_zoom)) ]  " is not correct 
or not well typed".
The generator should have created a code such as:

  VAR use_zoom : boolean ;
  INIT use_zoom in FALSE
  ASSIGN next ( use_zoom ) := FALSE
    | xGenerate_city.s in { ... some states ... }
    ... ;

2. There is a problem in the generated steps of a use-case state machine. See 
"MODULE UC_Generate_restaurant_map_for_city". There is a state "s1__" for which 
no transition is specified. Error message: "line 115: case conditions are not 
exhaustive".
I was able to fix the error manually by adding "s=s1__ : s1_".

Original comment by viliam.s...@gmail.com on 14 Dec 2011 at 10:22

Attachments:

GoogleCodeExporter commented 8 years ago

Original comment by viliam.s...@gmail.com on 14 Dec 2011 at 11:16

GoogleCodeExporter commented 8 years ago 
The issue has been fixed

Original comment by rud...@gmail.com on 6 Jan 2012 at 1:21