how to designate a particular initial state for a model？

[fanji...@gmail.com]

Hi everyone,

I want to construct a model in PRISM through direct specification of its files of transition matrix ,labels and states.

Actually, i just want to get an actual optimal route of an adversary.

First I used this command and got those files:

command:  "./prism test.nm -pf 'Rmax=? [F t=5]' -exportadvmdp adv.tra -exportstates adv.sta -exportlabels adv.lab -noprob1 -s"

Then  I used this command to  construct a model  to get an actual optimal route:

command:" ./prism -importmodel adv.all -exporttrans stdout.txt"

But,the initial state in my model is 23,as the adv.lab shows,

0="init" 1="deadlock" 2="final"

23: 0

2511: 1 2

2512: 1 2

2513: 1 2

2514: 1 2

2515: 1 2

2516: 1 2

2517: 1 2

2518: 1 2

2519: 1 2

2520: 1 2

2521: 1 2

(......)

But finally the sdout.txt compute the transition start at state 0. I've already imported the file of lables ,i don't know the  reason.

31 31 31

0 0 5 1 tick

1 0 0 1 IncDimmer_start

2 0 1 1 

3 0 2 1 

4 0 3 1 

5 0 10 1 tack

6 0 11 1 tick

7 0 6 1 IncDimmer_start

8 0 7 1 

9 0 8 1 

10 0 9 1 

11 0 16 1 tack

12 0 17 1 tick

13 0 12 1 IncDimmer_start

14 0 13 1 

15 0 14 1 

16 0 15 1 

17 0 22 1 tack

18 0 23 1 tick

19 0 18 1 IncDimmer_start

(......)

Sincerely.

:)

Jenney.

[Dave Parker]

Hi,

You'll probably find that the induced model has less states since not
all of them are explored under that optimal adversary. Export the states
for the second invocation of prism too (with -exportstates or
-exportmodel) and see if state 23 in the original model corresponds to
state 0 in the induced one.

Dave

> --
> You received this message because you are subscribed to the Google
> Groups "PRISM model checker" group.
> To unsubscribe from this group and stop receiving emails from it, send
> an email to prismmodelchec...@googlegroups.com
> <mailto:prismmodelchec...@googlegroups.com>.
> To post to this group, send email to prismmod...@googlegroups.com
> <mailto:prismmod...@googlegroups.com>.
> Visit this group at https://groups.google.com/group/prismmodelchecker.
> For more options, visit https://groups.google.com/d/optout.

[fanji...@gmail.com]

Dear Dave,

Thank you for your answer.

I tried this command to export the states,but the 'new state 0' is not corresponds to the 'original state 23'.

my command:   ./prism -importmodel adv.all -exporttrans stdout.txt -exportstates adv.sta

original state 23:    23:(0,true,0,0,true,true,false,true,false,true,false,1,1)

new state 0:    0:(0,true,0,0,false,false,false,false,true,false,false,1,2)

additionally, the sdout.txt (adversary route) shows that the first action is :

0 0 5 1 tick

but it's wrong.according to my model ,the first action can't be tick,it's guard can' t be satisfied at the beginning.

Sincerely   :)

Jenney.

在 2018年1月11日星期四 UTC+8下午5:33:53，d.a.parker写道：

> <mailto:prismmodelchecker+unsub...@googlegroups.com>.