Task #6061
closed
EFSM-based transition assertion generator
Added by Sergey Smolov almost 9 years ago.
Updated over 6 years ago.
Category:
Engine (Extractor)
Description
For the every (state, guard) pair (where state is an EFSM state constraint and guard is a guard of EFSM transition started from state) returns "!(state && guard)" constraint and prints it to the SMV format.
- Status changed from New to Open
- % Done changed from 0 to 30
Add assertion representation to r2403
- % Done changed from 30 to 60
Add efsm-based transition assertion generator engine (r2407).
- % Done changed from 60 to 80
Add SMV printer stub (everything exception printing) for assertion entity in r2357.
- Status changed from Open to Resolved
- % Done changed from 80 to 100
The rest of the functionality is moved to HlddSmvPrinter.
- Status changed from Resolved to Closed
- Published in build set to 0.2.1
- Target version changed from 2.0 to 1.0
Also available in: Atom
PDF