# A STGA model is ready with 4 node(s) and 6 edge(s).
# 1 constraint(s) is/are concerned.
# Slice w.r.t constraint no.0: _A _G[<deposit?x[]> _A _G[{deposit?x[]} _true]] 
A test sequence (0->1) is ready with a constraint .
A test sequence (0->1,1->3) is ready with a constraint .
A test sequence (0->1,1->3,3->1) is ready with a constraint .
# 3 test sequences created in 0.s.