search

luisandresilva / reprotool

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

Show description of the formula in the counterexample editor #75

Closed GoogleCodeExporter closed 8 years ago

GoogleCodeExporter commented 8 years ago 
What steps will reproduce the problem?
1. Create a project containing some violation of a temporal propety e.g. a 
single step with #use:item annotation
2. Generate SMV code from the project
3. Run "Check CTL using NuSMV"
4. Open the generated counterexample (*.cexmp) file
5. The root element of the tree will be "Counter Example A[ !use_item U 
create_item | !AF(use_item)])"

What is the expected output?
There should be something like:
  "Counter Example: No 'use' before 'create' = A[ !use_item U create_item | !AF(use_item)])"

As you can see, you just have to prepend the description of the formula.

Original issue reported on code.google.com by viliam.s...@gmail.com on 18 Dec 2011 at 8:03

GoogleCodeExporter commented 8 years ago 
I have fixed it

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