[Analyses] Translation to NuSMV does not preserve non-determinism for weakly causal components
Concrete use case where it entails a failing behaviour:
Step-by-step:
- open the attached model
- open the “A/G, Contracts, Patterns” element of the Component “Component”
- check the only specification atom
Expected: FAILURE (indeed, there are two transitions in the component, one potentially leading to the case “Output == Input”, therrefore this case is NOT globally false)
Actual result: SUCCESS
—>the successful transition is not taken into account
Heart of the problem: transitions for strongly causal components are translated into a NEXT-expression which enforces a priority on the non-deterministic execution.
(from redmine: issue id 2124, created on 2014-09-05, closed on 2016-11-07)
- Relations:
- parent #2689 (closed)
- Uploads: