search

favu100 / b2program

READ-ONLY MIRROR of https://gitlab.cs.uni-duesseldorf.de/general/stups/b2program; DO NOT PUSH
5 stars 3 forks source link

Fix invariant violation error in ExplicitChecks #16

Closed leuschel closed 2 years ago

leuschel commented 2 years ago

make ExplicitChecks LANGUAGE=java DIRECTORY=benchmarks/model_checking/ProB/Other java -jar B2Program-all-0.1.0-SNAPSHOT.jar -l java -mc true -f benchmarks/model_checking/ProB/Other/ExplicitChecks.mch cp benchmarks/model_checking/ProB/Other/*.java . javac -cp .:btypes.jar ExplicitChecks.java java -cp .:btypes.jar ExplicitChecks mixed 1 false INVARIANT VIOLATED COUNTER EXAMPLE TRACE:

_get_x: 0 Number of States: 2 Number of Transitions: 2

favu100 commented 2 years ago

& // REPL Unit Tests ( (%x.(x : 1 .. 9000|{x + 1}) \/ {0 |-> {0}} ; %y.(y <: {0,3}|y) \/ {{0} |-> {0}}) = {(0|->{0}),(2|->{3})} ) / 15/10/2011 9:20 /

This seems to be the conjunct that causes the problem

favu100 commented 2 years ago

This problem also occurs for C++

favu100 commented 2 years ago

Checking equaility of BRelation seems to be wrong

favu100 commented 2 years ago

This issue is solved now. It was caused by a wrong implementation of composition. In particular, the problem occurs when the relational image on a singleton set of a domain element is the empty set. The internal representation maps to the empty set due to performance reason. This means that the implementation of the equal operator differs from the equality of the underlying PersistentHashMap data structure

Nevertheless, the model's invariant is too complicated so that model checking finishes in reasonable time