[tlaplus] how TLA+ verify the crash model?

[杨超 <magicsupery@xxxxxxxxx>]

fair process config = CONFIG

begin

Ctor:

Tick:

CrashOrContinue:

            if sthDone then

                   goto  Done;

            else

                     either

                         goto Tick;

                     or

                          goto Ctor;

                      end either;

            end if;   

end process;

my system has 4 process, the config process maybe crash, i want to verify that after the config crash, the whole system can eventually stable.

but i found the "either or" not make sure that goto Ctor will happen!

How can i do that, the crash will happen at some time, but the time not sure?

-- 
You received this message because you are subscribed to the Google Groups "tlaplus" group.
To unsubscribe from this group and stop receiving emails from it, send an email to tlaplus+unsubscribe@xxxxxxxxxxxxxxxx.
To view this discussion on the web visit https://groups.google.com/d/msgid/tlaplus/62e4f654-bdaf-473b-bc7a-18ad3d1e9f7dn%40googlegroups.com.