Feature #849: Model checking extensions for AF3 2.1
Can DataStateVariables inside an automaton be NoVal?
- 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
#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.