simpath doesn't work when the model is imported via .tra file

[Jin Ge]

simpath works fine on lec3.pm :

bin/prism lec3.pm -simpath 20 stdout

But when I import the model from the transition file and then ask for a random traj, simpath refuses to work. I thought my installation was not good but I did PRISM in an Ubuntu and a RedHat machine, and both give me the same error.

===Testtrans.tra===

6 9
0 1 0.5
0 3 0.5
1 0 0.5
1 2 0.25
1 4 0.25
2 5 1
3 3 1
4 4 1
5 2 1

================

Command line: prism -importtrans Testtrans.tra -dtmc -simpath time=5 stdout

Importing model (DTMC) from "Testtrans.tra"...

Generating random path with time limit 5.0...

action step x

Exception in thread "main" java.lang.ArrayIndexOutOfBoundsException: -1

at java.util.ArrayList.elementData(ArrayList.java:400)

at java.util.ArrayList.get(ArrayList.java:413)

at simulator.PathFull.getPreviousModuleOrActionIndex(PathFull.java:273)

at simulator.PathFull.getPreviousModuleOrAction(PathFull.java:279)

at simulator.GenerateSimulationPath.generatePath(GenerateSimulationPath.java:439)

at simulator.GenerateSimulationPath.generateSimulationPath(GenerateSimulationPath.java:126)

at prism.Prism.generateSimulationPath(Prism.java:3289)

at prism.PrismCL.run(PrismCL.java:304)

at prism.PrismCL.go(PrismCL.java:212)

at prism.PrismCL.main(PrismCL.java:2419)

I synthesized an adversary/strategy and would like to see a run using that strategy. It would be nice to import back the transitions and simpath.

Any suggestions? Thanks!

[Jin Ge]

Command line: prism -importtrans Testtrans.tra -dtmc -simpath 20 stdout

Importing model (DTMC) from "Testtrans.tra"...

Generating random path of length 20 steps...

action step x

Exception in thread "main" java.lang.ArrayIndexOutOfBoundsException: -1

at java.util.ArrayList.elementData(ArrayList.java:400)

at java.util.ArrayList.get(ArrayList.java:413)

at simulator.PathFull.getPreviousModuleOrActionIndex(PathFull.java:273)

at simulator.PathFull.getPreviousModuleOrAction(PathFull.java:279)

at simulator.GenerateSimulationPath.generatePath(GenerateSimulationPath.java:439)

at simulator.GenerateSimulationPath.generateSimulationPath(GenerateSimulationPath.java:126)

at prism.Prism.generateSimulationPath(Prism.java:3289)

at prism.PrismCL.run(PrismCL.java:304)

at prism.PrismCL.go(PrismCL.java:212)

at prism.PrismCL.main(PrismCL.java:2419)

[Dave Parker]

Hi,

I'm afraid simulation-based methods are not supported when models are
imported explicitly.

Best wishes,

Dave

On 24/08/2016 17:06, Jin Ge wrote:
>
> Command line: prism -importtrans Testtrans.tra -dtmc -simpath 20 stdout
>
> Importing model (DTMC) from "Testtrans.tra"...
>
> Generating random path of length 20 steps...
>
> action step x
> Exception in thread "main" java.lang.ArrayIndexOutOfBoundsException: -1
> at java.util.ArrayList.elementData(ArrayList.java:400)
> at java.util.ArrayList.get(ArrayList.java:413)
> at simulator.PathFull.getPreviousModuleOrActionIndex(PathFull.java:273)
> at simulator.PathFull.getPreviousModuleOrAction(PathFull.java:279)
> at
> simulator.GenerateSimulationPath.generatePath(GenerateSimulationPath.java:439)
> at
> simulator.GenerateSimulationPath.generateSimulationPath(GenerateSimulationPath.java:126)
> at prism.Prism.generateSimulationPath(Prism.java:3289)
> at prism.PrismCL.run(PrismCL.java:304)
> at prism.PrismCL.go(PrismCL.java:212)
> at prism.PrismCL.main(PrismCL.java:2419)
>
>
> On Wednesday, August 24, 2016 at 12:01:09 PM UTC-4, Jin Ge wrote:
>
> simpath works fine on lec3.pm

> <http://www.prismmodelchecker.org/manual/uploads/lec3.pm> :
> bin/prism lec3.pm <http://lec3.pm> -simpath 20 stdout

> --
> 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.