Possible bug in containment algorithm (the default one)
Below is a proof that there exists a counterexample to the inclusion of planning_robotic_robustness_3600_A.bs.baccmin into planning_robotic_robustness_3600_B.bs. However, --included-in
with SPOT_CONTAINMENT_CHECK=default
returns that the inclusion holds.
On the other hand --included-in
with SPOT_CONTAINMENT_CHECK=forq
returns that the inclusion does not hold.
Unfortunately the Buchi automata are large and it takes SPOT (default) around one hour to return from the containment check.
I am using SPOT revision eff7966ce
.
Membership in the "small" language:
autfilt --accept-word='!l0 & l1 & !l2 & !l3 & !l4; !l0 & l1 & !l2 & !l3 & !l4; !l0 & l1 & !l2 & !l3 & !l4; !l0 & l1 & !l2 & !l3 & !l4; !l0
& l1 & !l2 & !l3 & !l4; !l0 & l1 & !l2 & !l3 & !l4; !l0 & !l1 & !l2 & !l3 & l4; !l0 & !l1 & !l2 & !l3 & l4; !l0 & !l1 & !l2 & !l3 & l4; !l0 & !l1 & !l2 & !l3 & l4; !l0 & !l1 & !l2 & !l3 & l4; !l0 & l1 & !l2 & !l3 & !l4; !l0 & l1 &
!l2 & !l3 & !l4; !l0 & !l1 & !l2 & !l3 & l4; !l0 & l1 & !l2 & !l3 & !l4; l0 & !l1 & !l2 & !l3 & l4; !l0 & !l1 & !l2 & !l3 & l4; !l0 & !l1 & !l2 & !l3 & l4; !l0 & !l1 & !l2 & !l3 & l4; !l0 & !l1 & !l2 & !l3 & l4; !l0 & l1 & !l2 & !l
3 & !l4; !l0 & l1 & !l2 & !l3 & !l4; !l0 & l1 & !l2 & !l3 & !l4; !l0 & l1 & !l2 & !l3 & !l4; !l0 & !l1 & !l2 & !l3 & l4; !l0 & l1 & !l2 & !l3 & !l4; !l0 & l1 & !l2 & !l3 & !l4; !l0 & !l1 & !l2 & !l3 & l4; !l0 & !l1 & !l2 & !l3 & l4
; !l0 & l1 & !l2 & !l3 & !l4; !l0 & l1 & !l2 & !l3 & !l4; !l0 & !l1 & !l2 & !l3 & l4; !l0 & !l1 & !l2 & !l3 & l4; !l0 & l1 & !l2 & !l3 & !l4; !l0 & !l1 & !l2 & !l3 & l4; !l0 & l1 & !l2 & !l3 & !l4; !l0 & !l1 & !l2 & !l3 & l4; !l0 &
l1 & !l2 & !l3 & !l4; !l0 & !l1 & !l2 & !l3 & l4; !l0 & !l1 & !l2 & !l3 & l4; !l0 & !l1 & !l2 & !l3 & l4; !l0 & !l1 & !l2 & !l3 & l4; !l0 & l1 & !l2 & !l3 & !l4; !l0 & l1 & !l2 & !l3 & !l4; !l0 & l1 & !l2 & !l3 & !l4; !l0 & l1 & !
l2 & !l3 & !l4; !l0 & !l1 & !l2 & !l3 & l4; !l0 & l1 & !l2 & !l3 & !l4; !l0 & l1 & !l2 & !l3 & !l4; !l0 & l1 & !l2 & !l3 & !l4; !l0 & l1 & !l2 & !l3 & !l4; !l0 & !l1 & !l2 & !l3 & l4; !l0 & !l1 & !l2 & !l3 & l4; !l0 & !l1 & !l2 & !
l3 & l4; !l0 & !l1 & !l2 & !l3 & l4; !l0 & l1 & !l2 & !l3 & !l4; !l0 & l1 & !l2 & !l3 & !l4; !l0 & !l1 & !l2 & !l3 & l4; !l0 & !l1 & !l2 & !l3 & l4; !l0 & !l1 & !l2 & !l3 & l4; !l0 & !l1 & !l2 & !l3 & l4; !l0 & !l1 & !l2 & !l3 & l4
; !l0 & l1 & !l2 & !l3 & !l4; !l0 & !l1 & !l2 & !l3 & l4; !l0 & l1 & !l2 & !l3 & !l4; !l0 & !l1 & !l2 & !l3 & l4; !l0 & l1 & !l2 & !l3 & !l4; !l0 & !l1 & !l2 & !l3 & l4; !l0 & l1 & !l2 & !l3 & !l4; !l0 & !l1 & !l2 & !l3 & l4; !l0 &
l1 & !l2 & !l3 & !l4; !l0 & !l1 & !l2 & !l3 & l4; !l0 & l1 & !l2 & !l3 & !l4; !l0 & l1 & !l2 & !l3 & !l4; !l0 & l1 & !l2 & !l3 & !l4; !l0 & !l1 & !l2 & !l3 & l4; !l0 & l1 & !l2 & !l3 & !l4; !l0 & !l1 & !l2 & !l3 & l4; !l0 & l1 & !
l2 & !l3 & !l4; !l0 & l1 & !l2 & !l3 & !l4; !l0 & l1 & !l2 & !l3 & !l4; !l0 & !l1 & !l2 & !l3 & l4; !l0 & !l1 & !l2 & !l3 & l4; !l0 & l1 & !l2 & !l3 & !l4; !l0 & l1 & !l2 & !l3 & !l4; !l0 & l1 & !l2 & !l3 & !l4; !l0 & !l1 & !l2 & !
l3 & l4; !l0 & l1 & !l2 & !l3 & !l4; !l0 & !l1 & !l2 & !l3 & l4; !l0 & !l1 & !l2 & !l3 & l4; !l0 & l1 & !l2 & !l3 & !l4; !l0 & !l1 & !l2 & !l3 & l4; !l0 & !l1 & !l2 & !l3 & l4; !l0 & l1 & !l2 & !l3 & !l4; !l0 & !l1 & !l2 & !l3 & l4
; !l0 & l1 & !l2 & !l3 & !l4; !l0 & l1 & !l2 & !l3 & !l4; !l0 & l1 & !l2 & !l3 & !l4; !l0 & l1 & !l2 & !l3 & !l4; !l0 & l1 & !l2 & !l3 & !l4; !l0 & !l1 & !l2 & !l3 & l4; !l0 & !l1 & !l2 & !l3 & l4; !l0 & !l1 & !l2 & !l3 & l4; !l0 &
l1 & !l2 & !l3 & !l4; !l0 & !l1 & !l2 & !l3 & l4; !l0 & l1 & !l2 & !l3 & !l4; !l0 & !l1 & !l2 & !l3 & l4; !l0 & l1 & !l2 & !l3 & !l4; !l0 & l1 & !l2 & !l3 & !l4; !l0 & !l1 & !l2 & !l3 & l4; !l0 & !l1 & !l2 & !l3 & l4; !l0 & l1 & !
l2 & !l3 & !l4; !l0 & !l1 & !l2 & l3 & !l4; cycle{!l0 & !l1 & l2 & !l3 & !l4; !l0 & !l1 & !l2 & !l3 & l4; !l0 & !l1 & !l2 & !l3 & l4; !l0 & !l1 & !l2 & !l3 & l4; !l0 & !l1 & !l2 & l3 & !l4; !l0 & l1 & !l2 & !l3 & !l4; !l0 & !l1 &
!l2 & l3 & !l4; !l0 & !l1 & !l2 & l3 & !l4 }' planning_robotic_robustness_3600_A.bs.baccmin -c
1
Non-membership in the "large" language:
autfilt --accept-word='!l0 & l1 & !l2 & !l3 & !l4; !l0 & l1 & !l2 & !l3 & !l4; !l0 & l1 & !l2 & !l3 & !l4; !l0 & l1 & !l2 & !l3 & !l4; !l0
& l1 & !l2 & !l3 & !l4; !l0 & l1 & !l2 & !l3 & !l4; !l0 & !l1 & !l2 & !l3 & l4; !l0 & !l1 & !l2 & !l3 & l4; !l0 & !l1 & !l2 & !l3 & l4; !l0 & !l1 & !l2 & !l3 & l4; !l0 & !l1 & !l2 & !l3 & l4; !l0 & l1 & !l2 & !l3 & !l4; !l0 & l1 &
!l2 & !l3 & !l4; !l0 & !l1 & !l2 & !l3 & l4; !l0 & l1 & !l2 & !l3 & !l4; l0 & !l1 & !l2 & !l3 & l4; !l0 & !l1 & !l2 & !l3 & l4; !l0 & !l1 & !l2 & !l3 & l4; !l0 & !l1 & !l2 & !l3 & l4; !l0 & !l1 & !l2 & !l3 & l4; !l0 & l1 & !l2 & !l
3 & !l4; !l0 & l1 & !l2 & !l3 & !l4; !l0 & l1 & !l2 & !l3 & !l4; !l0 & l1 & !l2 & !l3 & !l4; !l0 & !l1 & !l2 & !l3 & l4; !l0 & l1 & !l2 & !l3 & !l4; !l0 & l1 & !l2 & !l3 & !l4; !l0 & !l1 & !l2 & !l3 & l4; !l0 & !l1 & !l2 & !l3 & l4
; !l0 & l1 & !l2 & !l3 & !l4; !l0 & l1 & !l2 & !l3 & !l4; !l0 & !l1 & !l2 & !l3 & l4; !l0 & !l1 & !l2 & !l3 & l4; !l0 & l1 & !l2 & !l3 & !l4; !l0 & !l1 & !l2 & !l3 & l4; !l0 & l1 & !l2 & !l3 & !l4; !l0 & !l1 & !l2 & !l3 & l4; !l0 &
l1 & !l2 & !l3 & !l4; !l0 & !l1 & !l2 & !l3 & l4; !l0 & !l1 & !l2 & !l3 & l4; !l0 & !l1 & !l2 & !l3 & l4; !l0 & !l1 & !l2 & !l3 & l4; !l0 & l1 & !l2 & !l3 & !l4; !l0 & l1 & !l2 & !l3 & !l4; !l0 & l1 & !l2 & !l3 & !l4; !l0 & l1 & !
l2 & !l3 & !l4; !l0 & !l1 & !l2 & !l3 & l4; !l0 & l1 & !l2 & !l3 & !l4; !l0 & l1 & !l2 & !l3 & !l4; !l0 & l1 & !l2 & !l3 & !l4; !l0 & l1 & !l2 & !l3 & !l4; !l0 & !l1 & !l2 & !l3 & l4; !l0 & !l1 & !l2 & !l3 & l4; !l0 & !l1 & !l2 & !
l3 & l4; !l0 & !l1 & !l2 & !l3 & l4; !l0 & l1 & !l2 & !l3 & !l4; !l0 & l1 & !l2 & !l3 & !l4; !l0 & !l1 & !l2 & !l3 & l4; !l0 & !l1 & !l2 & !l3 & l4; !l0 & !l1 & !l2 & !l3 & l4; !l0 & !l1 & !l2 & !l3 & l4; !l0 & !l1 & !l2 & !l3 & l4
; !l0 & l1 & !l2 & !l3 & !l4; !l0 & !l1 & !l2 & !l3 & l4; !l0 & l1 & !l2 & !l3 & !l4; !l0 & !l1 & !l2 & !l3 & l4; !l0 & l1 & !l2 & !l3 & !l4; !l0 & !l1 & !l2 & !l3 & l4; !l0 & l1 & !l2 & !l3 & !l4; !l0 & !l1 & !l2 & !l3 & l4; !l0 &
l1 & !l2 & !l3 & !l4; !l0 & !l1 & !l2 & !l3 & l4; !l0 & l1 & !l2 & !l3 & !l4; !l0 & l1 & !l2 & !l3 & !l4; !l0 & l1 & !l2 & !l3 & !l4; !l0 & !l1 & !l2 & !l3 & l4; !l0 & l1 & !l2 & !l3 & !l4; !l0 & !l1 & !l2 & !l3 & l4; !l0 & l1 & !
l2 & !l3 & !l4; !l0 & l1 & !l2 & !l3 & !l4; !l0 & l1 & !l2 & !l3 & !l4; !l0 & !l1 & !l2 & !l3 & l4; !l0 & !l1 & !l2 & !l3 & l4; !l0 & l1 & !l2 & !l3 & !l4; !l0 & l1 & !l2 & !l3 & !l4; !l0 & l1 & !l2 & !l3 & !l4; !l0 & !l1 & !l2 & !
l3 & l4; !l0 & l1 & !l2 & !l3 & !l4; !l0 & !l1 & !l2 & !l3 & l4; !l0 & !l1 & !l2 & !l3 & l4; !l0 & l1 & !l2 & !l3 & !l4; !l0 & !l1 & !l2 & !l3 & l4; !l0 & !l1 & !l2 & !l3 & l4; !l0 & l1 & !l2 & !l3 & !l4; !l0 & !l1 & !l2 & !l3 & l4
; !l0 & l1 & !l2 & !l3 & !l4; !l0 & l1 & !l2 & !l3 & !l4; !l0 & l1 & !l2 & !l3 & !l4; !l0 & l1 & !l2 & !l3 & !l4; !l0 & l1 & !l2 & !l3 & !l4; !l0 & !l1 & !l2 & !l3 & l4; !l0 & !l1 & !l2 & !l3 & l4; !l0 & !l1 & !l2 & !l3 & l4; !l0 &
l1 & !l2 & !l3 & !l4; !l0 & !l1 & !l2 & !l3 & l4; !l0 & l1 & !l2 & !l3 & !l4; !l0 & !l1 & !l2 & !l3 & l4; !l0 & l1 & !l2 & !l3 & !l4; !l0 & l1 & !l2 & !l3 & !l4; !l0 & !l1 & !l2 & !l3 & l4; !l0 & !l1 & !l2 & !l3 & l4; !l0 & l1 & !
l2 & !l3 & !l4; !l0 & !l1 & !l2 & l3 & !l4; cycle{!l0 & !l1 & l2 & !l3 & !l4; !l0 & !l1 & !l2 & !l3 & l4; !l0 & !l1 & !l2 & !l3 & l4; !l0 & !l1 & !l2 & !l3 & l4; !l0 & !l1 & !l2 & l3 & !l4; !l0 & l1 & !l2 & !l3 & !l4; !l0 & !l1 &
!l2 & l3 & !l4; !l0 & !l1 & !l2 & l3 & !l4 }' planning_robotic_robustness_3600_B.bs -c
0
SPOT says inclusion holds:
SPOT_CONTAINMENT_CHECK=default autfilt planning_robotic_robustness_3600_A.bs.baccmin --included-in=planning_robotic_robustness_3600_B.bs -c
1