Spinroot

A forum for Spin users

You are not logged in.

#1 2011-03-28 09:54:54

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

Offline

#2 2011-04-01 18:24:35

spinroot
forum
Registered: 2010-11-18
Posts: 691
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.

Offline

Board footer

Powered by FluxBB