-never { /* []<>e->[](d-><>r) */
-
+never { /* !([]<>p->[](q-><>r)) */
T0_init:
if
- :: (!d) || (r) -> goto accept_S1
- :: (1) -> goto T1_S4
- :: (1) -> goto T0_S2
- :: (!e) -> goto accept_S3
+ :: (1) -> goto T0_init
+ :: (!r && q) -> goto T1_S4
fi;
T1_S4:
if
- :: (1) -> goto T1_S4
- :: (r) -> goto accept_S1
+ :: (!r) -> goto T1_S4
+ :: (!r && p) -> goto accept_S4
fi;
-accept_S1:
+accept_S4:
if
- :: (!d) || (r) -> goto accept_S1
- :: (1) -> goto T1_S4
- fi;
-T0_S2:
- if
- :: (1) -> goto T0_S2
- :: (!e) -> goto accept_S3
- fi;
-accept_S3:
- if
- :: (!e) -> goto accept_S3
+ :: (!r) -> goto T1_S4
+ :: (!r && p) -> goto accept_S4
fi;
}