imitator icon indicating copy to clipboard operation
imitator copied to clipboard

-merge should automatically enable -comparison=inclusion

Open jacopol opened this issue 3 years ago • 0 comments

The "merging" code assumes that the inclusion code is enabled. So during option parsing, -merge should trigger -comparison=inclusion. Currently, -merge gives a wrong result on the following specification, while -merge -comparison=inclusion gives the correct result. (this model is also known as "interesting2.imi")

var x,y: clock; p,q: parameter;

automaton P loc s0: invariant True when x<=p & y<=p goto s1; when x<=p & y>=p goto s1; loc s1: invariant x<=p when x>=q do { x := 0 } goto s1; end

init := loc[P]=s0 & x>=0 & y>=0 & p>=0 & q>=0;

jacopol avatar Feb 26 '22 09:02 jacopol