Spinroot

marion

Member

Registered: 2011-03-28

Posts: 1

nondeterministic automaton

Hello,

I am new user to Spin and I was wondering how spin responds to a non-deterministic automaton ? I saw that you can add options such as "random" or "interactive" but if you don't use this options, how Spin choose an edge when you have a non-deterministic automaton ?

Thanks.

Marion

spinroot

forum

Registered: 2010-11-18

Posts: 700

Website

Re: nondeterministic automaton

Hi Marion,
In simulation mode non-determinism is resolved by making pseudo-random choices (or interactively prompting the user if you use -i)
In verification model the model checker considers all possible ways that the non-determinism can be resolved.