Currently a condition has a setInvariant and isInvariant method that are legacy of a simpler timer when the engine only supported reachability.
These methods should be removed and the reachability engine should be extended to support the "EF" and "AG" propositions directly.
This will also require a minor change in the advanced pre-verification pipeline of the CTL-engine.
Currently a condition has a
setInvariantandisInvariantmethod that are legacy of a simpler timer when the engine only supported reachability.These methods should be removed and the reachability engine should be extended to support the "EF" and "AG" propositions directly.
This will also require a minor change in the advanced pre-verification pipeline of the CTL-engine.