Bug #764

Feature #849: Model checking extensions for AF3 2.1

Can DataStateVariables inside an automaton be NoVal?

Added by Anonymous over 8 years ago. Updated almost 8 years ago.

Target version:
Start date:
Due date:
% Done:


Estimated time:
(Total: 0.00 h)


- in the simulator this is allowed (a local variable to a state automaton can be NoVal)
- in the C, Yices, NuSMV code generators this is not allowed

I think that this is a more fundamental discussion ... in my opinion the NoVal makes sense for streams and not for data-state-variables

patch.txt (4.87 KB) patch.txt Florian Hölzl, 04/07/2012 10:03 AM


Bug #760: Non determinism Analysis - Unknown Runtime Error :-(Closed


#1 Updated by Florian Hölzl over 8 years ago

DSVs are value-only, so NoVal is NOT allowed.

Constraint checkers do not protect against this yet.
The attached patch alters the relevant part of the code without implementing it fully (for Guards, Actions, and DSvs there will be errors).

#2 Updated by Anonymous over 8 years ago

  • Status changed from New to In Progress
  • Assignee changed from Anonymous to Florian Hölzl

I've applied the patch ... the constraints checker now checks the inappropriate use of the NoVal constant

- the simulator should be extended to raise a RuntimeException when NoVal is assigned to a data-state-variable.
- the code is in class TypeCheckConstraintCheckerBase - please review

#3 Updated by Florian Hölzl over 8 years ago

  • Status changed from In Progress to Resolved
  • Assignee changed from Florian Hölzl to Anonymous

Action "dsv=NoVal" was not recognized by the checker. It does so now.

Runtime exception is raised if simulator assigns NoVal to a data state variable.

Code was reviewed. Bug can be closed.

#4 Updated by Anonymous over 8 years ago

  • Status changed from Resolved to Closed

#5 Updated by Anonymous almost 8 years ago

  • Parent task set to #849

Also available in: Atom PDF