Spinroot

aleander

Member

Registered: 2013-01-25

Posts: 3

random and interactive simulation

Hello to each forumers,

I'm approaching with formal verification for my master degree thesis. I'm implementing an automatic trasformation from uml state machine to promela process in the scope of model-driven engeenering.
I modelled the state by a global variable "state", and created the aliases for the state by means of "mtype".
I also initialized the variable in a manner like: state = INIT_STATE.

Then I write my process. It is like:

active proctype tsr() {
do
    :: (state == INIT_STATE) ->
           // do-things
    :: (state == T01) ->
          // do-thing
  etc.
}

So it happens to me that when I try interactive simulation, spin asks to choice the value of the state as if it were a non-deterministic choice.
But I initialized the state variable for avoid this non-determinism.

So what is my (conceptual, i think) error?

Thanks in advance for help.

Alessandro Ranieri

Last edited by aleander (2013-01-27 13:38:54)

spinroot

forum

Registered: 2010-11-18

Posts: 704

Website

Re: random and interactive simulation

You're doing it correctly -- there might be a bug in the interactive simulation though. I'll check.