Problem importing explicit model

[Inés Álvarez Vadillo]

Hello,

I am writing because I am experiencing issues with the -importtrans command in the command line. Specifically, I have developed a model using the PRISM GUI and exported it using the following command:

./prism link-model.pm -exporttrans link.tra -exportstates link.sta

The output is the following: 

PRISM

=====

Version: 4.6

Date: Thu Sep 01 15:48:24 CEST 2022

Hostname: MacBook-Pro-de-Ines-2.local

Memory limits: cudd=1g, java(heap)=910.5m

Command line: prism link-model.pm -exporttrans link.tra -exportstates link.sta

Parsing model file "link-model.pm"...

Type:        DTMC

Modules:     link 

Variables:   r 

Building model...

Computing reachable states...

Reachability (BFS): 2 iterations in 0.00 seconds (average 0.000000, setup 0.00)

Time for model construction: 0.016 seconds.

Type:        DTMC

States:      5 (1 initial)

Transitions: 15

Transition matrix: 41 nodes (16 terminal), 15 minterms, vars: 3r/3c

Exporting transition matrix in plain text format to file "link.tra"...

Exporting list of reachable states in plain text format to file "link.sta"...

Nonetheless, when I try to import the explicit model using this command:

./prism -importtrans link.tra -importstates link.sta -dtmc

The result is:

PRISM

=====

Version: 4.6

Date: Thu Sep 01 15:49:25 CEST 2022

Hostname: MacBook-Pro-de-Ines-2.local

Memory limits: cudd=1g, java(heap)=910.5m

Command line: prism -importtrans link.tra -importstates link.sta -dtmc

Importing model from "link.tra", "link.sta"...

Using specified model type: DTMC

---------------------------------------------------------------------

Building model...

Computing reachable states...

Reachability (BFS): 1 iterations in 0.00 seconds (average 0.000000, setup 0.00)

Time for model construction: 0.011 seconds.

Type:        DTMC

States:      1 (1 initial)

Transitions: 1

Transition matrix: 8 nodes (2 terminal), 1 minterms, vars: 3r/3c

I will be very grateful if I could get any help in this regard. Thank yo for your time.

Best wishes,

Inés Álvarez

[Gethin Norman]

Hi Inés,

the issue could be that the initial state is not the first state listed in the sta file and therefore the initial state in the important model will be different. To fix this if you also export and import the labels:

-exportlabels <file>
-importlabels <file>

this will include the lab for the initial state (“init”).

thanks

Gethin

> --
> 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.
> To view this discussion on the web, visit https://groups.google.com/d/msgid/prismmodelchecker/de1c1c94-f147-485e-bc9c-31a9dfe77073n%40googlegroups.com.