To give some help and instructions how to use the tool, consider the following: Given formulas S1=[a WB [c WB b]] and S2=[a WB [c SB b]], we first check whether the one implies the other one.
The tool quickly tells us that [a WB [c WB b]] -> [a WB [c SB b]] is valid, while we get a counterexample for [a WB [c SB b]] -> [a WB [c WB b]]. That counterexample consists of an infinite path where G(!a&!b&!c) holds. Hence, we know that
- G(!a&!b&!c) -> [a WB [c SB b]]
- G(!a&!b&!c) -> ![a WB [c WB b]]
which is also easily seen with the semantics of the WB and SB operators. Hence, we already have a first formula to distinguish between the two formulas. To find a second one, we ask the tool whether this is the only counterexample in that we let the tool check the following
!G(!a&!b&!c) -> ([a WB [c SB b]] -> [a WB [c WB b]])
A counterexamle would satisfy !G(!a&!b&!c) & [a WB [c SB b]] & ![a WB [c WB b]]. The tools gives a counterexample which is an infinite path where G(a&!b&!c) holds. So, we have a second counterexample.
If you want a third one, you may ask now
!G(!a&!b&!c) & !G(a&!b&!c) -> ([a WB [c SB b]] -> [a WB [c WB b]])
This time, we get a counterexample with two alternating states which may be described with the following LTL formula:
(!a&!b&!c) & G( ((!a&!b&!c) -> X(a&!b&!c)) & ((a&!b&!c) -> X(!a&!b&!c)))
This way, you can construct many counterexamples or models that satisfy a formula like !S1&S2.
