# A STGA model is ready with 5 node(s) and 8 edge(s).
# 1 constraint(s) is/are concerned.
# Slice w.r.t constraint no.0: _E[_true _U <a?x[x >= 3]> _E[_true _U <ok!p[p = 2]> _true]] 
A test sequence (0->1) is ready with a constraint .
A test sequence (0->1,1->2) is ready with a constraint .
A test sequence (0->1,1->2,2->3) is ready with a constraint _2x >= 0.
A test sequence (0->1,1->2,2->3,3->1) is ready with a constraint _2x >= 0 && _3y < 0.
A test sequence (0->1,1->2,2->3,3->1) is ready with a constraint _2x >= 0 && _3y >= 0 && _3y - _2x <= 2 && _2x - _3y <= 2.
A test sequence (0->1,1->2,2->3,3->1) is ready with a constraint _2x >= 0 && _3y >= 0 && _3y - _2x > 2 || _2x - _3y > 2.
A test sequence (0->1,1->2,2->1) is ready with a constraint _2x < 0.
# 7 test sequences created in 0.s.