Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Performance difference for CTMC model checking #88

Open
volkm opened this issue Sep 23, 2020 · 0 comments
Open

Performance difference for CTMC model checking #88

volkm opened this issue Sep 23, 2020 · 0 comments

Comments

@volkm
Copy link
Contributor

volkm commented Sep 23, 2020

I get different runtimes for CTMC modelchecking when computing the transient probability of reaching a label compared to avoiding the label.

I attached a minimal CTMC modeling a phase-type distribution with 9 states. I compute the following properties:

  1. P=? [F=30000 "goal"]
  2. P=? [F=30000 !"goal"]

Model checking the first property is over 10 times slower than the second property even though the second one is just the inverse of the first one.
The complete output is:

Command line arguments: -drn ctmc.drn --prop 'P=? [F=30000 "goal"];P=? [F=30000 !"goal"]'
Current working directory: ~/storm/build

Time for model construction: 0.000s.

-------------------------------------------------------------- 
Model type: 	CTMC (sparse)
States: 	9
Transitions: 	9
Reward Models:  none
State Labels: 	2 labels
   * init -> 1 item(s)
   * goal -> 1 item(s)
Choice Labels: 	none
-------------------------------------------------------------- 

Model checking property "1": P=? [true U[30000, 30000] "goal"] ...
Result (for initial states): 0.6646109497
Time for model checking: 0.018s.

Model checking property "2": P=? [true U[30000, 30000] !("goal")] ...
Result (for initial states): 0.3353890503
Time for model checking: 0.000s.

Do we have an idea what might be responsible for this difference?

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Projects
None yet
Development

No branches or pull requests

2 participants