Interactive simulation shows unexecutable choices

[LauraPanizo]

I modeled a simple coffe machine and I have notice a weird behaviour in the interactive simulation when using the following code

active proctype coffemachine(){
int estado = 0; //off
inicio:
if
:: estado == 0 -> estado = 1; //idle
:: estado == 1 -> estado = 0; //off
:: estado == 1 -> estado = 2; //making coffe
:: estado == 2 -> estado = 3; /serving coffe
:: estado == 3 -> estado = 1; //idle
fi;
goto inicio;

}

In the first decision point, the interactive simulator shows that estado is 1 and gives me three possible options (estado==0, estado ==1, estado==1), but the first option is not executable. Similarly, if I make select different options at some points when estado is 1 and gives me 4 options to choose (estado ==1, estado==1, estado==2 and estado ==3), the last two are not executable.
I have always believe that interactive simulation let us choose between the executable options and hides the non-excutables.
Could you confirm that it is a bug?

Best regards,
Laura

[nimble-code]

Hi Laura -- yes, this is not ideal and could be improved. Thanks for reporting it. -g

…

On Tue, Sep 16, 2025 at 6:35 AM Laura Panizo Jaime ***@***.***> wrote: *LauraPanizo* created an issue (nimble-code/Spin#84) <#84> I modeled a simple coffe machine and I have notice a weird behaviour in the interactive simulation when using the following code active proctype coffemachine(){ int estado = 0; //off inicio: if :: estado == 0 -> estado = 1; //idle :: estado == 1 -> estado = 0; //off :: estado == 1 -> estado = 2; //making coffe :: estado == 2 -> estado = 3; /serving coffe :: estado == 3 -> estado = 1; //idle fi; goto inicio; } In the first decision point, the interactive simulator shows that estado is 1 and gives me three possible options (estado==0, estado ==1, estado==1), but the first option is not executable. Similarly, if I make select different options at some points when estado is 1 and gives me 4 options to choose (estado ==1, estado==1, estado==2 and estado ==3), the last two are not executable. I have always believe that interactive simulation let us choose between the executable options and hides the non-excutables. Could you confirm that it is a bug? Best regards, Laura — Reply to this email directly, view it on GitHub <#84>, or unsubscribe <https://github.com/notifications/unsubscribe-auth/AK6L6IP5UNFYEPJTAAGHWN33TAGZHAVCNFSM6AAAAACGU3OWGGVHI2DSMVQWIX3LMV43ASLTON2WKOZTGQZDEMZTHA3DMNA> . You are receiving this because you are subscribed to this thread.Message ID: ***@***.***>

[LauraPanizo]

Dear G.,
Thank you for your reply. I am almost sure that in previous versions of SPIN the interactive simulator worked correctly. I have a new example in which the list of choices is even stranger.
The following code is modeling a vending machine with two kind of products. If we guide the simulation to a state in which there is no products, at some point the simulator behaves as shown in the screenshot, in which the list of choices in the idle if returns the option else. In addition, if this third option is selected, the simulator prints "timeout".

vending_machine.txt

BR,
Laura

[nimble-code]

you can find earlier versions of Spin at: https://spinroot.com/spin/Archive/

…

On Wed, Sep 17, 2025 at 9:38 AM Laura Panizo Jaime ***@***.***> wrote: *LauraPanizo* left a comment (nimble-code/Spin#84) <#84 (comment)> Dear G., Thank you for your reply. I am almost sure that in previous versions of SPIN the interactive simulator worked correctly. I have a new example in which the list of choices is even stranger. The following code is modeling a vending machine with two kind of products. If we guide the simulation to a state in which there is no products, at some point the simulator behaves as shown in the screenshot, in which the list of choices in the idle if returns the option else. In addition, if this third option is selected, the simulator prints "timeout". vending_machine.txt <https://github.com/user-attachments/files/22390324/vending_machine.txt> Captura.de.pantalla.2025-09-17.181827.png (view on web) <https://github.com/user-attachments/assets/ee32fc68-52c8-415f-a839-b5dabadbe9c8> BR, Laura — Reply to this email directly, view it on GitHub <#84 (comment)>, or unsubscribe <https://github.com/notifications/unsubscribe-auth/AK6L6IMAPU7VPV6XK6Q4ED33TGFBDAVCNFSM6AAAAACGU3OWGGVHI2DSMVQWIX3LMV43OSLTON2WKQ3PNVWWK3TUHMZTGMBTG44DKMJWGE> . You are receiving this because you commented.Message ID: ***@***.***>