Animation breaking the draw screen
Florencia Zanollo created an issue 2025-05-20
Steps to reproduce:
Have a specification that has several LTSs
for example:
const N = 2 const K = 3
const Teams = N const Steps = K
range Team = 0..(Teams-1) range Step = 1..Steps
/*****************************************************************************/
Crew(Tid=0) = Pending, Pending = ( {approve,refuse} -> ERROR | assign[Tid] -> Assigned[1] ), Assigned[s:Step] = ( reject[Tid][s] -> Rejected[s] | accept[Tid] -> Accepted ), Rejected[s:Step] = ( refuse -> Pending | approve -> ERROR | assign[Tid] -> if (s < Steps) then Assigned[s+1] else ERROR ), Accepted = ( {approve,refuse} -> Pending | assign[Tid] -> ERROR ).
Document = Count[0], Count[c:0..Teams-1] = ( reject[Team][Steps] -> Rejected | accept[Team] -> Count[c+1] | approve -> ERROR | refuse -> if (c==0) then Document else ERROR ), Count[Teams] = ( {accept[Team],reject[Team][Steps]} -> Count[Teams] | approve -> Document | refuse -> ERROR ), Rejected = ( {accept[Team],reject[Team][Steps]} -> Rejected | approve -> ERROR | refuse -> Document ).
/*****************************************************************************/
||Plant = (Document || forall [t:Team] Crew(t)).
set Alphabet = {approve, refuse, assign[t:Team], accept[t:Team], reject[t:Team][s:Step]} fluent F = <{refuse, approve}, Alphabet{refuse, approve}> assert A = F controllerSpec Goal = { controllable = {assign[Team], refuse, approve} liveness = {A} } assert Check = ([]<>A)
Compose plant
button that’s like ||
Options → Multiple LTSs…
Draw multiple, everything works fine, draws the Plant and everything. Hide the Plant LTS
Animate (A button), play around, close animation
The Plant does not show anymore, it might even break the other LTSs, leaving them with some transition in red like the animation is still running