sp
/
tempest
1
0
Fork 0
Code Issues Pull Requests Projects Releases Wiki Activity
Browse Source

removed old examples 

Former-commit-id: 9611fcfe4a [formerly 56da087130]
Former-commit-id: a4afe1fd18
main
sjunges 9 years ago
parent
6843f4349f
commit
1ed5581a1d
224 changed files with 0 additions and 1044090 deletions
Split View
  1. 1655
      examples/exported-jani-models/beauquier11.jani
  2. 455
      examples/exported-jani-models/beauquier3.jani
  3. 743
      examples/exported-jani-models/beauquier5.jani
  4. 1039
      examples/exported-jani-models/beauquier7.jani
  5. 1343
      examples/exported-jani-models/beauquier9.jani
  6. 1676
      examples/exported-jani-models/brp.jani
  7. 3081
      examples/exported-jani-models/byzantine4_1.jani
  8. 13978
      examples/exported-jani-models/cc_edf.jani
  9. 209
      examples/exported-jani-models/cell.jani
  10. 2023
      examples/exported-jani-models/circadian.jani
  11. 1556
      examples/exported-jani-models/cluster.jani
  12. 4237
      examples/exported-jani-models/coin10.jani
  13. 901
      examples/exported-jani-models/coin2.jani
  14. 1723
      examples/exported-jani-models/coin4.jani
  15. 2553
      examples/exported-jani-models/coin6.jani
  16. 3391
      examples/exported-jani-models/coin8.jani
  17. 2455
      examples/exported-jani-models/contract_bmgr.jani
  18. 3508
      examples/exported-jani-models/crowds.jani
  19. 2125
      examples/exported-jani-models/csma2_2.jani
  20. 3265
      examples/exported-jani-models/csma2_4.jani
  21. 7573
      examples/exported-jani-models/csma2_6.jani
  22. 3047
      examples/exported-jani-models/csma3_2.jani
  23. 4757
      examples/exported-jani-models/csma3_4.jani
  24. 11219
      examples/exported-jani-models/csma3_6.jani
  25. 3977
      examples/exported-jani-models/csma4_2.jani
  26. 6257
      examples/exported-jani-models/csma4_4.jani
  27. 14873
      examples/exported-jani-models/csma4_6.jani
  28. 2359
      examples/exported-jani-models/cyclin.jani
  29. 439
      examples/exported-jani-models/dice.jani
  30. 3994
      examples/exported-jani-models/dining_crypt10.jani
  31. 6044
      examples/exported-jani-models/dining_crypt15.jani
  32. 1208
      examples/exported-jani-models/dining_crypt3.jani
  33. 1600
      examples/exported-jani-models/dining_crypt4.jani
  34. 1994
      examples/exported-jani-models/dining_crypt5.jani
  35. 2390
      examples/exported-jani-models/dining_crypt6.jani
  36. 2788
      examples/exported-jani-models/dining_crypt7.jani
  37. 3188
      examples/exported-jani-models/dining_crypt8.jani
  38. 3590
      examples/exported-jani-models/dining_crypt9.jani
  39. 1755
      examples/exported-jani-models/embedded.jani
  40. 508
      examples/exported-jani-models/fair_exchange10.jani
  41. 6102
      examples/exported-jani-models/fgf.jani
  42. 214
      examples/exported-jani-models/firewire_abs.jani
  43. 5013
      examples/exported-jani-models/firewire_impl.jani
  44. 3456
      examples/exported-jani-models/fms.jani
  45. 16360
      examples/exported-jani-models/gossip4.jani
  46. 928
      examples/exported-jani-models/graph4.jani
  47. 1094
      examples/exported-jani-models/herman11.jani
  48. 1284
      examples/exported-jani-models/herman13.jani
  49. 1474
      examples/exported-jani-models/herman15.jani
  50. 1664
      examples/exported-jani-models/herman17.jani
  51. 1854
      examples/exported-jani-models/herman19.jani
  52. 2044
      examples/exported-jani-models/herman21.jani
  53. 334
      examples/exported-jani-models/herman3.jani
  54. 524
      examples/exported-jani-models/herman5.jani
  55. 714
      examples/exported-jani-models/herman7.jani
  56. 904
      examples/exported-jani-models/herman9.jani
  57. 968
      examples/exported-jani-models/ij10.jani
  58. 1072
      examples/exported-jani-models/ij11.jani
  59. 1178
      examples/exported-jani-models/ij12.jani
  60. 1286
      examples/exported-jani-models/ij13.jani
  61. 1396
      examples/exported-jani-models/ij14.jani
  62. 1508
      examples/exported-jani-models/ij15.jani
  63. 1622
      examples/exported-jani-models/ij16.jani
  64. 1738
      examples/exported-jani-models/ij17.jani
  65. 1856
      examples/exported-jani-models/ij18.jani
  66. 1976
      examples/exported-jani-models/ij19.jani
  67. 2098
      examples/exported-jani-models/ij20.jani
  68. 2222
      examples/exported-jani-models/ij21.jani
  69. 296
      examples/exported-jani-models/ij3.jani
  70. 386
      examples/exported-jani-models/ij4.jani
  71. 478
      examples/exported-jani-models/ij5.jani
  72. 572
      examples/exported-jani-models/ij6.jani
  73. 668
      examples/exported-jani-models/ij7.jani
  74. 766
      examples/exported-jani-models/ij8.jani
  75. 866
      examples/exported-jani-models/ij9.jani
  76. 835
      examples/exported-jani-models/investor.jani
  77. 1584
      examples/exported-jani-models/kaminsky.jani
  78. 1580
      examples/exported-jani-models/kanban.jani
  79. 683
      examples/exported-jani-models/knacl.jani
  80. 9214
      examples/exported-jani-models/leader_async_10.jani
  81. 2739
      examples/exported-jani-models/leader_async_3.jani
  82. 3646
      examples/exported-jani-models/leader_async_4.jani
  83. 4559
      examples/exported-jani-models/leader_async_5.jani
  84. 5478
      examples/exported-jani-models/leader_async_6.jani
  85. 6403
      examples/exported-jani-models/leader_async_7.jani
  86. 7334
      examples/exported-jani-models/leader_async_8.jani
  87. 8271
      examples/exported-jani-models/leader_async_9.jani
  88. 1687
      examples/exported-jani-models/leader_sync_3_2.jani
  89. 1777
      examples/exported-jani-models/leader_sync_3_3.jani
  90. 1867
      examples/exported-jani-models/leader_sync_3_4.jani
  91. 1957
      examples/exported-jani-models/leader_sync_3_5.jani
  92. 2047
      examples/exported-jani-models/leader_sync_3_6.jani
  93. 2227
      examples/exported-jani-models/leader_sync_3_8.jani
  94. 2165
      examples/exported-jani-models/leader_sync_4_2.jani
  95. 2283
      examples/exported-jani-models/leader_sync_4_3.jani
  96. 2401
      examples/exported-jani-models/leader_sync_4_4.jani
  97. 2519
      examples/exported-jani-models/leader_sync_4_5.jani
  98. 2637
      examples/exported-jani-models/leader_sync_4_6.jani
  99. 2873
      examples/exported-jani-models/leader_sync_4_8.jani
  100. 2643
      examples/exported-jani-models/leader_sync_5_2.jani

1655
examples/exported-jani-models/beauquier11.jani
File diff suppressed because it is too large
View File

455
examples/exported-jani-models/beauquier3.jani
View File

@ -1,455 +0,0 @@
{
"jani-version":1,
"features":[
"derived-operators"
],
"name":"Converted from PRISM by IscasMC",
"type":"mdp",
"actions":[
{
"name":"tau__"
}
],
"variables":[
{
"name":"d1",
"type":"bool"
},
{
"name":"p1",
"type":"bool"
},
{
"name":"d2",
"type":"bool"
},
{
"name":"p2",
"type":"bool"
},
{
"name":"d3",
"type":"bool"
},
{
"name":"p3",
"type":"bool"
}
],
"observables":[
{
"name":"\"steps\""
}
],
"initial-states":{
"exp":true
},
"automata":[
{
"name":"process1",
"locations":[
{
"name":"location",
"observables":[
{
"ref":"\"steps\"",
"value":1
}
]
}
],
"initial-locations":[
"location"
],
"edges":[
{
"location":"location",
"action":"tau__",
"guard":{
"exp":{
"op":"∧",
"left":{
"op":"=",
"left":"d1",
"right":"d3"
},
"right":{
"op":"=",
"left":"p1",
"right":"p3"
}
}
},
"destinations":[
{
"probability":{
"exp":0.5000000
},
"location":"location",
"assignments":[
{
"ref":"d1",
"value":{
"op":"¬",
"exp":"d1"
}
},
{
"ref":"p1",
"value":"p1"
}
],
"observables":[
]
},
{
"probability":{
"exp":0.5000000
},
"location":"location",
"assignments":[
{
"ref":"d1",
"value":{
"op":"¬",
"exp":"d1"
}
},
{
"ref":"p1",
"value":{
"op":"¬",
"exp":"p1"
}
}
],
"observables":[
]
}
]
},
{
"location":"location",
"action":"tau__",
"guard":{
"exp":{
"op":"∧",
"left":{
"op":"=",
"left":"d1",
"right":"d3"
},
"right":{
"op":"¬",
"exp":{
"op":"=",
"left":"p1",
"right":"p3"
}
}
}
},
"destinations":[
{
"probability":{
"exp":1
},
"location":"location",
"assignments":[
{
"ref":"d1",
"value":{
"op":"¬",
"exp":"d1"
}
}
],
"observables":[
]
}
]
}
]
},
{
"name":"process2",
"locations":[
{
"name":"location"
}
],
"initial-locations":[
"location"
],
"edges":[
{
"location":"location",
"action":"tau__",
"guard":{
"exp":{
"op":"∧",
"left":{
"op":"=",
"left":"d2",
"right":"d1"
},
"right":{
"op":"=",
"left":"p2",
"right":"p1"
}
}
},
"destinations":[
{
"probability":{
"exp":0.5000000
},
"location":"location",
"assignments":[
{
"ref":"d2",
"value":{
"op":"¬",
"exp":"d2"
}
},
{
"ref":"p2",
"value":"p2"
}
],
"observables":[
]
},
{
"probability":{
"exp":0.5000000
},
"location":"location",
"assignments":[
{
"ref":"d2",
"value":{
"op":"¬",
"exp":"d2"
}
},
{
"ref":"p2",
"value":{
"op":"¬",
"exp":"p2"
}
}
],
"observables":[
]
}
]
},
{
"location":"location",
"action":"tau__",
"guard":{
"exp":{
"op":"∧",
"left":{
"op":"=",
"left":"d2",
"right":"d1"
},
"right":{
"op":"¬",
"exp":{
"op":"=",
"left":"p2",
"right":"p1"
}
}
}
},
"destinations":[
{
"probability":{
"exp":1
},
"location":"location",
"assignments":[
{
"ref":"d2",
"value":{
"op":"¬",
"exp":"d2"
}
}
],
"observables":[
]
}
]
}
]
},
{
"name":"process3",
"locations":[
{
"name":"location"
}
],
"initial-locations":[
"location"
],
"edges":[
{
"location":"location",
"action":"tau__",
"guard":{
"exp":{
"op":"∧",
"left":{
"op":"=",
"left":"d3",
"right":"d2"
},
"right":{
"op":"=",
"left":"p3",
"right":"p2"
}
}
},
"destinations":[
{
"probability":{
"exp":0.5000000
},
"location":"location",
"assignments":[
{
"ref":"d3",
"value":{
"op":"¬",
"exp":"d3"
}
},
{
"ref":"p3",
"value":"p3"
}
],
"observables":[
]
},
{
"probability":{
"exp":0.5000000
},
"location":"location",
"assignments":[
{
"ref":"d3",
"value":{
"op":"¬",
"exp":"d3"
}
},
{
"ref":"p3",
"value":{
"op":"¬",
"exp":"p3"
}
}
],
"observables":[
]
}
]
},
{
"location":"location",
"action":"tau__",
"guard":{
"exp":{
"op":"∧",
"left":{
"op":"=",
"left":"d3",
"right":"d2"
},
"right":{
"op":"¬",
"exp":{
"op":"=",
"left":"p3",
"right":"p2"
}
}
}
},
"destinations":[
{
"probability":{
"exp":1
},
"location":"location",
"assignments":[
{
"ref":"d3",
"value":{
"op":"¬",
"exp":"d3"
}
}
],
"observables":[
]
}
]
}
]
}
],
"system":{
"elements":[
{
"automaton":"process1"
},
{
"automaton":"process2"
},
{
"automaton":"process3"
}
],
"syncs":[
{
"synchronise":[
"tau__",
null,
null
],
"result":"tau__"
},
{
"synchronise":[
null,
"tau__",
null
],
"result":"tau__"
},
{
"synchronise":[
null,
null,
"tau__"
],
"result":"tau__"
}
]
}
}

743
examples/exported-jani-models/beauquier5.jani
View File

@ -1,743 +0,0 @@
{
"jani-version":1,
"features":[
"derived-operators"
],
"name":"Converted from PRISM by IscasMC",
"type":"mdp",
"actions":[
{
"name":"tau__"
}
],
"variables":[
{
"name":"d1",
"type":"bool"
},
{
"name":"p1",
"type":"bool"
},
{
"name":"d2",
"type":"bool"
},
{
"name":"p2",
"type":"bool"
},
{
"name":"d3",
"type":"bool"
},
{
"name":"p3",
"type":"bool"
},
{
"name":"d4",
"type":"bool"
},
{
"name":"p4",
"type":"bool"
},
{
"name":"d5",
"type":"bool"
},
{
"name":"p5",
"type":"bool"
}
],
"observables":[
{
"name":"\"steps\""
}
],
"initial-states":{
"exp":true
},
"automata":[
{
"name":"process1",
"locations":[
{
"name":"location",
"observables":[
{
"ref":"\"steps\"",
"value":1
}
]
}
],
"initial-locations":[
"location"
],
"edges":[
{
"location":"location",
"action":"tau__",
"guard":{
"exp":{
"op":"∧",
"left":{
"op":"=",
"left":"d1",
"right":"d5"
},
"right":{
"op":"=",
"left":"p1",
"right":"p5"
}
}
},
"destinations":[
{
"probability":{
"exp":0.5000000
},
"location":"location",
"assignments":[
{
"ref":"d1",
"value":{
"op":"¬",
"exp":"d1"
}
},
{
"ref":"p1",
"value":"p1"
}
],
"observables":[
]
},
{
"probability":{
"exp":0.5000000
},
"location":"location",
"assignments":[
{
"ref":"d1",
"value":{
"op":"¬",
"exp":"d1"
}
},
{
"ref":"p1",
"value":{
"op":"¬",
"exp":"p1"
}
}
],
"observables":[
]
}
]
},
{
"location":"location",
"action":"tau__",
"guard":{
"exp":{
"op":"∧",
"left":{
"op":"=",
"left":"d1",
"right":"d5"
},
"right":{
"op":"¬",
"exp":{
"op":"=",
"left":"p1",
"right":"p5"
}
}
}
},
"destinations":[
{
"probability":{
"exp":1
},
"location":"location",
"assignments":[
{
"ref":"d1",
"value":{
"op":"¬",
"exp":"d1"
}
}
],
"observables":[
]
}
]
}
]
},
{
"name":"process2",
"locations":[
{
"name":"location"
}
],
"initial-locations":[
"location"
],
"edges":[
{
"location":"location",
"action":"tau__",
"guard":{
"exp":{
"op":"∧",
"left":{
"op":"=",
"left":"d2",
"right":"d1"
},
"right":{
"op":"=",
"left":"p2",
"right":"p1"
}
}
},
"destinations":[
{
"probability":{
"exp":0.5000000
},
"location":"location",
"assignments":[
{
"ref":"d2",
"value":{
"op":"¬",
"exp":"d2"
}
},
{
"ref":"p2",
"value":"p2"
}
],
"observables":[
]
},
{
"probability":{
"exp":0.5000000
},
"location":"location",
"assignments":[
{
"ref":"d2",
"value":{
"op":"¬",
"exp":"d2"
}
},
{
"ref":"p2",
"value":{
"op":"¬",
"exp":"p2"
}
}
],
"observables":[
]
}
]
},
{
"location":"location",
"action":"tau__",
"guard":{
"exp":{
"op":"∧",
"left":{
"op":"=",
"left":"d2",
"right":"d1"
},
"right":{
"op":"¬",
"exp":{
"op":"=",
"left":"p2",
"right":"p1"
}
}
}
},
"destinations":[
{
"probability":{
"exp":1
},
"location":"location",
"assignments":[
{
"ref":"d2",
"value":{
"op":"¬",
"exp":"d2"
}
}
],
"observables":[
]
}
]
}
]
},
{
"name":"process3",
"locations":[
{
"name":"location"
}
],
"initial-locations":[
"location"
],
"edges":[
{
"location":"location",
"action":"tau__",
"guard":{
"exp":{
"op":"∧",
"left":{
"op":"=",
"left":"d3",
"right":"d2"
},
"right":{
"op":"=",
"left":"p3",
"right":"p2"
}
}
},
"destinations":[
{
"probability":{
"exp":0.5000000
},
"location":"location",
"assignments":[
{
"ref":"d3",
"value":{
"op":"¬",
"exp":"d3"
}
},
{
"ref":"p3",
"value":"p3"
}
],
"observables":[
]
},
{
"probability":{
"exp":0.5000000
},
"location":"location",
"assignments":[
{
"ref":"d3",
"value":{
"op":"¬",
"exp":"d3"
}
},
{
"ref":"p3",
"value":{
"op":"¬",
"exp":"p3"
}
}
],
"observables":[
]
}
]
},
{
"location":"location",
"action":"tau__",
"guard":{
"exp":{
"op":"∧",
"left":{
"op":"=",
"left":"d3",
"right":"d2"
},
"right":{
"op":"¬",
"exp":{
"op":"=",
"left":"p3",
"right":"p2"
}
}
}
},
"destinations":[
{
"probability":{
"exp":1
},
"location":"location",
"assignments":[
{
"ref":"d3",
"value":{
"op":"¬",
"exp":"d3"
}
}
],
"observables":[
]
}
]
}
]
},
{
"name":"process4",
"locations":[
{
"name":"location"
}
],
"initial-locations":[
"location"
],
"edges":[
{
"location":"location",
"action":"tau__",
"guard":{
"exp":{
"op":"∧",
"left":{
"op":"=",
"left":"d4",
"right":"d3"
},
"right":{
"op":"=",
"left":"p4",
"right":"p3"
}
}
},
"destinations":[
{
"probability":{
"exp":0.5000000
},
"location":"location",
"assignments":[
{
"ref":"d4",
"value":{
"op":"¬",
"exp":"d4"
}
},
{
"ref":"p4",
"value":"p4"
}
],
"observables":[
]
},
{
"probability":{
"exp":0.5000000
},
"location":"location",
"assignments":[
{
"ref":"d4",
"value":{
"op":"¬",
"exp":"d4"
}
},
{
"ref":"p4",
"value":{
"op":"¬",
"exp":"p4"
}
}
],
"observables":[
]
}
]
},
{
"location":"location",
"action":"tau__",
"guard":{
"exp":{
"op":"∧",
"left":{
"op":"=",
"left":"d4",
"right":"d3"
},
"right":{
"op":"¬",
"exp":{
"op":"=",
"left":"p4",
"right":"p3"
}
}
}
},
"destinations":[
{
"probability":{
"exp":1
},
"location":"location",
"assignments":[
{
"ref":"d4",
"value":{
"op":"¬",
"exp":"d4"
}
}
],
"observables":[
]
}
]
}
]
},
{
"name":"process5",
"locations":[
{
"name":"location"
}
],
"initial-locations":[
"location"
],
"edges":[
{
"location":"location",
"action":"tau__",
"guard":{
"exp":{
"op":"∧",
"left":{
"op":"=",
"left":"d5",
"right":"d4"
},
"right":{
"op":"=",
"left":"p5",
"right":"p4"
}
}
},
"destinations":[
{
"probability":{
"exp":0.5000000
},
"location":"location",
"assignments":[
{
"ref":"d5",
"value":{
"op":"¬",
"exp":"d5"
}
},
{
"ref":"p5",
"value":"p5"
}
],
"observables":[
]
},
{
"probability":{
"exp":0.5000000
},
"location":"location",
"assignments":[
{
"ref":"d5",
"value":{
"op":"¬",
"exp":"d5"
}
},
{
"ref":"p5",
"value":{
"op":"¬",
"exp":"p5"
}
}
],
"observables":[
]
}
]
},
{
"location":"location",
"action":"tau__",
"guard":{
"exp":{
"op":"∧",
"left":{
"op":"=",
"left":"d5",
"right":"d4"
},
"right":{
"op":"¬",
"exp":{
"op":"=",
"left":"p5",
"right":"p4"
}
}
}
},
"destinations":[
{
"probability":{
"exp":1
},
"location":"location",
"assignments":[
{
"ref":"d5",
"value":{
"op":"¬",
"exp":"d5"
}
}
],
"observables":[
]
}
]
}
]
}
],
"system":{
"elements":[
{
"automaton":"process1"
},
{
"automaton":"process2"
},
{
"automaton":"process3"
},
{
"automaton":"process4"
},
{
"automaton":"process5"
}
],
"syncs":[
{
"synchronise":[
"tau__",
null,
null,
null,
null
],
"result":"tau__"
},
{
"synchronise":[
null,
"tau__",
null,
null,
null
],
"result":"tau__"
},
{
"synchronise":[
null,
null,
"tau__",
null,
null
],
"result":"tau__"
},
{
"synchronise":[
null,
null,
null,
"tau__",
null
],
"result":"tau__"
},
{
"synchronise":[
null,
null,
null,
null,
"tau__"
],
"result":"tau__"
}
]
}
}

1039
examples/exported-jani-models/beauquier7.jani
File diff suppressed because it is too large
View File

1343
examples/exported-jani-models/beauquier9.jani
File diff suppressed because it is too large
View File

1676
examples/exported-jani-models/brp.jani
File diff suppressed because it is too large
View File

3081
examples/exported-jani-models/byzantine4_1.jani
File diff suppressed because it is too large
View File

13978
examples/exported-jani-models/cc_edf.jani
File diff suppressed because it is too large
View File

209
examples/exported-jani-models/cell.jani
View File

@ -1,209 +0,0 @@
{
"jani-version":1,
"features":[
"derived-operators"
],
"name":"Converted from PRISM by IscasMC",
"type":"ctmc",
"actions":[
{
"name":"tau__"
}
],
"constants":[
{
"name":"N",
"type":"int"
}
],
"variables":[
{
"name":"n",
"type":{
"kind":"bounded",
"base":"int",
"lower-bound":0,
"upper-bound":"N"
}
}
],
"observables":[
{
"name":"\"calls\""
}
],
"initial-states":{
"exp":{
"op":"=",
"left":"n",
"right":0
}
},
"automata":[
{
"name":"cell",
"locations":[
{
"name":"location",
"observables":[
{
"ref":"\"calls\"",
"value":"n"
}
]
}
],
"initial-locations":[
"location"
],
"edges":[
{
"location":"location",
"action":"tau__",
"rate":{
"exp":49
},
"guard":{
"exp":{
"op":"<",
"left":"n",
"right":{
"op":"*",
"left":"N",
"right":0.8000000
}
}
},
"destinations":[
{
"probability":{
"exp":{
"op":"/",
"left":49,
"right":49
}
},
"location":"location",
"assignments":[
{
"ref":"n",
"value":{
"op":"+",
"left":"n",
"right":1
}
}
],
"observables":[
]
}
]
},
{
"location":"location",
"action":"tau__",
"rate":{
"exp":21
},
"guard":{
"exp":{
"op":"<",
"left":"n",
"right":"N"
}
},
"destinations":[
{
"probability":{
"exp":{
"op":"/",
"left":21,
"right":21
}
},
"location":"location",
"assignments":[
{
"ref":"n",
"value":{
"op":"+",
"left":"n",
"right":1
}
}
],
"observables":[
]
}
]
},
{
"location":"location",
"action":"tau__",
"rate":{
"exp":{
"op":"*",
"left":"n",
"right":1
}
},
"guard":{
"exp":{
"op":">",
"left":"n",
"right":0
}
},
"destinations":[
{
"probability":{
"exp":{
"op":"/",
"left":{
"op":"*",
"left":"n",
"right":1
},
"right":{
"op":"*",
"left":"n",
"right":1
}
}
},
"location":"location",
"assignments":[
{
"ref":"n",
"value":{
"op":"-",
"left":"n",
"right":1
}
}
],
"observables":[
]
}
]
}
]
}
],
"system":{
"elements":[
{
"automaton":"cell"
}
],
"syncs":[
{
"synchronise":[
"tau__"
],
"result":"tau__"
}
]
}
}

2023
examples/exported-jani-models/circadian.jani
File diff suppressed because it is too large
View File

1556
examples/exported-jani-models/cluster.jani
File diff suppressed because it is too large
View File

4237
examples/exported-jani-models/coin10.jani
File diff suppressed because it is too large
View File

901
examples/exported-jani-models/coin2.jani
View File

@ -1,901 +0,0 @@
{
"jani-version":1,
"features":[
"derived-operators"
],
"name":"Converted from PRISM by IscasMC",
"type":"mdp",
"actions":[
{
"name":"tau__"
},
{
"name":"done"
}
],
"constants":[
{
"name":"K",
"type":"int"
}
],
"variables":[
{
"name":"counter",
"type":{
"kind":"bounded",
"base":"int",
"lower-bound":0,
"upper-bound":{
"op":"*",
"left":{
"op":"*",
"left":2,
"right":{
"op":"+",
"left":"K",
"right":1
}
},
"right":2
}
}
},
{
"name":"pc1",
"type":{
"kind":"bounded",
"base":"int",
"lower-bound":0,
"upper-bound":3
}
},
{
"name":"coin1",
"type":{
"kind":"bounded",
"base":"int",
"lower-bound":0,
"upper-bound":1
}
},
{
"name":"pc2",
"type":{
"kind":"bounded",
"base":"int",
"lower-bound":0,
"upper-bound":3
}
},
{
"name":"coin2",
"type":{
"kind":"bounded",
"base":"int",
"lower-bound":0,
"upper-bound":1
}
}
],
"observables":[
{
"name":"\"steps\""
}
],
"initial-states":{
"exp":{
"op":"∧",
"left":{
"op":"∧",
"left":{
"op":"∧",
"left":{
"op":"∧",
"left":{
"op":"=",
"left":"counter",
"right":{
"op":"*",
"left":{
"op":"+",
"left":"K",
"right":1
},
"right":2
}
},
"right":{
"op":"=",
"left":"pc1",
"right":0
}
},
"right":{
"op":"=",
"left":"coin1",
"right":0
}
},
"right":{
"op":"=",
"left":"pc2",
"right":0
}
},
"right":{
"op":"=",
"left":"coin2",
"right":0
}
}
},
"automata":[
{
"name":"process1",
"locations":[
{
"name":"location",
"observables":[
{
"ref":"\"steps\"",
"value":1
}
]
}
],
"initial-locations":[
"location"
],
"edges":[
{
"location":"location",
"action":"tau__",
"guard":{
"exp":{
"op":"=",
"left":"pc1",
"right":0
}
},
"destinations":[
{
"probability":{
"exp":0.5000000
},
"location":"location",
"assignments":[
{
"ref":"coin1",
"value":0
},
{
"ref":"pc1",
"value":1
}
],
"observables":[
]
},
{
"probability":{
"exp":0.5000000
},
"location":"location",
"assignments":[
{
"ref":"coin1",
"value":1
},
{
"ref":"pc1",
"value":1
}
],
"observables":[
]
}
]
},
{
"location":"location",
"action":"tau__",
"guard":{
"exp":{
"op":"∧",
"left":{
"op":"∧",
"left":{
"op":"=",
"left":"pc1",
"right":1
},
"right":{
"op":"=",
"left":"coin1",
"right":0
}
},
"right":{
"op":">",
"left":"counter",
"right":0
}
}
},
"destinations":[
{
"probability":{
"exp":1
},
"location":"location",
"assignments":[
{
"ref":"counter",
"value":{
"op":"-",
"left":"counter",
"right":1
}
},
{
"ref":"pc1",
"value":2
},
{
"ref":"coin1",
"value":0
}
],
"observables":[
]
}
]
},
{
"location":"location",
"action":"tau__",
"guard":{
"exp":{
"op":"∧",
"left":{
"op":"∧",
"left":{
"op":"=",
"left":"pc1",
"right":1
},
"right":{
"op":"=",
"left":"coin1",
"right":1
}
},
"right":{
"op":"<",
"left":"counter",
"right":{
"op":"*",
"left":{
"op":"*",
"left":2,
"right":{
"op":"+",
"left":"K",
"right":1
}
},
"right":2
}
}
}
},
"destinations":[
{
"probability":{
"exp":1
},
"location":"location",
"assignments":[
{
"ref":"counter",
"value":{
"op":"+",
"left":"counter",
"right":1
}
},
{
"ref":"pc1",
"value":2
},
{
"ref":"coin1",
"value":0
}
],
"observables":[
]
}
]
},
{
"location":"location",
"action":"tau__",
"guard":{
"exp":{
"op":"∧",
"left":{
"op":"=",
"left":"pc1",
"right":2
},
"right":{
"op":"≤",
"left":"counter",
"right":2
}
}
},
"destinations":[
{
"probability":{
"exp":1
},
"location":"location",
"assignments":[
{
"ref":"pc1",
"value":3
},
{
"ref":"coin1",
"value":0
}
],
"observables":[
]
}
]
},
{
"location":"location",
"action":"tau__",
"guard":{
"exp":{
"op":"∧",
"left":{
"op":"=",
"left":"pc1",
"right":2
},
"right":{
"op":"≥",
"left":"counter",
"right":{
"op":"-",
"left":{
"op":"*",
"left":{
"op":"*",
"left":2,
"right":{
"op":"+",
"left":"K",
"right":1
}
},
"right":2
},
"right":2
}
}
}
},
"destinations":[
{
"probability":{
"exp":1
},
"location":"location",
"assignments":[
{
"ref":"pc1",
"value":3
},
{
"ref":"coin1",
"value":1
}
],
"observables":[
]
}
]
},
{
"location":"location",
"action":"tau__",
"guard":{
"exp":{
"op":"∧",
"left":{
"op":"∧",
"left":{
"op":"=",
"left":"pc1",
"right":2
},
"right":{
"op":">",
"left":"counter",
"right":2
}
},
"right":{
"op":"<",
"left":"counter",
"right":{
"op":"-",
"left":{
"op":"*",
"left":{
"op":"*",
"left":2,
"right":{
"op":"+",
"left":"K",
"right":1
}
},
"right":2
},
"right":2
}
}
}
},
"destinations":[
{
"probability":{
"exp":1
},
"location":"location",
"assignments":[
{
"ref":"pc1",
"value":0
}
],
"observables":[
]
}
]
},
{
"location":"location",
"action":"done",
"guard":{
"exp":{
"op":"=",
"left":"pc1",
"right":3
}
},
"destinations":[
{
"probability":{
"exp":1
},
"location":"location",
"assignments":[
{
"ref":"pc1",
"value":3
}
],
"observables":[
]
}
]
}
]
},
{
"name":"process2",
"locations":[
{
"name":"location"
}
],
"initial-locations":[
"location"
],
"edges":[
{
"location":"location",
"action":"tau__",
"guard":{
"exp":{
"op":"=",
"left":"pc2",
"right":0
}
},
"destinations":[
{
"probability":{
"exp":0.5000000
},
"location":"location",
"assignments":[
{
"ref":"coin2",
"value":0
},
{
"ref":"pc2",
"value":1
}
],
"observables":[
]
},
{
"probability":{
"exp":0.5000000
},
"location":"location",
"assignments":[
{
"ref":"coin2",
"value":1
},
{
"ref":"pc2",
"value":1
}
],
"observables":[
]
}
]
},
{
"location":"location",
"action":"tau__",
"guard":{
"exp":{
"op":"∧",
"left":{
"op":"∧",
"left":{
"op":"=",
"left":"pc2",
"right":1
},
"right":{
"op":"=",
"left":"coin2",
"right":0
}
},
"right":{
"op":">",
"left":"counter",
"right":0
}
}
},
"destinations":[
{
"probability":{
"exp":1
},
"location":"location",
"assignments":[
{
"ref":"counter",
"value":{
"op":"-",
"left":"counter",
"right":1
}
},
{
"ref":"pc2",
"value":2
},
{
"ref":"coin2",
"value":0
}
],
"observables":[
]
}
]
},
{
"location":"location",
"action":"tau__",
"guard":{
"exp":{
"op":"∧",
"left":{
"op":"∧",
"left":{
"op":"=",
"left":"pc2",
"right":1
},
"right":{
"op":"=",
"left":"coin2",
"right":1
}
},
"right":{
"op":"<",
"left":"counter",
"right":{
"op":"*",
"left":{
"op":"*",
"left":2,
"right":{
"op":"+",
"left":"K",
"right":1
}
},
"right":2
}
}
}
},
"destinations":[
{
"probability":{
"exp":1
},
"location":"location",
"assignments":[
{
"ref":"counter",
"value":{
"op":"+",
"left":"counter",
"right":1
}
},
{
"ref":"pc2",
"value":2
},
{
"ref":"coin2",
"value":0
}
],
"observables":[
]
}
]
},
{
"location":"location",
"action":"tau__",
"guard":{
"exp":{
"op":"∧",
"left":{
"op":"=",
"left":"pc2",
"right":2
},
"right":{
"op":"≤",
"left":"counter",
"right":2
}
}
},
"destinations":[
{
"probability":{
"exp":1
},
"location":"location",
"assignments":[
{
"ref":"pc2",
"value":3
},
{
"ref":"coin2",
"value":0
}
],
"observables":[
]
}
]
},
{
"location":"location",
"action":"tau__",
"guard":{
"exp":{
"op":"∧",
"left":{
"op":"=",
"left":"pc2",
"right":2
},
"right":{
"op":"≥",
"left":"counter",
"right":{
"op":"-",
"left":{
"op":"*",
"left":{
"op":"*",
"left":2,
"right":{
"op":"+",
"left":"K",
"right":1
}
},
"right":2
},
"right":2
}
}
}
},
"destinations":[
{
"probability":{
"exp":1
},
"location":"location",
"assignments":[
{
"ref":"pc2",
"value":3
},
{
"ref":"coin2",
"value":1
}
],
"observables":[
]
}
]
},
{
"location":"location",
"action":"tau__",
"guard":{
"exp":{
"op":"∧",
"left":{
"op":"∧",
"left":{
"op":"=",
"left":"pc2",
"right":2
},
"right":{
"op":">",
"left":"counter",
"right":2
}
},
"right":{
"op":"<",
"left":"counter",
"right":{
"op":"-",
"left":{
"op":"*",
"left":{
"op":"*",
"left":2,
"right":{
"op":"+",
"left":"K",
"right":1
}
},
"right":2
},
"right":2
}
}
}
},
"destinations":[
{
"probability":{
"exp":1
},
"location":"location",
"assignments":[
{
"ref":"pc2",
"value":0
}
],
"observables":[
]
}
]
},
{
"location":"location",
"action":"done",
"guard":{
"exp":{
"op":"=",
"left":"pc2",
"right":3
}
},
"destinations":[
{
"probability":{
"exp":1
},
"location":"location",
"assignments":[
{
"ref":"pc2",
"value":3
}
]
}
]
}
]
}
],
"system":{
"elements":[
{
"automaton":"process1"
},
{
"automaton":"process2"
}
],
"syncs":[
{
"synchronise":[
"done",
"done"
],
"result":"done"
},
{
"synchronise":[
"tau__",
null
],
"result":"tau__"
},
{
"synchronise":[
null,
"tau__"
],
"result":"tau__"
}
]
}
}

1723
examples/exported-jani-models/coin4.jani
File diff suppressed because it is too large
View File

2553
examples/exported-jani-models/coin6.jani
File diff suppressed because it is too large
View File

3391
examples/exported-jani-models/coin8.jani
File diff suppressed because it is too large
View File

2455
examples/exported-jani-models/contract_bmgr.jani
File diff suppressed because it is too large
View File

3508
examples/exported-jani-models/crowds.jani
File diff suppressed because it is too large
View File

2125
examples/exported-jani-models/csma2_2.jani
File diff suppressed because it is too large
View File

3265
examples/exported-jani-models/csma2_4.jani
File diff suppressed because it is too large
View File

7573
examples/exported-jani-models/csma2_6.jani
File diff suppressed because it is too large
View File

3047
examples/exported-jani-models/csma3_2.jani
File diff suppressed because it is too large
View File

4757
examples/exported-jani-models/csma3_4.jani
File diff suppressed because it is too large
View File

11219
examples/exported-jani-models/csma3_6.jani
File diff suppressed because it is too large
View File

3977
examples/exported-jani-models/csma4_2.jani
File diff suppressed because it is too large
View File

6257
examples/exported-jani-models/csma4_4.jani
File diff suppressed because it is too large
View File

14873
examples/exported-jani-models/csma4_6.jani
File diff suppressed because it is too large
View File

2359
examples/exported-jani-models/cyclin.jani
File diff suppressed because it is too large
View File

439
examples/exported-jani-models/dice.jani
View File

@ -1,439 +0,0 @@
{
"jani-version":1,
"features":[
"derived-operators"
],
"name":"Converted from PRISM by IscasMC",
"type":"dtmc",
"actions":[
{
"name":"tau__"
}
],
"variables":[
{
"name":"s",
"type":{
"kind":"bounded",
"base":"int",
"lower-bound":0,
"upper-bound":7
}
},
{
"name":"d",
"type":{
"kind":"bounded",
"base":"int",
"lower-bound":0,
"upper-bound":6
}
}
],
"observables":[
{
"name":"\"coin_flips\""
}
],
"initial-states":{
"exp":{
"op":"∧",
"left":{
"op":"=",
"left":"s",
"right":0
},
"right":{
"op":"=",
"left":"d",
"right":0
}
}
},
"automata":[
{
"name":"die",
"locations":[
{
"name":"location",
"observables":[
{
"ref":"\"coin_flips\"",
"value":{
"op":"?:",
"args":[
{
"op":"<",
"left":"s",
"right":7
},
1,
0
]
}
}
]
}
],
"initial-locations":[
"location"
],
"edges":[
{
"location":"location",
"action":"tau__",
"guard":{
"exp":{
"op":"=",
"left":"s",
"right":0
}
},
"destinations":[
{
"probability":{
"exp":0.5000000
},
"location":"location",
"assignments":[
{
"ref":"s",
"value":1
}
],
"observables":[
]
},
{
"probability":{
"exp":0.5000000
},
"location":"location",
"assignments":[
{
"ref":"s",
"value":2
}
],
"observables":[
]
}
]
},
{
"location":"location",
"action":"tau__",
"guard":{
"exp":{
"op":"=",
"left":"s",
"right":1
}
},
"destinations":[
{
"probability":{
"exp":0.5000000
},
"location":"location",
"assignments":[
{
"ref":"s",
"value":3
}
],
"observables":[
]
},
{
"probability":{
"exp":0.5000000
},
"location":"location",
"assignments":[
{
"ref":"s",
"value":4
}
],
"observables":[
]
}
]
},
{
"location":"location",
"action":"tau__",
"guard":{
"exp":{
"op":"=",
"left":"s",
"right":2
}
},
"destinations":[
{
"probability":{
"exp":0.5000000
},
"location":"location",
"assignments":[
{
"ref":"s",
"value":5
}
],
"observables":[
]
},
{
"probability":{
"exp":0.5000000
},
"location":"location",
"assignments":[
{
"ref":"s",
"value":6
}
],
"observables":[
]
}
]
},
{
"location":"location",
"action":"tau__",
"guard":{
"exp":{
"op":"=",
"left":"s",
"right":3
}
},
"destinations":[
{
"probability":{
"exp":0.5000000
},
"location":"location",
"assignments":[
{
"ref":"s",
"value":1
}
],
"observables":[
]
},
{
"probability":{
"exp":0.5000000
},
"location":"location",
"assignments":[
{
"ref":"s",
"value":7
},
{
"ref":"d",
"value":1
}
],
"observables":[
]
}
]
},
{
"location":"location",
"action":"tau__",
"guard":{
"exp":{
"op":"=",
"left":"s",
"right":4
}
},
"destinations":[
{
"probability":{
"exp":0.5000000
},
"location":"location",
"assignments":[
{
"ref":"s",
"value":7
},
{
"ref":"d",
"value":2
}
],
"observables":[
]
},
{
"probability":{
"exp":0.5000000
},
"location":"location",
"assignments":[
{
"ref":"s",
"value":7
},
{
"ref":"d",
"value":3
}
],
"observables":[
]
}
]
},
{
"location":"location",
"action":"tau__",
"guard":{
"exp":{
"op":"=",
"left":"s",
"right":5
}
},
"destinations":[
{
"probability":{
"exp":0.5000000
},
"location":"location",
"assignments":[
{
"ref":"s",
"value":7
},
{
"ref":"d",
"value":4
}
],
"observables":[
]
},
{
"probability":{
"exp":0.5000000
},
"location":"location",
"assignments":[
{
"ref":"s",
"value":7
},
{
"ref":"d",
"value":5
}
],
"observables":[
]
}
]
},
{
"location":"location",
"action":"tau__",
"guard":{
"exp":{
"op":"=",
"left":"s",
"right":6
}
},
"destinations":[
{
"probability":{
"exp":0.5000000
},
"location":"location",
"assignments":[
{
"ref":"s",
"value":2
}
],
"observables":[
]
},
{
"probability":{
"exp":0.5000000
},
"location":"location",
"assignments":[
{
"ref":"s",
"value":7
},
{
"ref":"d",
"value":6
}
],
"observables":[
]
}
]
},
{
"location":"location",
"action":"tau__",
"guard":{
"exp":{
"op":"=",
"left":"s",
"right":7
}
},
"destinations":[
{
"probability":{
"exp":1
},
"location":"location",
"assignments":[
{
"ref":"s",
"value":7
}
],
"observables":[
]
}
]
}
]
}
],
"system":{
"elements":[
{
"automaton":"die"
}
],
"syncs":[
{
"synchronise":[
"tau__"
],
"result":"tau__"
}
]
}
}

3994
examples/exported-jani-models/dining_crypt10.jani
File diff suppressed because it is too large
View File

6044
examples/exported-jani-models/dining_crypt15.jani
File diff suppressed because it is too large
View File

1208
examples/exported-jani-models/dining_crypt3.jani
File diff suppressed because it is too large
View File

1600
examples/exported-jani-models/dining_crypt4.jani
File diff suppressed because it is too large
View File

1994
examples/exported-jani-models/dining_crypt5.jani
File diff suppressed because it is too large
View File

2390
examples/exported-jani-models/dining_crypt6.jani
File diff suppressed because it is too large
View File

2788
examples/exported-jani-models/dining_crypt7.jani
File diff suppressed because it is too large
View File

3188
examples/exported-jani-models/dining_crypt8.jani
File diff suppressed because it is too large
View File

3590
examples/exported-jani-models/dining_crypt9.jani
File diff suppressed because it is too large
View File

1755
examples/exported-jani-models/embedded.jani
File diff suppressed because it is too large
View File

508
examples/exported-jani-models/fair_exchange10.jani
View File

@ -1,508 +0,0 @@
{
"jani-version":1,
"features":[
"derived-operators"
],
"name":"Converted from PRISM by IscasMC",
"type":"mdp",
"actions":[
{
"name":"tau__"
}
],
"variables":[
{
"name":"mA",
"type":{
"kind":"bounded",
"base":"int",
"lower-bound":0,
"upper-bound":10
}
},
{
"name":"mB",
"type":{
"kind":"bounded",
"base":"int",
"lower-bound":0,
"upper-bound":10
}
},
{
"name":"turn",
"type":{
"kind":"bounded",
"base":"int",
"lower-bound":0,
"upper-bound":1
}
},
{
"name":"d",
"type":{
"kind":"bounded",
"base":"int",
"lower-bound":0,
"upper-bound":1
}
},
{
"name":"i",
"type":{
"kind":"bounded",
"base":"int",
"lower-bound":0,
"upper-bound":10
}
}
],
"observables":[
],
"initial-states":{
"exp":{
"op":"∧",
"left":{
"op":"∧",
"left":{
"op":"∧",
"left":{
"op":"∧",
"left":{
"op":"=",
"left":"mA",
"right":0
},
"right":{
"op":"=",
"left":"mB",
"right":0
}
},
"right":{
"op":"=",
"left":"turn",
"right":0
}
},
"right":{
"op":"=",
"left":"d",
"right":0
}
},
"right":{
"op":"=",
"left":"i",
"right":0
}
}
},
"automata":[
{
"name":"parties",
"locations":[
{
"name":"location"
}
],
"initial-locations":[
"location"
],
"edges":[
{
"location":"location",
"action":"tau__",
"guard":{
"exp":{
"op":"∧",
"left":{
"op":"∧",
"left":{
"op":"=",
"left":"turn",
"right":0
},
"right":{
"op":"<",
"left":"mA",
"right":10
}
},
"right":{
"op":"=",
"left":"d",
"right":0
}
}
},
"destinations":[
{
"probability":{
"exp":1
},
"location":"location",
"assignments":[
{
"ref":"turn",
"value":1
},
{
"ref":"mA",
"value":{
"op":"+",
"left":"mA",
"right":1
}
}
],
"observables":[
]
}
]
},
{
"location":"location",
"action":"tau__",
"guard":{
"exp":{
"op":"∧",
"left":{
"op":"∧",
"left":{
"op":"=",
"left":"turn",
"right":1
},
"right":{
"op":"<",
"left":"mA",
"right":10
}
},
"right":{
"op":"=",
"left":"d",
"right":0
}
}
},
"destinations":[
{
"probability":{
"exp":1
},
"location":"location",
"assignments":[
{
"ref":"turn",
"value":0
},
{
"ref":"mB",
"value":"mA"
}
],
"observables":[
]
}
]
}
]
},
{
"name":"date",
"locations":[
{
"name":"location"
}
],
"initial-locations":[
"location"
],
"edges":[
{
"location":"location",
"action":"tau__",
"guard":{
"exp":{
"op":"=",
"left":"d",
"right":0
}
},
"destinations":[
{
"probability":{
"exp":1
},
"location":"location",
"assignments":[
{
"ref":"d",
"value":1
}
],
"observables":[
]
}
]
}
]
},
{
"name":"third_party",
"locations":[
{
"name":"location"
}
],
"initial-locations":[
"location"
],
"edges":[
{
"location":"location",
"action":"tau__",
"guard":{
"exp":{
"op":"∧",
"left":{
"op":"=",
"left":"i",
"right":0
},
"right":{
"op":"=",
"left":"d",
"right":1
}
}
},
"destinations":[
{
"probability":{
"exp":{
"op":"/",
"left":1,
"right":10
}
},
"location":"location",
"assignments":[
{
"ref":"i",
"value":1
}
],
"observables":[
]
},
{
"probability":{
"exp":{
"op":"/",
"left":1,
"right":10
}
},
"location":"location",
"assignments":[
{
"ref":"i",
"value":2
}
],
"observables":[
]
},
{
"probability":{
"exp":{
"op":"/",
"left":1,
"right":10
}
},
"location":"location",
"assignments":[
{
"ref":"i",
"value":3
}
],
"observables":[
]
},
{
"probability":{
"exp":{
"op":"/",
"left":1,
"right":10
}
},
"location":"location",
"assignments":[
{
"ref":"i",
"value":4
}
],
"observables":[
]
},
{
"probability":{
"exp":{
"op":"/",
"left":1,
"right":10
}
},
"location":"location",
"assignments":[
{
"ref":"i",
"value":5
}
],
"observables":[
]
},
{
"probability":{
"exp":{
"op":"/",
"left":1,
"right":10
}
},
"location":"location",
"assignments":[
{
"ref":"i",
"value":6
}
],
"observables":[
]
},
{
"probability":{
"exp":{
"op":"/",
"left":1,
"right":10
}
},
"location":"location",
"assignments":[
{
"ref":"i",
"value":7
}
],
"observables":[
]
},
{
"probability":{
"exp":{
"op":"/",
"left":1,
"right":10
}
},
"location":"location",
"assignments":[
{
"ref":"i",
"value":8
}
],
"observables":[
]
},
{
"probability":{
"exp":{
"op":"/",
"left":1,
"right":10
}
},
"location":"location",
"assignments":[
{
"ref":"i",
"value":9
}
],
"observables":[
]
},
{
"probability":{
"exp":{
"op":"/",
"left":1,
"right":10
}
},
"location":"location",
"assignments":[
{
"ref":"i",
"value":10
}
],
"observables":[
]
}
]
}
]
}
],
"system":{
"elements":[
{
"automaton":"parties"
},
{
"automaton":"date"
},
{
"automaton":"third_party"
}
],
"syncs":[
{
"synchronise":[
"tau__",
null,
null
],
"result":"tau__"
},
{
"synchronise":[
null,
"tau__",
null
],
"result":"tau__"
},
{
"synchronise":[
null,
null,
"tau__"
],
"result":"tau__"
}
]
}
}

6102
examples/exported-jani-models/fgf.jani
File diff suppressed because it is too large
View File

214
examples/exported-jani-models/firewire_abs.jani
View File

@ -1,214 +0,0 @@
{
"jani-version":1,
"features":[
"derived-operators"
],
"name":"Converted from PRISM by IscasMC",
"type":"mdp",
"actions":[
{
"name":"time"
},
{
"name":"round"
}
],
"constants":[
{
"name":"delay",
"type":"int"
},
{
"name":"fast",
"type":"real"
}
],
"variables":[
{
"name":"x",
"type":{
"kind":"bounded",
"base":"int",
"lower-bound":0,
"upper-bound":{
"op":"+",
"left":167,
"right":1
}
}
},
{
"name":"s",
"type":{
"kind":"bounded",
"base":"int",
"lower-bound":0,
"upper-bound":9
}
}
],
"observables":[
{
"name":"\"time\""
},
{
"name":"\"rounds\""
}
],
"initial-states":{
"exp":{
"op":"∧",
"left":{
"op":"=",
"left":"x",
"right":0
},
"right":{
"op":"=",
"left":"s",
"right":0
}
}
},
"automata":[
{
"name":"abstract_firewire",
"locations":[
{
"name":"location"
}
],
"initial-locations":[
"location"
],
"edges":[
{
"location":"location",
"action":"time",
"guard":{
"exp":{
"op":"∧",
"left":{
"op":"=",
"left":"s",
"right":0
},
"right":{
"op":"<",
"left":"x",
"right":"delay"
}
}
},
"destinations":[
{
"probability":{
"exp":1
},
"location":"location",
"assignments":[
{
"ref":"x",
"value":{
"op":"min",
"left":{
"op":"+",
"left":"x",
"right":1
},
"right":{
"op":"+",
"left":167,
"right":1
}
}
}
],
"observables":[
{
"ref":"\"time\"",
"value":1
}
]
}
]
},
{
"location":"location",
"action":"round",
"guard":{
"exp":{
"op":"=",
"left":"s",
"right":0
}
},
"destinations":[
{
"probability":{
"exp":"fast"
},
"location":"location",
"assignments":[
{
"ref":"s",
"value":1
}
],
"observables":[
{
"ref":"\"rounds\"",
"value":1
}
]
},
{
"probability":{
"exp":{
"op":"-",
"left":1,
"right":"fast"
}
},
"location":"location",
"assignments":[
{
"ref":"s",
"value":4
}
],
"observables":[
{
"ref":"\"rounds\"",
"value":1
}
]
}
]
}
]
}
],
"system":{
"elements":[
{
"automaton":"abstract_firewire"
}
],
"syncs":[
{
"synchronise":[
"time"
],
"result":"time"
},
{
"synchronise":[
"round"
],
"result":"round"
}
]
}
}

5013
examples/exported-jani-models/firewire_impl.jani
File diff suppressed because it is too large
View File

3456
examples/exported-jani-models/fms.jani
File diff suppressed because it is too large
View File

16360
examples/exported-jani-models/gossip4.jani
File diff suppressed because it is too large
View File

928
examples/exported-jani-models/graph4.jani
View File

@ -1,928 +0,0 @@
{
"jani-version":1,
"features":[
"derived-operators"
],
"name":"Converted from PRISM by IscasMC",
"type":"mdp",
"actions":[
{
"name":"s12"
},
{
"name":"s13"
},
{
"name":"s14"
},
{
"name":"s23"
},
{
"name":"s24"
},
{
"name":"s34"
},
{
"name":"tau__"
}
],
"constants":[
{
"name":"p",
"type":"real"
}
],
"variables":[
{
"name":"pc",
"type":{
"kind":"bounded",
"base":"int",
"lower-bound":0,
"upper-bound":12
}
},
{
"name":"x12",
"type":"bool"
},
{
"name":"x13",
"type":"bool"
},
{
"name":"x14",
"type":"bool"
},
{
"name":"x23",
"type":"bool"
},
{
"name":"x24",
"type":"bool"
},
{
"name":"x34",
"type":"bool"
}
],
"observables":[
],
"initial-states":{
"exp":{
"op":"∧",
"left":{
"op":"∧",
"left":{
"op":"∧",
"left":{
"op":"∧",
"left":{
"op":"∧",
"left":{
"op":"∧",
"left":{
"op":"=",
"left":"pc",
"right":0
},
"right":{
"op":"=",
"left":"x12",
"right":false
}
},
"right":{
"op":"=",
"left":"x13",
"right":false
}
},
"right":{
"op":"=",
"left":"x14",
"right":false
}
},
"right":{
"op":"=",
"left":"x23",
"right":false
}
},
"right":{
"op":"=",
"left":"x24",
"right":false
}
},
"right":{
"op":"=",
"left":"x34",
"right":false
}
}
},
"automata":[
{
"name":"PC",
"locations":[
{
"name":"location"
}
],
"initial-locations":[
"location"
],
"edges":[
{
"location":"location",
"action":"s12",
"guard":{
"exp":{
"op":"=",
"left":"pc",
"right":0
}
},
"destinations":[
{
"probability":{
"exp":1
},
"location":"location",
"assignments":[
{
"ref":"pc",
"value":{
"op":"+",
"left":"pc",
"right":1
}
}
],
"observables":[
]
}
]
},
{
"location":"location",
"action":"s13",
"guard":{
"exp":{
"op":"=",
"left":"pc",
"right":1
}
},
"destinations":[
{
"probability":{
"exp":1
},
"location":"location",
"assignments":[
{
"ref":"pc",
"value":{
"op":"+",
"left":"pc",
"right":1
}
}
],
"observables":[
]
}
]
},
{
"location":"location",
"action":"s14",
"guard":{
"exp":{
"op":"=",
"left":"pc",
"right":2
}
},
"destinations":[
{
"probability":{
"exp":1
},
"location":"location",
"assignments":[
{
"ref":"pc",
"value":{
"op":"+",
"left":"pc",
"right":1
}
}
],
"observables":[
]
}
]
},
{
"location":"location",
"action":"s23",
"guard":{
"exp":{
"op":"=",
"left":"pc",
"right":3
}
},
"destinations":[
{
"probability":{
"exp":1
},
"location":"location",
"assignments":[
{
"ref":"pc",
"value":{
"op":"+",
"left":"pc",
"right":1
}
}
],
"observables":[
]
}
]
},
{
"location":"location",
"action":"s24",
"guard":{
"exp":{
"op":"=",
"left":"pc",
"right":4
}
},
"destinations":[
{
"probability":{
"exp":1
},
"location":"location",
"assignments":[
{
"ref":"pc",
"value":{
"op":"+",
"left":"pc",
"right":1
}
}
],
"observables":[
]
}
]
},
{
"location":"location",
"action":"s34",
"guard":{
"exp":{
"op":"=",
"left":"pc",
"right":5
}
},
"destinations":[
{
"probability":{
"exp":1
},
"location":"location",
"assignments":[
{
"ref":"pc",
"value":{
"op":"+",
"left":"pc",
"right":1
}
}
],
"observables":[
]
}
]
}
]
},
{
"name":"M12",
"locations":[
{
"name":"location"
}
],
"initial-locations":[
"location"
],
"edges":[
{
"location":"location",
"action":"s12",
"guard":{
"exp":true
},
"destinations":[
{
"probability":{
"exp":"p"
},
"location":"location",
"assignments":[
{
"ref":"x12",
"value":true
}
]
},
{
"probability":{
"exp":{
"op":"-",
"left":1,
"right":"p"
}
},
"location":"location",
"assignments":[
{
"ref":"x12",
"value":false
}
]
}
]
},
{
"location":"location",
"action":"tau__",
"guard":{
"exp":{
"op":"∧",
"left":{
"op":"∧",
"left":{
"op":"=",
"left":"pc",
"right":6
},
"right":{
"op":"¬",
"exp":"x12"
}
},
"right":{
"op":"∨",
"left":{
"op":"∨",
"left":false,
"right":{
"op":"∧",
"left":"x13",
"right":"x23"
}
},
"right":{
"op":"∧",
"left":"x14",
"right":"x24"
}
}
}
},
"destinations":[
{
"probability":{
"exp":1
},
"location":"location",
"assignments":[
{
"ref":"x12",
"value":true
}
],
"observables":[
]
}
]
}
]
},
{
"name":"M13",
"locations":[
{
"name":"location"
}
],
"initial-locations":[
"location"
],
"edges":[
{
"location":"location",
"action":"s13",
"guard":{
"exp":true
},
"destinations":[
{
"probability":{
"exp":"p"
},
"location":"location",
"assignments":[
{
"ref":"x13",
"value":true
}
]
},
{
"probability":{
"exp":{
"op":"-",
"left":1,
"right":"p"
}
},
"location":"location",
"assignments":[
{
"ref":"x13",
"value":false
}
]
}
]
}
]
},
{
"name":"M14",
"locations":[
{
"name":"location"
}
],
"initial-locations":[
"location"
],
"edges":[
{
"location":"location",
"action":"s14",
"guard":{
"exp":true
},
"destinations":[
{
"probability":{
"exp":"p"
},
"location":"location",
"assignments":[
{
"ref":"x14",
"value":true
}
]
},
{
"probability":{
"exp":{
"op":"-",
"left":1,
"right":"p"
}
},
"location":"location",
"assignments":[
{
"ref":"x14",
"value":false
}
]
}
]
}
]
},
{
"name":"M23",
"locations":[
{
"name":"location"
}
],
"initial-locations":[
"location"
],
"edges":[
{
"location":"location",
"action":"s23",
"guard":{
"exp":true
},
"destinations":[
{
"probability":{
"exp":"p"
},
"location":"location",
"assignments":[
{
"ref":"x23",
"value":true
}
]
},
{
"probability":{
"exp":{
"op":"-",
"left":1,
"right":"p"
}
},
"location":"location",
"assignments":[
{
"ref":"x23",
"value":false
}
]
}
]
},
{
"location":"location",
"action":"tau__",
"guard":{
"exp":{
"op":"∧",
"left":{
"op":"∧",
"left":{
"op":"=",
"left":"pc",
"right":6
},
"right":{
"op":"¬",
"exp":"x23"
}
},
"right":{
"op":"∨",
"left":{
"op":"∨",
"left":false,
"right":{
"op":"∧",
"left":"x12",
"right":"x13"
}
},
"right":{
"op":"∧",
"left":"x24",
"right":"x34"
}
}
}
},
"destinations":[
{
"probability":{
"exp":1
},
"location":"location",
"assignments":[
{
"ref":"x23",
"value":true
}
],
"observables":[
]
}
]
}
]
},
{
"name":"M24",
"locations":[
{
"name":"location"
}
],
"initial-locations":[
"location"
],
"edges":[
{
"location":"location",
"action":"s24",
"guard":{
"exp":true
},
"destinations":[
{
"probability":{
"exp":"p"
},
"location":"location",
"assignments":[
{
"ref":"x24",
"value":true
}
]
},
{
"probability":{
"exp":{
"op":"-",
"left":1,
"right":"p"
}
},
"location":"location",
"assignments":[
{
"ref":"x24",
"value":false
}
]
}
]
},
{
"location":"location",
"action":"tau__",
"guard":{
"exp":{
"op":"∧",
"left":{
"op":"∧",
"left":{
"op":"=",
"left":"pc",
"right":6
},
"right":{
"op":"¬",
"exp":"x24"
}
},
"right":{
"op":"∨",
"left":{
"op":"∨",
"left":false,
"right":{
"op":"∧",
"left":"x12",
"right":"x14"
}
},
"right":{
"op":"∧",
"left":"x23",
"right":"x34"
}
}
}
},
"destinations":[
{
"probability":{
"exp":1
},
"location":"location",
"assignments":[
{
"ref":"x24",
"value":true
}
],
"observables":[
]
}
]
}
]
},
{
"name":"M34",
"locations":[
{
"name":"location"
}
],
"initial-locations":[
"location"
],
"edges":[
{
"location":"location",
"action":"s34",
"guard":{
"exp":true
},
"destinations":[
{
"probability":{
"exp":"p"
},
"location":"location",
"assignments":[
{
"ref":"x34",
"value":true
}
]
},
{
"probability":{
"exp":{
"op":"-",
"left":1,
"right":"p"
}
},
"location":"location",
"assignments":[
{
"ref":"x34",
"value":false
}
]
}
]
}
]
}
],
"system":{
"elements":[
{
"automaton":"PC"
},
{
"automaton":"M12"
},
{
"automaton":"M13"
},
{
"automaton":"M14"
},
{
"automaton":"M23"
},
{
"automaton":"M24"
},
{
"automaton":"M34"
}
],
"syncs":[
{
"synchronise":[
"s34",
null,
null,
null,
null,
null,
"s34"
],
"result":"s34"
},
{
"synchronise":[
"s24",
null,
null,
null,
null,
"s24",
null
],
"result":"s24"
},
{
"synchronise":[
"s23",
null,
null,
null,
"s23",
null,
null
],
"result":"s23"
},
{
"synchronise":[
"s14",
null,
null,
"s14",
null,
null,
null
],
"result":"s14"
},
{
"synchronise":[
"s13",
null,
"s13",
null,
null,
null,
null
],
"result":"s13"
},
{
"synchronise":[
"s12",
"s12",
null,
null,
null,
null,
null
],
"result":"s12"
},
{
"synchronise":[
null,
"tau__",
null,
null,
null,
null,
null
],
"result":"tau__"
},
{
"synchronise":[
null,
null,
null,
null,
"tau__",
null,
null
],
"result":"tau__"
},
{
"synchronise":[
null,
null,
null,
null,
null,
"tau__",
null
],
"result":"tau__"
}
]
}
}

1094
examples/exported-jani-models/herman11.jani
File diff suppressed because it is too large
View File

1284
examples/exported-jani-models/herman13.jani
File diff suppressed because it is too large
View File

1474
examples/exported-jani-models/herman15.jani
File diff suppressed because it is too large
View File

1664
examples/exported-jani-models/herman17.jani
File diff suppressed because it is too large
View File

1854
examples/exported-jani-models/herman19.jani
File diff suppressed because it is too large
View File

2044
examples/exported-jani-models/herman21.jani
File diff suppressed because it is too large
View File

334
examples/exported-jani-models/herman3.jani
View File

@ -1,334 +0,0 @@
{
"jani-version":1,
"features":[
"derived-operators"
],
"name":"Converted from PRISM by IscasMC",
"type":"dtmc",
"actions":[
{
"name":"step"
}
],
"variables":[
{
"name":"x1",
"type":{
"kind":"bounded",
"base":"int",
"lower-bound":0,
"upper-bound":1
}
},
{
"name":"x2",
"type":{
"kind":"bounded",
"base":"int",
"lower-bound":0,
"upper-bound":1
}
},
{
"name":"x3",
"type":{
"kind":"bounded",
"base":"int",
"lower-bound":0,
"upper-bound":1
}
}
],
"observables":[
{
"name":"\"steps\""
}
],
"initial-states":{
"exp":true
},
"automata":[
{
"name":"process1",
"locations":[
{
"name":"location",
"observables":[
{
"ref":"\"steps\"",
"value":1
}
]
}
],
"initial-locations":[
"location"
],
"edges":[
{
"location":"location",
"action":"step",
"guard":{
"exp":{
"op":"=",
"left":"x1",
"right":"x3"
}
},
"destinations":[
{
"probability":{
"exp":0.5000000
},
"location":"location",
"assignments":[
{
"ref":"x1",
"value":0
}
],
"observables":[
]
},
{
"probability":{
"exp":{
"op":"-",
"left":1,
"right":0.5000000
}
},
"location":"location",
"assignments":[
{
"ref":"x1",
"value":1
}
],
"observables":[
]
}
]
},
{
"location":"location",
"action":"step",
"guard":{
"exp":{
"op":"¬",
"exp":{
"op":"=",
"left":"x1",
"right":"x3"
}
}
},
"destinations":[
{
"probability":{
"exp":1
},
"location":"location",
"assignments":[
{
"ref":"x1",
"value":"x3"
}
],
"observables":[
]
}
]
}
]
},
{
"name":"process2",
"locations":[
{
"name":"location"
}
],
"initial-locations":[
"location"
],
"edges":[
{
"location":"location",
"action":"step",
"guard":{
"exp":{
"op":"=",
"left":"x2",
"right":"x1"
}
},
"destinations":[
{
"probability":{
"exp":0.5000000
},
"location":"location",
"assignments":[
{
"ref":"x2",
"value":0
}
]
},
{
"probability":{
"exp":{
"op":"-",
"left":1,
"right":0.5000000
}
},
"location":"location",
"assignments":[
{
"ref":"x2",
"value":1
}
]
}
]
},
{
"location":"location",
"action":"step",
"guard":{
"exp":{
"op":"¬",
"exp":{
"op":"=",
"left":"x2",
"right":"x1"
}
}
},
"destinations":[
{
"probability":{
"exp":1
},
"location":"location",
"assignments":[
{
"ref":"x2",
"value":"x1"
}
]
}
]
}
]
},
{
"name":"process3",
"locations":[
{
"name":"location"
}
],
"initial-locations":[
"location"
],
"edges":[
{
"location":"location",
"action":"step",
"guard":{
"exp":{
"op":"=",
"left":"x3",
"right":"x2"
}
},
"destinations":[
{
"probability":{
"exp":0.5000000
},
"location":"location",
"assignments":[
{
"ref":"x3",
"value":0
}
]
},
{
"probability":{
"exp":{
"op":"-",
"left":1,
"right":0.5000000
}
},
"location":"location",
"assignments":[
{
"ref":"x3",
"value":1
}
]
}
]
},
{
"location":"location",
"action":"step",
"guard":{
"exp":{
"op":"¬",
"exp":{
"op":"=",
"left":"x3",
"right":"x2"
}
}
},
"destinations":[
{
"probability":{
"exp":1
},
"location":"location",
"assignments":[
{
"ref":"x3",
"value":"x2"
}
]
}
]
}
]
}
],
"system":{
"elements":[
{
"automaton":"process1"
},
{
"automaton":"process2"
},
{
"automaton":"process3"
}
],
"syncs":[
{
"synchronise":[
"step",
"step",
"step"
],
"result":"step"
}
]
}
}

524
examples/exported-jani-models/herman5.jani
View File

@ -1,524 +0,0 @@
{
"jani-version":1,
"features":[
"derived-operators"
],
"name":"Converted from PRISM by IscasMC",
"type":"dtmc",
"actions":[
{
"name":"step"
}
],
"variables":[
{
"name":"x1",
"type":{
"kind":"bounded",
"base":"int",
"lower-bound":0,
"upper-bound":1
}
},
{
"name":"x2",
"type":{
"kind":"bounded",
"base":"int",
"lower-bound":0,
"upper-bound":1
}
},
{
"name":"x3",
"type":{
"kind":"bounded",
"base":"int",
"lower-bound":0,
"upper-bound":1
}
},
{
"name":"x4",
"type":{
"kind":"bounded",
"base":"int",
"lower-bound":0,
"upper-bound":1
}
},
{
"name":"x5",
"type":{
"kind":"bounded",
"base":"int",
"lower-bound":0,
"upper-bound":1
}
}
],
"observables":[
{
"name":"\"steps\""
}
],
"initial-states":{
"exp":true
},
"automata":[
{
"name":"process1",
"locations":[
{
"name":"location",
"observables":[
{
"ref":"\"steps\"",
"value":1
}
]
}
],
"initial-locations":[
"location"
],
"edges":[
{
"location":"location",
"action":"step",
"guard":{
"exp":{
"op":"=",
"left":"x1",
"right":"x5"
}
},
"destinations":[
{
"probability":{
"exp":0.5000000
},
"location":"location",
"assignments":[
{
"ref":"x1",
"value":0
}
],
"observables":[
]
},
{
"probability":{
"exp":{
"op":"-",
"left":1,
"right":0.5000000
}
},
"location":"location",
"assignments":[
{
"ref":"x1",
"value":1
}
],
"observables":[
]
}
]
},
{
"location":"location",
"action":"step",
"guard":{
"exp":{
"op":"¬",
"exp":{
"op":"=",
"left":"x1",
"right":"x5"
}
}
},
"destinations":[
{
"probability":{
"exp":1
},
"location":"location",
"assignments":[
{
"ref":"x1",
"value":"x5"
}
],
"observables":[
]
}
]
}
]
},
{
"name":"process2",
"locations":[
{
"name":"location"
}
],
"initial-locations":[
"location"
],
"edges":[
{
"location":"location",
"action":"step",
"guard":{
"exp":{
"op":"=",
"left":"x2",
"right":"x1"
}
},
"destinations":[
{
"probability":{
"exp":0.5000000
},
"location":"location",
"assignments":[
{
"ref":"x2",
"value":0
}
]
},
{
"probability":{
"exp":{
"op":"-",
"left":1,
"right":0.5000000
}
},
"location":"location",
"assignments":[
{
"ref":"x2",
"value":1
}
]
}
]
},
{
"location":"location",
"action":"step",
"guard":{
"exp":{
"op":"¬",
"exp":{
"op":"=",
"left":"x2",
"right":"x1"
}
}
},
"destinations":[
{
"probability":{
"exp":1
},
"location":"location",
"assignments":[
{
"ref":"x2",
"value":"x1"
}
]
}
]
}
]
},
{
"name":"process3",
"locations":[
{
"name":"location"
}
],
"initial-locations":[
"location"
],
"edges":[
{
"location":"location",
"action":"step",
"guard":{
"exp":{
"op":"=",
"left":"x3",
"right":"x2"
}
},
"destinations":[
{
"probability":{
"exp":0.5000000
},
"location":"location",
"assignments":[
{
"ref":"x3",
"value":0
}
]
},
{
"probability":{
"exp":{
"op":"-",
"left":1,
"right":0.5000000
}
},
"location":"location",
"assignments":[
{
"ref":"x3",
"value":1
}
]
}
]
},
{
"location":"location",
"action":"step",
"guard":{
"exp":{
"op":"¬",
"exp":{
"op":"=",
"left":"x3",
"right":"x2"
}
}
},
"destinations":[
{
"probability":{
"exp":1
},
"location":"location",
"assignments":[
{
"ref":"x3",
"value":"x2"
}
]
}
]
}
]
},
{
"name":"process4",
"locations":[
{
"name":"location"
}
],
"initial-locations":[
"location"
],
"edges":[
{
"location":"location",
"action":"step",
"guard":{
"exp":{
"op":"=",
"left":"x4",
"right":"x3"
}
},
"destinations":[
{
"probability":{
"exp":0.5000000
},
"location":"location",
"assignments":[
{
"ref":"x4",
"value":0
}
]
},
{
"probability":{
"exp":{
"op":"-",
"left":1,
"right":0.5000000
}
},
"location":"location",
"assignments":[
{
"ref":"x4",
"value":1
}
]
}
]
},
{
"location":"location",
"action":"step",
"guard":{
"exp":{
"op":"¬",
"exp":{
"op":"=",
"left":"x4",
"right":"x3"
}
}
},
"destinations":[
{
"probability":{
"exp":1
},
"location":"location",
"assignments":[
{
"ref":"x4",
"value":"x3"
}
]
}
]
}
]
},
{
"name":"process5",
"locations":[
{
"name":"location"
}
],
"initial-locations":[
"location"
],
"edges":[
{
"location":"location",
"action":"step",
"guard":{
"exp":{
"op":"=",
"left":"x5",
"right":"x4"
}
},
"destinations":[
{
"probability":{
"exp":0.5000000
},
"location":"location",
"assignments":[
{
"ref":"x5",
"value":0
}
]
},
{
"probability":{
"exp":{
"op":"-",
"left":1,
"right":0.5000000
}
},
"location":"location",
"assignments":[
{
"ref":"x5",
"value":1
}
]
}
]
},
{
"location":"location",
"action":"step",
"guard":{
"exp":{
"op":"¬",
"exp":{
"op":"=",
"left":"x5",
"right":"x4"
}
}
},
"destinations":[
{
"probability":{
"exp":1
},
"location":"location",
"assignments":[
{
"ref":"x5",
"value":"x4"
}
]
}
]
}
]
}
],
"system":{
"elements":[
{
"automaton":"process1"
},
{
"automaton":"process2"
},
{
"automaton":"process3"
},
{
"automaton":"process4"
},
{
"automaton":"process5"
}
],
"syncs":[
{
"synchronise":[
"step",
"step",
"step",
"step",
"step"
],
"result":"step"
}
]
}
}

714
examples/exported-jani-models/herman7.jani
View File

@ -1,714 +0,0 @@
{
"jani-version":1,
"features":[
"derived-operators"
],
"name":"Converted from PRISM by IscasMC",
"type":"dtmc",
"actions":[
{
"name":"step"
}
],
"variables":[
{
"name":"x1",
"type":{
"kind":"bounded",
"base":"int",
"lower-bound":0,
"upper-bound":1
}
},
{
"name":"x2",
"type":{
"kind":"bounded",
"base":"int",
"lower-bound":0,
"upper-bound":1
}
},
{
"name":"x3",
"type":{
"kind":"bounded",
"base":"int",
"lower-bound":0,
"upper-bound":1
}
},
{
"name":"x4",
"type":{
"kind":"bounded",
"base":"int",
"lower-bound":0,
"upper-bound":1
}
},
{
"name":"x5",
"type":{
"kind":"bounded",
"base":"int",
"lower-bound":0,
"upper-bound":1
}
},
{
"name":"x6",
"type":{
"kind":"bounded",
"base":"int",
"lower-bound":0,
"upper-bound":1
}
},
{
"name":"x7",
"type":{
"kind":"bounded",
"base":"int",
"lower-bound":0,
"upper-bound":1
}
}
],
"observables":[
{
"name":"\"steps\""
}
],
"initial-states":{
"exp":true
},
"automata":[
{
"name":"process1",
"locations":[
{
"name":"location",
"observables":[
{
"ref":"\"steps\"",
"value":1
}
]
}
],
"initial-locations":[
"location"
],
"edges":[
{
"location":"location",
"action":"step",
"guard":{
"exp":{
"op":"=",
"left":"x1",
"right":"x7"
}
},
"destinations":[
{
"probability":{
"exp":0.5000000
},
"location":"location",
"assignments":[
{
"ref":"x1",
"value":0
}
],
"observables":[
]
},
{
"probability":{
"exp":{
"op":"-",
"left":1,
"right":0.5000000
}
},
"location":"location",
"assignments":[
{
"ref":"x1",
"value":1
}
],
"observables":[
]
}
]
},
{
"location":"location",
"action":"step",
"guard":{
"exp":{
"op":"¬",
"exp":{
"op":"=",
"left":"x1",
"right":"x7"
}
}
},
"destinations":[
{
"probability":{
"exp":1
},
"location":"location",
"assignments":[
{
"ref":"x1",
"value":"x7"
}
],
"observables":[
]
}
]
}
]
},
{
"name":"process2",
"locations":[
{
"name":"location"
}
],
"initial-locations":[
"location"
],
"edges":[
{
"location":"location",
"action":"step",
"guard":{
"exp":{
"op":"=",
"left":"x2",
"right":"x1"
}
},
"destinations":[
{
"probability":{
"exp":0.5000000
},
"location":"location",
"assignments":[
{
"ref":"x2",
"value":0
}
]
},
{
"probability":{
"exp":{
"op":"-",
"left":1,
"right":0.5000000
}
},
"location":"location",
"assignments":[
{
"ref":"x2",
"value":1
}
]
}
]
},
{
"location":"location",
"action":"step",
"guard":{
"exp":{
"op":"¬",
"exp":{
"op":"=",
"left":"x2",
"right":"x1"
}
}
},
"destinations":[
{
"probability":{
"exp":1
},
"location":"location",
"assignments":[
{
"ref":"x2",
"value":"x1"
}
]
}
]
}
]
},
{
"name":"process3",
"locations":[
{
"name":"location"
}
],
"initial-locations":[
"location"
],
"edges":[
{
"location":"location",
"action":"step",
"guard":{
"exp":{
"op":"=",
"left":"x3",
"right":"x2"
}
},
"destinations":[
{
"probability":{
"exp":0.5000000
},
"location":"location",
"assignments":[
{
"ref":"x3",
"value":0
}
]
},
{
"probability":{
"exp":{
"op":"-",
"left":1,
"right":0.5000000
}
},
"location":"location",
"assignments":[
{
"ref":"x3",
"value":1
}
]
}
]
},
{
"location":"location",
"action":"step",
"guard":{
"exp":{
"op":"¬",
"exp":{
"op":"=",
"left":"x3",
"right":"x2"
}
}
},
"destinations":[
{
"probability":{
"exp":1
},
"location":"location",
"assignments":[
{
"ref":"x3",
"value":"x2"
}
]
}
]
}
]
},
{
"name":"process4",
"locations":[
{
"name":"location"
}
],
"initial-locations":[
"location"
],
"edges":[
{
"location":"location",
"action":"step",
"guard":{
"exp":{
"op":"=",
"left":"x4",
"right":"x3"
}
},
"destinations":[
{
"probability":{
"exp":0.5000000
},
"location":"location",
"assignments":[
{
"ref":"x4",
"value":0
}
]
},
{
"probability":{
"exp":{
"op":"-",
"left":1,
"right":0.5000000
}
},
"location":"location",
"assignments":[
{
"ref":"x4",
"value":1
}
]
}
]
},
{
"location":"location",
"action":"step",
"guard":{
"exp":{
"op":"¬",
"exp":{
"op":"=",
"left":"x4",
"right":"x3"
}
}
},
"destinations":[
{
"probability":{
"exp":1
},
"location":"location",
"assignments":[
{
"ref":"x4",
"value":"x3"
}
]
}
]
}
]
},
{
"name":"process5",
"locations":[
{
"name":"location"
}
],
"initial-locations":[
"location"
],
"edges":[
{
"location":"location",
"action":"step",
"guard":{
"exp":{
"op":"=",
"left":"x5",
"right":"x4"
}
},
"destinations":[
{
"probability":{
"exp":0.5000000
},
"location":"location",
"assignments":[
{
"ref":"x5",
"value":0
}
]
},
{
"probability":{
"exp":{
"op":"-",
"left":1,
"right":0.5000000
}
},
"location":"location",
"assignments":[
{
"ref":"x5",
"value":1
}
]
}
]
},
{
"location":"location",
"action":"step",
"guard":{
"exp":{
"op":"¬",
"exp":{
"op":"=",
"left":"x5",
"right":"x4"
}
}
},
"destinations":[
{
"probability":{
"exp":1
},
"location":"location",
"assignments":[
{
"ref":"x5",
"value":"x4"
}
]
}
]
}
]
},
{
"name":"process6",
"locations":[
{
"name":"location"
}
],
"initial-locations":[
"location"
],
"edges":[
{
"location":"location",
"action":"step",
"guard":{
"exp":{
"op":"=",
"left":"x6",
"right":"x5"
}
},
"destinations":[
{
"probability":{
"exp":0.5000000
},
"location":"location",
"assignments":[
{
"ref":"x6",
"value":0
}
]
},
{
"probability":{
"exp":{
"op":"-",
"left":1,
"right":0.5000000
}
},
"location":"location",
"assignments":[
{
"ref":"x6",
"value":1
}
]
}
]
},
{
"location":"location",
"action":"step",
"guard":{
"exp":{
"op":"¬",
"exp":{
"op":"=",
"left":"x6",
"right":"x5"
}
}
},
"destinations":[
{
"probability":{
"exp":1
},
"location":"location",
"assignments":[
{
"ref":"x6",
"value":"x5"
}
]
}
]
}
]
},
{
"name":"process7",
"locations":[
{
"name":"location"
}
],
"initial-locations":[
"location"
],
"edges":[
{
"location":"location",
"action":"step",
"guard":{
"exp":{
"op":"=",
"left":"x7",
"right":"x6"
}
},
"destinations":[
{
"probability":{
"exp":0.5000000
},
"location":"location",
"assignments":[
{
"ref":"x7",
"value":0
}
]
},
{
"probability":{
"exp":{
"op":"-",
"left":1,
"right":0.5000000
}
},
"location":"location",
"assignments":[
{
"ref":"x7",
"value":1
}
]
}
]
},
{
"location":"location",
"action":"step",
"guard":{
"exp":{
"op":"¬",
"exp":{
"op":"=",
"left":"x7",
"right":"x6"
}
}
},
"destinations":[
{
"probability":{
"exp":1
},
"location":"location",
"assignments":[
{
"ref":"x7",
"value":"x6"
}
]
}
]
}
]
}
],
"system":{
"elements":[
{
"automaton":"process1"
},
{
"automaton":"process2"
},
{
"automaton":"process3"
},
{
"automaton":"process4"
},
{
"automaton":"process5"
},
{
"automaton":"process6"
},
{
"automaton":"process7"
}
],
"syncs":[
{
"synchronise":[
"step",
"step",
"step",
"step",
"step",
"step",
"step"
],
"result":"step"
}
]
}
}

904
examples/exported-jani-models/herman9.jani
View File

@ -1,904 +0,0 @@
{
"jani-version":1,
"features":[
"derived-operators"
],
"name":"Converted from PRISM by IscasMC",
"type":"dtmc",
"actions":[
{
"name":"step"
}
],
"variables":[
{
"name":"x1",
"type":{
"kind":"bounded",
"base":"int",
"lower-bound":0,
"upper-bound":1
}
},
{
"name":"x2",
"type":{
"kind":"bounded",
"base":"int",
"lower-bound":0,
"upper-bound":1
}
},
{
"name":"x3",
"type":{
"kind":"bounded",
"base":"int",
"lower-bound":0,
"upper-bound":1
}
},
{
"name":"x4",
"type":{
"kind":"bounded",
"base":"int",
"lower-bound":0,
"upper-bound":1
}
},
{
"name":"x5",
"type":{
"kind":"bounded",
"base":"int",
"lower-bound":0,
"upper-bound":1
}
},
{
"name":"x6",
"type":{
"kind":"bounded",
"base":"int",
"lower-bound":0,
"upper-bound":1
}
},
{
"name":"x7",
"type":{
"kind":"bounded",
"base":"int",
"lower-bound":0,
"upper-bound":1
}
},
{
"name":"x8",
"type":{
"kind":"bounded",
"base":"int",
"lower-bound":0,
"upper-bound":1
}
},
{
"name":"x9",
"type":{
"kind":"bounded",
"base":"int",
"lower-bound":0,
"upper-bound":1
}
}
],
"observables":[
{
"name":"\"steps\""
}
],
"initial-states":{
"exp":true
},
"automata":[
{
"name":"process1",
"locations":[
{
"name":"location",
"observables":[
{
"ref":"\"steps\"",
"value":1
}
]
}
],
"initial-locations":[
"location"
],
"edges":[
{
"location":"location",
"action":"step",
"guard":{
"exp":{
"op":"=",
"left":"x1",
"right":"x9"
}
},
"destinations":[
{
"probability":{
"exp":0.5000000
},
"location":"location",
"assignments":[
{
"ref":"x1",
"value":0
}
],
"observables":[
]
},
{
"probability":{
"exp":{
"op":"-",
"left":1,
"right":0.5000000
}
},
"location":"location",
"assignments":[
{
"ref":"x1",
"value":1
}
],
"observables":[
]
}
]
},
{
"location":"location",
"action":"step",
"guard":{
"exp":{
"op":"¬",
"exp":{
"op":"=",
"left":"x1",
"right":"x9"
}
}
},
"destinations":[
{
"probability":{
"exp":1
},
"location":"location",
"assignments":[
{
"ref":"x1",
"value":"x9"
}
],
"observables":[
]
}
]
}
]
},
{
"name":"process2",
"locations":[
{
"name":"location"
}
],
"initial-locations":[
"location"
],
"edges":[
{
"location":"location",
"action":"step",
"guard":{
"exp":{
"op":"=",
"left":"x2",
"right":"x1"
}
},
"destinations":[
{
"probability":{
"exp":0.5000000
},
"location":"location",
"assignments":[
{
"ref":"x2",
"value":0
}
]
},
{
"probability":{
"exp":{
"op":"-",
"left":1,
"right":0.5000000
}
},
"location":"location",
"assignments":[
{
"ref":"x2",
"value":1
}
]
}
]
},
{
"location":"location",
"action":"step",
"guard":{
"exp":{
"op":"¬",
"exp":{
"op":"=",
"left":"x2",
"right":"x1"
}
}
},
"destinations":[
{
"probability":{
"exp":1
},
"location":"location",
"assignments":[
{
"ref":"x2",
"value":"x1"
}
]
}
]
}
]
},
{
"name":"process3",
"locations":[
{
"name":"location"
}
],
"initial-locations":[
"location"
],
"edges":[
{
"location":"location",
"action":"step",
"guard":{
"exp":{
"op":"=",
"left":"x3",
"right":"x2"
}
},
"destinations":[
{
"probability":{
"exp":0.5000000
},
"location":"location",
"assignments":[
{
"ref":"x3",
"value":0
}
]
},
{
"probability":{
"exp":{
"op":"-",
"left":1,
"right":0.5000000
}
},
"location":"location",
"assignments":[
{
"ref":"x3",
"value":1
}
]
}
]
},
{
"location":"location",
"action":"step",
"guard":{
"exp":{
"op":"¬",
"exp":{
"op":"=",
"left":"x3",
"right":"x2"
}
}
},
"destinations":[
{
"probability":{
"exp":1
},
"location":"location",
"assignments":[
{
"ref":"x3",
"value":"x2"
}
]
}
]
}
]
},
{
"name":"process4",
"locations":[
{
"name":"location"
}
],
"initial-locations":[
"location"
],
"edges":[
{
"location":"location",
"action":"step",
"guard":{
"exp":{
"op":"=",
"left":"x4",
"right":"x3"
}
},
"destinations":[
{
"probability":{
"exp":0.5000000
},
"location":"location",
"assignments":[
{
"ref":"x4",
"value":0
}
]
},
{
"probability":{
"exp":{
"op":"-",
"left":1,
"right":0.5000000
}
},
"location":"location",
"assignments":[
{
"ref":"x4",
"value":1
}
]
}
]
},
{
"location":"location",
"action":"step",
"guard":{
"exp":{
"op":"¬",
"exp":{
"op":"=",
"left":"x4",
"right":"x3"
}
}
},
"destinations":[
{
"probability":{
"exp":1
},
"location":"location",
"assignments":[
{
"ref":"x4",
"value":"x3"
}
]
}
]
}
]
},
{
"name":"process5",
"locations":[
{
"name":"location"
}
],
"initial-locations":[
"location"
],
"edges":[
{
"location":"location",
"action":"step",
"guard":{
"exp":{
"op":"=",
"left":"x5",
"right":"x4"
}
},
"destinations":[
{
"probability":{
"exp":0.5000000
},
"location":"location",
"assignments":[
{
"ref":"x5",
"value":0
}
]
},
{
"probability":{
"exp":{
"op":"-",
"left":1,
"right":0.5000000
}
},
"location":"location",
"assignments":[
{
"ref":"x5",
"value":1
}
]
}
]
},
{
"location":"location",
"action":"step",
"guard":{
"exp":{
"op":"¬",
"exp":{
"op":"=",
"left":"x5",
"right":"x4"
}
}
},
"destinations":[
{
"probability":{
"exp":1
},
"location":"location",
"assignments":[
{
"ref":"x5",
"value":"x4"
}
]
}
]
}
]
},
{
"name":"process6",
"locations":[
{
"name":"location"
}
],
"initial-locations":[
"location"
],
"edges":[
{
"location":"location",
"action":"step",
"guard":{
"exp":{
"op":"=",
"left":"x6",
"right":"x5"
}
},
"destinations":[
{
"probability":{
"exp":0.5000000
},
"location":"location",
"assignments":[
{
"ref":"x6",
"value":0
}
]
},
{
"probability":{
"exp":{
"op":"-",
"left":1,
"right":0.5000000
}
},
"location":"location",
"assignments":[
{
"ref":"x6",
"value":1
}
]
}
]
},
{
"location":"location",
"action":"step",
"guard":{
"exp":{
"op":"¬",
"exp":{
"op":"=",
"left":"x6",
"right":"x5"
}
}
},
"destinations":[
{
"probability":{
"exp":1
},
"location":"location",
"assignments":[
{
"ref":"x6",
"value":"x5"
}
]
}
]
}
]
},
{
"name":"process7",
"locations":[
{
"name":"location"
}
],
"initial-locations":[
"location"
],
"edges":[
{
"location":"location",
"action":"step",
"guard":{
"exp":{
"op":"=",
"left":"x7",
"right":"x6"
}
},
"destinations":[
{
"probability":{
"exp":0.5000000
},
"location":"location",
"assignments":[
{
"ref":"x7",
"value":0
}
]
},
{
"probability":{
"exp":{
"op":"-",
"left":1,
"right":0.5000000
}
},
"location":"location",
"assignments":[
{
"ref":"x7",
"value":1
}
]
}
]
},
{
"location":"location",
"action":"step",
"guard":{
"exp":{
"op":"¬",
"exp":{
"op":"=",
"left":"x7",
"right":"x6"
}
}
},
"destinations":[
{
"probability":{
"exp":1
},
"location":"location",
"assignments":[
{
"ref":"x7",
"value":"x6"
}
]
}
]
}
]
},
{
"name":"process8",
"locations":[
{
"name":"location"
}
],
"initial-locations":[
"location"
],
"edges":[
{
"location":"location",
"action":"step",
"guard":{
"exp":{
"op":"=",
"left":"x8",
"right":"x7"
}
},
"destinations":[
{
"probability":{
"exp":0.5000000
},
"location":"location",
"assignments":[
{
"ref":"x8",
"value":0
}
]
},
{
"probability":{
"exp":{
"op":"-",
"left":1,
"right":0.5000000
}
},
"location":"location",
"assignments":[
{
"ref":"x8",
"value":1
}
]
}
]
},
{
"location":"location",
"action":"step",
"guard":{
"exp":{
"op":"¬",
"exp":{
"op":"=",
"left":"x8",
"right":"x7"
}
}
},
"destinations":[
{
"probability":{
"exp":1
},
"location":"location",
"assignments":[
{
"ref":"x8",
"value":"x7"
}
]
}
]
}
]
},
{
"name":"process9",
"locations":[
{
"name":"location"
}
],
"initial-locations":[
"location"
],
"edges":[
{
"location":"location",
"action":"step",
"guard":{
"exp":{
"op":"=",
"left":"x9",
"right":"x8"
}
},
"destinations":[
{
"probability":{
"exp":0.5000000
},
"location":"location",
"assignments":[
{
"ref":"x9",
"value":0
}
]
},
{
"probability":{
"exp":{
"op":"-",
"left":1,
"right":0.5000000
}
},
"location":"location",
"assignments":[
{
"ref":"x9",
"value":1
}
]
}
]
},
{
"location":"location",
"action":"step",
"guard":{
"exp":{
"op":"¬",
"exp":{
"op":"=",
"left":"x9",
"right":"x8"
}
}
},
"destinations":[
{
"probability":{
"exp":1
},
"location":"location",
"assignments":[
{
"ref":"x9",
"value":"x8"
}
]
}
]
}
]
}
],
"system":{
"elements":[
{
"automaton":"process1"
},
{
"automaton":"process2"
},
{
"automaton":"process3"
},
{
"automaton":"process4"
},
{
"automaton":"process5"
},
{
"automaton":"process6"
},
{
"automaton":"process7"
},
{
"automaton":"process8"
},
{
"automaton":"process9"
}
],
"syncs":[
{
"synchronise":[
"step",
"step",
"step",
"step",
"step",
"step",
"step",
"step",
"step"
],
"result":"step"
}
]
}
}

968
examples/exported-jani-models/ij10.jani
View File

@ -1,968 +0,0 @@
{
"jani-version":1,
"features":[
"derived-operators"
],
"name":"Converted from PRISM by IscasMC",
"type":"mdp",
"actions":[
{
"name":"tau__"
}
],
"variables":[
{
"name":"q1",
"type":{
"kind":"bounded",
"base":"int",
"lower-bound":0,
"upper-bound":1
}
},
{
"name":"q2",
"type":{
"kind":"bounded",
"base":"int",
"lower-bound":0,
"upper-bound":1
}
},
{
"name":"q3",
"type":{
"kind":"bounded",
"base":"int",
"lower-bound":0,
"upper-bound":1
}
},
{
"name":"q4",
"type":{
"kind":"bounded",
"base":"int",
"lower-bound":0,
"upper-bound":1
}
},
{
"name":"q5",
"type":{
"kind":"bounded",
"base":"int",
"lower-bound":0,
"upper-bound":1
}
},
{
"name":"q6",
"type":{
"kind":"bounded",
"base":"int",
"lower-bound":0,
"upper-bound":1
}
},
{
"name":"q7",
"type":{
"kind":"bounded",
"base":"int",
"lower-bound":0,
"upper-bound":1
}
},
{
"name":"q8",
"type":{
"kind":"bounded",
"base":"int",
"lower-bound":0,
"upper-bound":1
}
},
{
"name":"q9",
"type":{
"kind":"bounded",
"base":"int",
"lower-bound":0,
"upper-bound":1
}
},
{
"name":"q10",
"type":{
"kind":"bounded",
"base":"int",
"lower-bound":0,
"upper-bound":1
}
}
],
"observables":[
{
"name":"\"steps\""
}
],
"initial-states":{
"exp":{
"op":"≥",
"left":{
"op":"+",
"left":{
"op":"+",
"left":{
"op":"+",
"left":{
"op":"+",
"left":{
"op":"+",
"left":{
"op":"+",
"left":{
"op":"+",
"left":{
"op":"+",
"left":{
"op":"+",
"left":"q1",
"right":"q2"
},
"right":"q3"
},
"right":"q4"
},
"right":"q5"
},
"right":"q6"
},
"right":"q7"
},
"right":"q8"
},
"right":"q9"
},
"right":"q10"
},
"right":1
}
},
"automata":[
{
"name":"process1",
"locations":[
{
"name":"location",
"observables":[
{
"ref":"\"steps\"",
"value":1
}
]
}
],
"initial-locations":[
"location"
],
"edges":[
{
"location":"location",
"action":"tau__",
"guard":{
"exp":{
"op":"=",
"left":"q1",
"right":1
}
},
"destinations":[
{
"probability":{
"exp":0.5000000
},
"location":"location",
"assignments":[
{
"ref":"q1",
"value":0
},
{
"ref":"q10",
"value":1
}
],
"observables":[
]
},
{
"probability":{
"exp":0.5000000
},
"location":"location",
"assignments":[
{
"ref":"q1",
"value":0
},
{
"ref":"q2",
"value":1
}
],
"observables":[
]
}
]
}
]
},
{
"name":"process2",
"locations":[
{
"name":"location"
}
],
"initial-locations":[
"location"
],
"edges":[
{
"location":"location",
"action":"tau__",
"guard":{
"exp":{
"op":"=",
"left":"q2",
"right":1
}
},
"destinations":[
{
"probability":{
"exp":0.5000000
},
"location":"location",
"assignments":[
{
"ref":"q2",
"value":0
},
{
"ref":"q1",
"value":1
}
],
"observables":[
]
},
{
"probability":{
"exp":0.5000000
},
"location":"location",
"assignments":[
{
"ref":"q2",
"value":0
},
{
"ref":"q3",
"value":1
}
],
"observables":[
]
}
]
}
]
},
{
"name":"process3",
"locations":[
{
"name":"location"
}
],
"initial-locations":[
"location"
],
"edges":[
{
"location":"location",
"action":"tau__",
"guard":{
"exp":{
"op":"=",
"left":"q3",
"right":1
}
},
"destinations":[
{
"probability":{
"exp":0.5000000
},
"location":"location",
"assignments":[
{
"ref":"q3",
"value":0
},
{
"ref":"q2",
"value":1
}
],
"observables":[
]
},
{
"probability":{
"exp":0.5000000
},
"location":"location",
"assignments":[
{
"ref":"q3",
"value":0
},
{
"ref":"q4",
"value":1
}
],
"observables":[
]
}
]
}
]
},
{
"name":"process4",
"locations":[
{
"name":"location"
}
],
"initial-locations":[
"location"
],
"edges":[
{
"location":"location",
"action":"tau__",
"guard":{
"exp":{
"op":"=",
"left":"q4",
"right":1
}
},
"destinations":[
{
"probability":{
"exp":0.5000000
},
"location":"location",
"assignments":[
{
"ref":"q4",
"value":0
},
{
"ref":"q3",
"value":1
}
],
"observables":[
]
},
{
"probability":{
"exp":0.5000000
},
"location":"location",
"assignments":[
{
"ref":"q4",
"value":0
},
{
"ref":"q5",
"value":1
}
],
"observables":[
]
}
]
}
]
},
{
"name":"process5",
"locations":[
{
"name":"location"
}
],
"initial-locations":[
"location"
],
"edges":[
{
"location":"location",
"action":"tau__",
"guard":{
"exp":{
"op":"=",
"left":"q5",
"right":1
}
},
"destinations":[
{
"probability":{
"exp":0.5000000
},
"location":"location",
"assignments":[
{
"ref":"q5",
"value":0
},
{
"ref":"q4",
"value":1
}
],
"observables":[
]
},
{
"probability":{
"exp":0.5000000
},
"location":"location",
"assignments":[
{
"ref":"q5",
"value":0
},
{
"ref":"q6",
"value":1
}
],
"observables":[
]
}
]
}
]
},
{
"name":"process6",
"locations":[
{
"name":"location"
}
],
"initial-locations":[
"location"
],
"edges":[
{
"location":"location",
"action":"tau__",
"guard":{
"exp":{
"op":"=",
"left":"q6",
"right":1
}
},
"destinations":[
{
"probability":{
"exp":0.5000000
},
"location":"location",
"assignments":[
{
"ref":"q6",
"value":0
},
{
"ref":"q5",
"value":1
}
],
"observables":[
]
},
{
"probability":{
"exp":0.5000000
},
"location":"location",
"assignments":[
{
"ref":"q6",
"value":0
},
{
"ref":"q7",
"value":1
}
],
"observables":[
]
}
]
}
]
},
{
"name":"process7",
"locations":[
{
"name":"location"
}
],
"initial-locations":[
"location"
],
"edges":[
{
"location":"location",
"action":"tau__",
"guard":{
"exp":{
"op":"=",
"left":"q7",
"right":1
}
},
"destinations":[
{
"probability":{
"exp":0.5000000
},
"location":"location",
"assignments":[
{
"ref":"q7",
"value":0
},
{
"ref":"q6",
"value":1
}
],
"observables":[
]
},
{
"probability":{
"exp":0.5000000
},
"location":"location",
"assignments":[
{
"ref":"q7",
"value":0
},
{
"ref":"q8",
"value":1
}
],
"observables":[
]
}
]
}
]
},
{
"name":"process8",
"locations":[
{
"name":"location"
}
],
"initial-locations":[
"location"
],
"edges":[
{
"location":"location",
"action":"tau__",
"guard":{
"exp":{
"op":"=",
"left":"q8",
"right":1
}
},
"destinations":[
{
"probability":{
"exp":0.5000000
},
"location":"location",
"assignments":[
{
"ref":"q8",
"value":0
},
{
"ref":"q7",
"value":1
}
],
"observables":[
]
},
{
"probability":{
"exp":0.5000000
},
"location":"location",
"assignments":[
{
"ref":"q8",
"value":0
},
{
"ref":"q9",
"value":1
}
],
"observables":[
]
}
]
}
]
},
{
"name":"process9",
"locations":[
{
"name":"location"
}
],
"initial-locations":[
"location"
],
"edges":[
{
"location":"location",
"action":"tau__",
"guard":{
"exp":{
"op":"=",
"left":"q9",
"right":1
}
},
"destinations":[
{
"probability":{
"exp":0.5000000
},
"location":"location",
"assignments":[
{
"ref":"q9",
"value":0
},
{
"ref":"q8",
"value":1
}
],
"observables":[
]
},
{
"probability":{
"exp":0.5000000
},
"location":"location",
"assignments":[
{
"ref":"q9",
"value":0
},
{
"ref":"q10",
"value":1
}
],
"observables":[
]
}
]
}
]
},
{
"name":"process10",
"locations":[
{
"name":"location"
}
],
"initial-locations":[
"location"
],
"edges":[
{
"location":"location",
"action":"tau__",
"guard":{
"exp":{
"op":"=",
"left":"q10",
"right":1
}
},
"destinations":[
{
"probability":{
"exp":0.5000000
},
"location":"location",
"assignments":[
{
"ref":"q10",
"value":0
},
{
"ref":"q9",
"value":1
}
],
"observables":[
]
},
{
"probability":{
"exp":0.5000000
},
"location":"location",
"assignments":[
{
"ref":"q10",
"value":0
},
{
"ref":"q1",
"value":1
}
],
"observables":[
]
}
]
}
]
}
],
"system":{
"elements":[
{
"automaton":"process1"
},
{
"automaton":"process2"
},
{
"automaton":"process3"
},
{
"automaton":"process4"
},
{
"automaton":"process5"
},
{
"automaton":"process6"
},
{
"automaton":"process7"
},
{
"automaton":"process8"
},
{
"automaton":"process9"
},
{
"automaton":"process10"
}
],
"syncs":[
{
"synchronise":[
"tau__",
null,
null,
null,
null,
null,
null,
null,
null,
null
],
"result":"tau__"
},
{
"synchronise":[
null,
"tau__",
null,
null,
null,
null,
null,
null,
null,
null
],
"result":"tau__"
},
{
"synchronise":[
null,
null,
"tau__",
null,
null,
null,
null,
null,
null,
null
],
"result":"tau__"
},
{
"synchronise":[
null,
null,
null,
"tau__",
null,
null,
null,
null,
null,
null
],
"result":"tau__"
},
{
"synchronise":[
null,
null,
null,
null,
"tau__",
null,
null,
null,
null,
null
],
"result":"tau__"
},
{
"synchronise":[
null,
null,
null,
null,
null,
"tau__",
null,
null,
null,
null
],
"result":"tau__"
},
{
"synchronise":[
null,
null,
null,
null,
null,
null,
"tau__",
null,
null,
null
],
"result":"tau__"
},
{
"synchronise":[
null,
null,
null,
null,
null,
null,
null,
"tau__",
null,
null
],
"result":"tau__"
},
{
"synchronise":[
null,
null,
null,
null,
null,
null,
null,
null,
"tau__",
null
],
"result":"tau__"
},
{
"synchronise":[
null,
null,
null,
null,
null,
null,
null,
null,
null,
"tau__"
],
"result":"tau__"
}
]
}
}

1072
examples/exported-jani-models/ij11.jani
File diff suppressed because it is too large
View File

1178
examples/exported-jani-models/ij12.jani
File diff suppressed because it is too large
View File

1286
examples/exported-jani-models/ij13.jani
File diff suppressed because it is too large
View File

1396
examples/exported-jani-models/ij14.jani
File diff suppressed because it is too large
View File

1508
examples/exported-jani-models/ij15.jani
File diff suppressed because it is too large
View File

1622
examples/exported-jani-models/ij16.jani
File diff suppressed because it is too large
View File

1738
examples/exported-jani-models/ij17.jani
File diff suppressed because it is too large
View File

1856
examples/exported-jani-models/ij18.jani
File diff suppressed because it is too large
View File

1976
examples/exported-jani-models/ij19.jani
File diff suppressed because it is too large
View File

2098
examples/exported-jani-models/ij20.jani
File diff suppressed because it is too large
View File

2222
examples/exported-jani-models/ij21.jani
File diff suppressed because it is too large
View File

296
examples/exported-jani-models/ij3.jani
View File

@ -1,296 +0,0 @@
{
"jani-version":1,
"features":[
"derived-operators"
],
"name":"Converted from PRISM by IscasMC",
"type":"mdp",
"actions":[
{
"name":"tau__"
}
],
"variables":[
{
"name":"q1",
"type":{
"kind":"bounded",
"base":"int",
"lower-bound":0,
"upper-bound":1
}
},
{
"name":"q2",
"type":{
"kind":"bounded",
"base":"int",
"lower-bound":0,
"upper-bound":1
}
},
{
"name":"q3",
"type":{
"kind":"bounded",
"base":"int",
"lower-bound":0,
"upper-bound":1
}
}
],
"observables":[
{
"name":"\"steps\""
}
],
"initial-states":{
"exp":{
"op":"≥",
"left":{
"op":"+",
"left":{
"op":"+",
"left":"q1",
"right":"q2"
},
"right":"q3"
},
"right":1
}
},
"automata":[
{
"name":"process1",
"locations":[
{
"name":"location",
"observables":[
{
"ref":"\"steps\"",
"value":1
}
]
}
],
"initial-locations":[
"location"
],
"edges":[
{
"location":"location",
"action":"tau__",
"guard":{
"exp":{
"op":"=",
"left":"q1",
"right":1
}
},
"destinations":[
{
"probability":{
"exp":0.5000000
},
"location":"location",
"assignments":[
{
"ref":"q1",
"value":0
},
{
"ref":"q3",
"value":1
}
],
"observables":[
]
},
{
"probability":{
"exp":0.5000000
},
"location":"location",
"assignments":[
{
"ref":"q1",
"value":0
},
{
"ref":"q2",
"value":1
}
],
"observables":[
]
}
]
}
]
},
{
"name":"process2",
"locations":[
{
"name":"location"
}
],
"initial-locations":[
"location"
],
"edges":[
{
"location":"location",
"action":"tau__",
"guard":{
"exp":{
"op":"=",
"left":"q2",
"right":1
}
},
"destinations":[
{
"probability":{
"exp":0.5000000
},
"location":"location",
"assignments":[
{
"ref":"q2",
"value":0
},
{
"ref":"q1",
"value":1
}
],
"observables":[
]
},
{
"probability":{
"exp":0.5000000
},
"location":"location",
"assignments":[
{
"ref":"q2",
"value":0
},
{
"ref":"q3",
"value":1
}
],
"observables":[
]
}
]
}
]
},
{
"name":"process3",
"locations":[
{
"name":"location"
}
],
"initial-locations":[
"location"
],
"edges":[
{
"location":"location",
"action":"tau__",
"guard":{
"exp":{
"op":"=",
"left":"q3",
"right":1
}
},
"destinations":[
{
"probability":{
"exp":0.5000000
},
"location":"location",
"assignments":[
{
"ref":"q3",
"value":0
},
{
"ref":"q2",
"value":1
}
],
"observables":[
]
},
{
"probability":{
"exp":0.5000000
},
"location":"location",
"assignments":[
{
"ref":"q3",
"value":0
},
{
"ref":"q1",
"value":1
}
],
"observables":[
]
}
]
}
]
}
],
"system":{
"elements":[
{
"automaton":"process1"
},
{
"automaton":"process2"
},
{
"automaton":"process3"
}
],
"syncs":[
{
"synchronise":[
"tau__",
null,
null
],
"result":"tau__"
},
{
"synchronise":[
null,
"tau__",
null
],
"result":"tau__"
},
{
"synchronise":[
null,
null,
"tau__"
],
"result":"tau__"
}
]
}
}

386
examples/exported-jani-models/ij4.jani
View File

@ -1,386 +0,0 @@
{
"jani-version":1,
"features":[
"derived-operators"
],
"name":"Converted from PRISM by IscasMC",
"type":"mdp",
"actions":[
{
"name":"tau__"
}
],
"variables":[
{
"name":"q1",
"type":{
"kind":"bounded",
"base":"int",
"lower-bound":0,
"upper-bound":1
}
},
{
"name":"q2",
"type":{
"kind":"bounded",
"base":"int",
"lower-bound":0,
"upper-bound":1
}
},
{
"name":"q3",
"type":{
"kind":"bounded",
"base":"int",
"lower-bound":0,
"upper-bound":1
}
},
{
"name":"q4",
"type":{
"kind":"bounded",
"base":"int",
"lower-bound":0,
"upper-bound":1
}
}
],
"observables":[
{
"name":"\"steps\""
}
],
"initial-states":{
"exp":{
"op":"≥",
"left":{
"op":"+",
"left":{
"op":"+",
"left":{
"op":"+",
"left":"q1",
"right":"q2"
},
"right":"q3"
},
"right":"q4"
},
"right":1
}
},
"automata":[
{
"name":"process1",
"locations":[
{
"name":"location",
"observables":[
{
"ref":"\"steps\"",
"value":1
}
]
}
],
"initial-locations":[
"location"
],
"edges":[
{
"location":"location",
"action":"tau__",
"guard":{
"exp":{
"op":"=",
"left":"q1",
"right":1
}
},
"destinations":[
{
"probability":{
"exp":0.5000000
},
"location":"location",
"assignments":[
{
"ref":"q1",
"value":0
},
{
"ref":"q4",
"value":1
}
],
"observables":[
]
},
{
"probability":{
"exp":0.5000000
},
"location":"location",
"assignments":[
{
"ref":"q1",
"value":0
},
{
"ref":"q2",
"value":1
}
],
"observables":[
]
}
]
}
]
},
{
"name":"process2",
"locations":[
{
"name":"location"
}
],
"initial-locations":[
"location"
],
"edges":[
{
"location":"location",
"action":"tau__",
"guard":{
"exp":{
"op":"=",
"left":"q2",
"right":1
}
},
"destinations":[
{
"probability":{
"exp":0.5000000
},
"location":"location",
"assignments":[
{
"ref":"q2",
"value":0
},
{
"ref":"q1",
"value":1
}
],
"observables":[
]
},
{
"probability":{
"exp":0.5000000
},
"location":"location",
"assignments":[
{
"ref":"q2",
"value":0
},
{
"ref":"q3",
"value":1
}
],
"observables":[
]
}
]
}
]
},
{
"name":"process3",
"locations":[
{
"name":"location"
}
],
"initial-locations":[
"location"
],
"edges":[
{
"location":"location",
"action":"tau__",
"guard":{
"exp":{
"op":"=",
"left":"q3",
"right":1
}
},
"destinations":[
{
"probability":{
"exp":0.5000000
},
"location":"location",
"assignments":[
{
"ref":"q3",
"value":0
},
{
"ref":"q2",
"value":1
}
],
"observables":[
]
},
{
"probability":{
"exp":0.5000000
},
"location":"location",
"assignments":[
{
"ref":"q3",
"value":0
},
{
"ref":"q4",
"value":1
}
],
"observables":[
]
}
]
}
]
},
{
"name":"process4",
"locations":[
{
"name":"location"
}
],
"initial-locations":[
"location"
],
"edges":[
{
"location":"location",
"action":"tau__",
"guard":{
"exp":{
"op":"=",
"left":"q4",
"right":1
}
},
"destinations":[
{
"probability":{
"exp":0.5000000
},
"location":"location",
"assignments":[
{
"ref":"q4",
"value":0
},
{
"ref":"q3",
"value":1
}
],
"observables":[
]
},
{
"probability":{
"exp":0.5000000
},
"location":"location",
"assignments":[
{
"ref":"q4",
"value":0
},
{
"ref":"q1",
"value":1
}
],
"observables":[
]
}
]
}
]
}
],
"system":{
"elements":[
{
"automaton":"process1"
},
{
"automaton":"process2"
},
{
"automaton":"process3"
},
{
"automaton":"process4"
}
],
"syncs":[
{
"synchronise":[
"tau__",
null,
null,
null
],
"result":"tau__"
},
{
"synchronise":[
null,
"tau__",
null,
null
],
"result":"tau__"
},
{
"synchronise":[
null,
null,
"tau__",
null
],
"result":"tau__"
},
{
"synchronise":[
null,
null,
null,
"tau__"
],
"result":"tau__"
}
]
}
}

478
examples/exported-jani-models/ij5.jani
View File

@ -1,478 +0,0 @@
{
"jani-version":1,
"features":[
"derived-operators"
],
"name":"Converted from PRISM by IscasMC",
"type":"mdp",
"actions":[
{
"name":"tau__"
}
],
"variables":[
{
"name":"q1",
"type":{
"kind":"bounded",
"base":"int",
"lower-bound":0,
"upper-bound":1
}
},
{
"name":"q2",
"type":{
"kind":"bounded",
"base":"int",
"lower-bound":0,
"upper-bound":1
}
},
{
"name":"q3",
"type":{
"kind":"bounded",
"base":"int",
"lower-bound":0,
"upper-bound":1
}
},
{
"name":"q4",
"type":{
"kind":"bounded",
"base":"int",
"lower-bound":0,
"upper-bound":1
}
},
{
"name":"q5",
"type":{
"kind":"bounded",
"base":"int",
"lower-bound":0,
"upper-bound":1
}
}
],
"observables":[
{
"name":"\"steps\""
}
],
"initial-states":{
"exp":{
"op":"≥",
"left":{
"op":"+",
"left":{
"op":"+",
"left":{
"op":"+",
"left":{
"op":"+",
"left":"q1",
"right":"q2"
},
"right":"q3"
},
"right":"q4"
},
"right":"q5"
},
"right":1
}
},
"automata":[
{
"name":"process1",
"locations":[
{
"name":"location",
"observables":[
{
"ref":"\"steps\"",
"value":1
}
]
}
],
"initial-locations":[
"location"
],
"edges":[
{
"location":"location",
"action":"tau__",
"guard":{
"exp":{
"op":"=",
"left":"q1",
"right":1
}
},
"destinations":[
{
"probability":{
"exp":0.5000000
},
"location":"location",
"assignments":[
{
"ref":"q1",
"value":0
},
{
"ref":"q5",
"value":1
}
],
"observables":[
]
},
{
"probability":{
"exp":0.5000000
},
"location":"location",
"assignments":[
{
"ref":"q1",
"value":0
},
{
"ref":"q2",
"value":1
}
],
"observables":[
]
}
]
}
]
},
{
"name":"process2",
"locations":[
{
"name":"location"
}
],
"initial-locations":[
"location"
],
"edges":[
{
"location":"location",
"action":"tau__",
"guard":{
"exp":{
"op":"=",
"left":"q2",
"right":1
}
},
"destinations":[
{
"probability":{
"exp":0.5000000
},
"location":"location",
"assignments":[
{
"ref":"q2",
"value":0
},
{
"ref":"q1",
"value":1
}
],
"observables":[
]
},
{
"probability":{
"exp":0.5000000
},
"location":"location",
"assignments":[
{
"ref":"q2",
"value":0
},
{
"ref":"q3",
"value":1
}
],
"observables":[
]
}
]
}
]
},
{
"name":"process3",
"locations":[
{
"name":"location"
}
],
"initial-locations":[
"location"
],
"edges":[
{
"location":"location",
"action":"tau__",
"guard":{
"exp":{
"op":"=",
"left":"q3",
"right":1
}
},
"destinations":[
{
"probability":{
"exp":0.5000000
},
"location":"location",
"assignments":[
{
"ref":"q3",
"value":0
},
{
"ref":"q2",
"value":1
}
],
"observables":[
]
},
{
"probability":{
"exp":0.5000000
},
"location":"location",
"assignments":[
{
"ref":"q3",
"value":0
},
{
"ref":"q4",
"value":1
}
],
"observables":[
]
}
]
}
]
},
{
"name":"process4",
"locations":[
{
"name":"location"
}
],
"initial-locations":[
"location"
],
"edges":[
{
"location":"location",
"action":"tau__",
"guard":{
"exp":{
"op":"=",
"left":"q4",
"right":1
}
},
"destinations":[
{
"probability":{
"exp":0.5000000
},
"location":"location",
"assignments":[
{
"ref":"q4",
"value":0
},
{
"ref":"q3",
"value":1
}
],
"observables":[
]
},
{
"probability":{
"exp":0.5000000
},
"location":"location",
"assignments":[
{
"ref":"q4",
"value":0
},
{
"ref":"q5",
"value":1
}
],
"observables":[
]
}
]
}
]
},
{
"name":"process5",
"locations":[
{
"name":"location"
}
],
"initial-locations":[
"location"
],
"edges":[
{
"location":"location",
"action":"tau__",
"guard":{
"exp":{
"op":"=",
"left":"q5",
"right":1
}
},
"destinations":[
{
"probability":{
"exp":0.5000000
},
"location":"location",
"assignments":[
{
"ref":"q5",
"value":0
},
{
"ref":"q4",
"value":1
}
],
"observables":[
]
},
{
"probability":{
"exp":0.5000000
},
"location":"location",
"assignments":[
{
"ref":"q5",
"value":0
},
{
"ref":"q1",
"value":1
}
],
"observables":[
]
}
]
}
]
}
],
"system":{
"elements":[
{
"automaton":"process1"
},
{
"automaton":"process2"
},
{
"automaton":"process3"
},
{
"automaton":"process4"
},
{
"automaton":"process5"
}
],
"syncs":[
{
"synchronise":[
"tau__",
null,
null,
null,
null
],
"result":"tau__"
},
{
"synchronise":[
null,
"tau__",
null,
null,
null
],
"result":"tau__"
},
{
"synchronise":[
null,
null,
"tau__",
null,
null
],
"result":"tau__"
},
{
"synchronise":[
null,
null,
null,
"tau__",
null
],
"result":"tau__"
},
{
"synchronise":[
null,
null,
null,
null,
"tau__"
],
"result":"tau__"
}
]
}
}

572
examples/exported-jani-models/ij6.jani
View File

@ -1,572 +0,0 @@
{
"jani-version":1,
"features":[
"derived-operators"
],
"name":"Converted from PRISM by IscasMC",
"type":"mdp",
"actions":[
{
"name":"tau__"
}
],
"variables":[
{
"name":"q1",
"type":{
"kind":"bounded",
"base":"int",
"lower-bound":0,
"upper-bound":1
}
},
{
"name":"q2",
"type":{
"kind":"bounded",
"base":"int",
"lower-bound":0,
"upper-bound":1
}
},
{
"name":"q3",
"type":{
"kind":"bounded",
"base":"int",
"lower-bound":0,
"upper-bound":1
}
},
{
"name":"q4",
"type":{
"kind":"bounded",
"base":"int",
"lower-bound":0,
"upper-bound":1
}
},
{
"name":"q5",
"type":{
"kind":"bounded",
"base":"int",
"lower-bound":0,
"upper-bound":1
}
},
{
"name":"q6",
"type":{
"kind":"bounded",
"base":"int",
"lower-bound":0,
"upper-bound":1
}
}
],
"observables":[
{
"name":"\"steps\""
}
],
"initial-states":{
"exp":{
"op":"≥",
"left":{
"op":"+",
"left":{
"op":"+",
"left":{
"op":"+",
"left":{
"op":"+",
"left":{
"op":"+",
"left":"q1",
"right":"q2"
},
"right":"q3"
},
"right":"q4"
},
"right":"q5"
},
"right":"q6"
},
"right":1
}
},
"automata":[
{
"name":"process1",
"locations":[
{
"name":"location",
"observables":[
{
"ref":"\"steps\"",
"value":1
}
]
}
],
"initial-locations":[
"location"
],
"edges":[
{
"location":"location",
"action":"tau__",
"guard":{
"exp":{
"op":"=",
"left":"q1",
"right":1
}
},
"destinations":[
{
"probability":{
"exp":0.5000000
},
"location":"location",
"assignments":[
{
"ref":"q1",
"value":0
},
{
"ref":"q6",
"value":1
}
],
"observables":[
]
},
{
"probability":{
"exp":0.5000000
},
"location":"location",
"assignments":[
{
"ref":"q1",
"value":0
},
{
"ref":"q2",
"value":1
}
],
"observables":[
]
}
]
}
]
},
{
"name":"process2",
"locations":[
{
"name":"location"
}
],
"initial-locations":[
"location"
],
"edges":[
{
"location":"location",
"action":"tau__",
"guard":{
"exp":{
"op":"=",
"left":"q2",
"right":1
}
},
"destinations":[
{
"probability":{
"exp":0.5000000
},
"location":"location",
"assignments":[
{
"ref":"q2",
"value":0
},
{
"ref":"q1",
"value":1
}
],
"observables":[
]
},
{
"probability":{
"exp":0.5000000
},
"location":"location",
"assignments":[
{
"ref":"q2",
"value":0
},
{
"ref":"q3",
"value":1
}
],
"observables":[
]
}
]
}
]
},
{
"name":"process3",
"locations":[
{
"name":"location"
}
],
"initial-locations":[
"location"
],
"edges":[
{
"location":"location",
"action":"tau__",
"guard":{
"exp":{
"op":"=",
"left":"q3",
"right":1
}
},
"destinations":[
{
"probability":{
"exp":0.5000000
},
"location":"location",
"assignments":[
{
"ref":"q3",
"value":0
},
{
"ref":"q2",
"value":1
}
],
"observables":[
]
},
{
"probability":{
"exp":0.5000000
},
"location":"location",
"assignments":[
{
"ref":"q3",
"value":0
},
{
"ref":"q4",
"value":1
}
],
"observables":[
]
}
]
}
]
},
{
"name":"process4",
"locations":[
{
"name":"location"
}
],
"initial-locations":[
"location"
],
"edges":[
{
"location":"location",
"action":"tau__",
"guard":{
"exp":{
"op":"=",
"left":"q4",
"right":1
}
},
"destinations":[
{
"probability":{
"exp":0.5000000
},
"location":"location",
"assignments":[
{
"ref":"q4",
"value":0
},
{
"ref":"q3",
"value":1
}
],
"observables":[
]
},
{
"probability":{
"exp":0.5000000
},
"location":"location",
"assignments":[
{
"ref":"q4",
"value":0
},
{
"ref":"q5",
"value":1
}
],
"observables":[
]
}
]
}
]
},
{
"name":"process5",
"locations":[
{
"name":"location"
}
],
"initial-locations":[
"location"
],
"edges":[
{
"location":"location",
"action":"tau__",
"guard":{
"exp":{
"op":"=",
"left":"q5",
"right":1
}
},
"destinations":[
{
"probability":{
"exp":0.5000000
},
"location":"location",
"assignments":[
{
"ref":"q5",
"value":0
},
{
"ref":"q4",
"value":1
}
],
"observables":[
]
},
{
"probability":{
"exp":0.5000000
},
"location":"location",
"assignments":[
{
"ref":"q5",
"value":0
},
{
"ref":"q6",
"value":1
}
],
"observables":[
]
}
]
}
]
},
{
"name":"process6",
"locations":[
{
"name":"location"
}
],
"initial-locations":[
"location"
],
"edges":[
{
"location":"location",
"action":"tau__",
"guard":{
"exp":{
"op":"=",
"left":"q6",
"right":1
}
},
"destinations":[
{
"probability":{
"exp":0.5000000
},
"location":"location",
"assignments":[
{
"ref":"q6",
"value":0
},
{
"ref":"q5",
"value":1
}
],
"observables":[
]
},
{
"probability":{
"exp":0.5000000
},
"location":"location",
"assignments":[
{
"ref":"q6",
"value":0
},
{
"ref":"q1",
"value":1
}
],
"observables":[
]
}
]
}
]
}
],
"system":{
"elements":[
{
"automaton":"process1"
},
{
"automaton":"process2"
},
{
"automaton":"process3"
},
{
"automaton":"process4"
},
{
"automaton":"process5"
},
{
"automaton":"process6"
}
],
"syncs":[
{
"synchronise":[
"tau__",
null,
null,
null,
null,
null
],
"result":"tau__"
},
{
"synchronise":[
null,
"tau__",
null,
null,
null,
null
],
"result":"tau__"
},
{
"synchronise":[
null,
null,
"tau__",
null,
null,
null
],
"result":"tau__"
},
{
"synchronise":[
null,
null,
null,
"tau__",
null,
null
],
"result":"tau__"
},
{
"synchronise":[
null,
null,
null,
null,
"tau__",
null
],
"result":"tau__"
},
{
"synchronise":[
null,
null,
null,
null,
null,
"tau__"
],
"result":"tau__"
}
]
}
}

668
examples/exported-jani-models/ij7.jani
View File

@ -1,668 +0,0 @@
{
"jani-version":1,
"features":[
"derived-operators"
],
"name":"Converted from PRISM by IscasMC",
"type":"mdp",
"actions":[
{
"name":"tau__"
}
],
"variables":[
{
"name":"q1",
"type":{
"kind":"bounded",
"base":"int",
"lower-bound":0,
"upper-bound":1
}
},
{
"name":"q2",
"type":{
"kind":"bounded",
"base":"int",
"lower-bound":0,
"upper-bound":1
}
},
{
"name":"q3",
"type":{
"kind":"bounded",
"base":"int",
"lower-bound":0,
"upper-bound":1
}
},
{
"name":"q4",
"type":{
"kind":"bounded",
"base":"int",
"lower-bound":0,
"upper-bound":1
}
},
{
"name":"q5",
"type":{
"kind":"bounded",
"base":"int",
"lower-bound":0,
"upper-bound":1
}
},
{
"name":"q6",
"type":{
"kind":"bounded",
"base":"int",
"lower-bound":0,
"upper-bound":1
}
},
{
"name":"q7",
"type":{
"kind":"bounded",
"base":"int",
"lower-bound":0,
"upper-bound":1
}
}
],
"observables":[
{
"name":"\"steps\""
}
],
"initial-states":{
"exp":{
"op":"≥",
"left":{
"op":"+",
"left":{
"op":"+",
"left":{
"op":"+",
"left":{
"op":"+",
"left":{
"op":"+",
"left":{
"op":"+",
"left":"q1",
"right":"q2"
},
"right":"q3"
},
"right":"q4"
},
"right":"q5"
},
"right":"q6"
},
"right":"q7"
},
"right":1
}
},
"automata":[
{
"name":"process1",
"locations":[
{
"name":"location",
"observables":[
{
"ref":"\"steps\"",
"value":1
}
]
}
],
"initial-locations":[
"location"
],
"edges":[
{
"location":"location",
"action":"tau__",
"guard":{
"exp":{
"op":"=",
"left":"q1",
"right":1
}
},
"destinations":[
{
"probability":{
"exp":0.5000000
},
"location":"location",
"assignments":[
{
"ref":"q1",
"value":0
},
{
"ref":"q7",
"value":1
}
],
"observables":[
]
},
{
"probability":{
"exp":0.5000000
},
"location":"location",
"assignments":[
{
"ref":"q1",
"value":0
},
{
"ref":"q2",
"value":1
}
],
"observables":[
]
}
]
}
]
},
{
"name":"process2",
"locations":[
{
"name":"location"
}
],
"initial-locations":[
"location"
],
"edges":[
{
"location":"location",
"action":"tau__",
"guard":{
"exp":{
"op":"=",
"left":"q2",
"right":1
}
},
"destinations":[
{
"probability":{
"exp":0.5000000
},
"location":"location",
"assignments":[
{
"ref":"q2",
"value":0
},
{
"ref":"q1",
"value":1
}
],
"observables":[
]
},
{
"probability":{
"exp":0.5000000
},
"location":"location",
"assignments":[
{
"ref":"q2",
"value":0
},
{
"ref":"q3",
"value":1
}
],
"observables":[
]
}
]
}
]
},
{
"name":"process3",
"locations":[
{
"name":"location"
}
],
"initial-locations":[
"location"
],
"edges":[
{
"location":"location",
"action":"tau__",
"guard":{
"exp":{
"op":"=",
"left":"q3",
"right":1
}
},
"destinations":[
{
"probability":{
"exp":0.5000000
},
"location":"location",
"assignments":[
{
"ref":"q3",
"value":0
},
{
"ref":"q2",
"value":1
}
],
"observables":[
]
},
{
"probability":{
"exp":0.5000000
},
"location":"location",
"assignments":[
{
"ref":"q3",
"value":0
},
{
"ref":"q4",
"value":1
}
],
"observables":[
]
}
]
}
]
},
{
"name":"process4",
"locations":[
{
"name":"location"
}
],
"initial-locations":[
"location"
],
"edges":[
{
"location":"location",
"action":"tau__",
"guard":{
"exp":{
"op":"=",
"left":"q4",
"right":1
}
},
"destinations":[
{
"probability":{
"exp":0.5000000
},
"location":"location",
"assignments":[
{
"ref":"q4",
"value":0
},
{
"ref":"q3",
"value":1
}
],
"observables":[
]
},
{
"probability":{
"exp":0.5000000
},
"location":"location",
"assignments":[
{
"ref":"q4",
"value":0
},
{
"ref":"q5",
"value":1
}
],
"observables":[
]
}
]
}
]
},
{
"name":"process5",
"locations":[
{
"name":"location"
}
],
"initial-locations":[
"location"
],
"edges":[
{
"location":"location",
"action":"tau__",
"guard":{
"exp":{
"op":"=",
"left":"q5",
"right":1
}
},
"destinations":[
{
"probability":{
"exp":0.5000000
},
"location":"location",
"assignments":[
{
"ref":"q5",
"value":0
},
{
"ref":"q4",
"value":1
}
],
"observables":[
]
},
{
"probability":{
"exp":0.5000000
},
"location":"location",
"assignments":[
{
"ref":"q5",
"value":0
},
{
"ref":"q6",
"value":1
}
],
"observables":[
]
}
]
}
]
},
{
"name":"process6",
"locations":[
{
"name":"location"
}
],
"initial-locations":[
"location"
],
"edges":[
{
"location":"location",
"action":"tau__",
"guard":{
"exp":{
"op":"=",
"left":"q6",
"right":1
}
},
"destinations":[
{
"probability":{
"exp":0.5000000
},
"location":"location",
"assignments":[
{
"ref":"q6",
"value":0
},
{
"ref":"q5",
"value":1
}
],
"observables":[
]
},
{
"probability":{
"exp":0.5000000
},
"location":"location",
"assignments":[
{
"ref":"q6",
"value":0
},
{
"ref":"q7",
"value":1
}
],
"observables":[
]
}
]
}
]
},
{
"name":"process7",
"locations":[
{
"name":"location"
}
],
"initial-locations":[
"location"
],
"edges":[
{
"location":"location",
"action":"tau__",
"guard":{
"exp":{
"op":"=",
"left":"q7",
"right":1
}
},
"destinations":[
{
"probability":{
"exp":0.5000000
},
"location":"location",
"assignments":[
{
"ref":"q7",
"value":0
},
{
"ref":"q6",
"value":1
}
],
"observables":[
]
},
{
"probability":{
"exp":0.5000000
},
"location":"location",
"assignments":[
{
"ref":"q7",
"value":0
},
{
"ref":"q1",
"value":1
}
],
"observables":[
]
}
]
}
]
}
],
"system":{
"elements":[
{
"automaton":"process1"
},
{
"automaton":"process2"
},
{
"automaton":"process3"
},
{
"automaton":"process4"
},
{
"automaton":"process5"
},
{
"automaton":"process6"
},
{
"automaton":"process7"
}
],
"syncs":[
{
"synchronise":[
"tau__",
null,
null,
null,
null,
null,
null
],
"result":"tau__"
},
{
"synchronise":[
null,
"tau__",
null,
null,
null,
null,
null
],
"result":"tau__"
},
{
"synchronise":[
null,
null,
"tau__",
null,
null,
null,
null
],
"result":"tau__"
},
{
"synchronise":[
null,
null,
null,
"tau__",
null,
null,
null
],
"result":"tau__"
},
{
"synchronise":[
null,
null,
null,
null,
"tau__",
null,
null
],
"result":"tau__"
},
{
"synchronise":[
null,
null,
null,
null,
null,
"tau__",
null
],
"result":"tau__"
},
{
"synchronise":[
null,
null,
null,
null,
null,
null,
"tau__"
],
"result":"tau__"
}
]
}
}

766
examples/exported-jani-models/ij8.jani
View File

@ -1,766 +0,0 @@
{
"jani-version":1,
"features":[
"derived-operators"
],
"name":"Converted from PRISM by IscasMC",
"type":"mdp",
"actions":[
{
"name":"tau__"
}
],
"variables":[
{
"name":"q1",
"type":{
"kind":"bounded",
"base":"int",
"lower-bound":0,
"upper-bound":1
}
},
{
"name":"q2",
"type":{
"kind":"bounded",
"base":"int",
"lower-bound":0,
"upper-bound":1
}
},
{
"name":"q3",
"type":{
"kind":"bounded",
"base":"int",
"lower-bound":0,
"upper-bound":1
}
},
{
"name":"q4",
"type":{
"kind":"bounded",
"base":"int",
"lower-bound":0,
"upper-bound":1
}
},
{
"name":"q5",
"type":{
"kind":"bounded",
"base":"int",
"lower-bound":0,
"upper-bound":1
}
},
{
"name":"q6",
"type":{
"kind":"bounded",
"base":"int",
"lower-bound":0,
"upper-bound":1
}
},
{
"name":"q7",
"type":{
"kind":"bounded",
"base":"int",
"lower-bound":0,
"upper-bound":1
}
},
{
"name":"q8",
"type":{
"kind":"bounded",
"base":"int",
"lower-bound":0,
"upper-bound":1
}
}
],
"observables":[
{
"name":"\"steps\""
}
],
"initial-states":{
"exp":{
"op":"≥",
"left":{
"op":"+",
"left":{
"op":"+",
"left":{
"op":"+",
"left":{
"op":"+",
"left":{
"op":"+",
"left":{
"op":"+",
"left":{
"op":"+",
"left":"q1",
"right":"q2"
},
"right":"q3"
},
"right":"q4"
},
"right":"q5"
},
"right":"q6"
},
"right":"q7"
},
"right":"q8"
},
"right":1
}
},
"automata":[
{
"name":"process1",
"locations":[
{
"name":"location",
"observables":[
{
"ref":"\"steps\"",
"value":1
}
]
}
],
"initial-locations":[
"location"
],
"edges":[
{
"location":"location",
"action":"tau__",
"guard":{
"exp":{
"op":"=",
"left":"q1",
"right":1
}
},
"destinations":[
{
"probability":{
"exp":0.5000000
},
"location":"location",
"assignments":[
{
"ref":"q1",
"value":0
},
{
"ref":"q8",
"value":1
}
],
"observables":[
]
},
{
"probability":{
"exp":0.5000000
},
"location":"location",
"assignments":[
{
"ref":"q1",
"value":0
},
{
"ref":"q2",
"value":1
}
],
"observables":[
]
}
]
}
]
},
{
"name":"process2",
"locations":[
{
"name":"location"
}
],
"initial-locations":[
"location"
],
"edges":[
{
"location":"location",
"action":"tau__",
"guard":{
"exp":{
"op":"=",
"left":"q2",
"right":1
}
},
"destinations":[
{
"probability":{
"exp":0.5000000
},
"location":"location",
"assignments":[
{
"ref":"q2",
"value":0
},
{
"ref":"q1",
"value":1
}
],
"observables":[
]
},
{
"probability":{
"exp":0.5000000
},
"location":"location",
"assignments":[
{
"ref":"q2",
"value":0
},
{
"ref":"q3",
"value":1
}
],
"observables":[
]
}
]
}
]
},
{
"name":"process3",
"locations":[
{
"name":"location"
}
],
"initial-locations":[
"location"
],
"edges":[
{
"location":"location",
"action":"tau__",
"guard":{
"exp":{
"op":"=",
"left":"q3",
"right":1
}
},
"destinations":[
{
"probability":{
"exp":0.5000000
},
"location":"location",
"assignments":[
{
"ref":"q3",
"value":0
},
{
"ref":"q2",
"value":1
}
],
"observables":[
]
},
{
"probability":{
"exp":0.5000000
},
"location":"location",
"assignments":[
{
"ref":"q3",
"value":0
},
{
"ref":"q4",
"value":1
}
],
"observables":[
]
}
]
}
]
},
{
"name":"process4",
"locations":[
{
"name":"location"
}
],
"initial-locations":[
"location"
],
"edges":[
{
"location":"location",
"action":"tau__",
"guard":{
"exp":{
"op":"=",
"left":"q4",
"right":1
}
},
"destinations":[
{
"probability":{
"exp":0.5000000
},
"location":"location",
"assignments":[
{
"ref":"q4",
"value":0
},
{
"ref":"q3",
"value":1
}
],
"observables":[
]
},
{
"probability":{
"exp":0.5000000
},
"location":"location",
"assignments":[
{
"ref":"q4",
"value":0
},
{
"ref":"q5",
"value":1
}
],
"observables":[
]
}
]
}
]
},
{
"name":"process5",
"locations":[
{
"name":"location"
}
],
"initial-locations":[
"location"
],
"edges":[
{
"location":"location",
"action":"tau__",
"guard":{
"exp":{
"op":"=",
"left":"q5",
"right":1
}
},
"destinations":[
{
"probability":{
"exp":0.5000000
},
"location":"location",
"assignments":[
{
"ref":"q5",
"value":0
},
{
"ref":"q4",
"value":1
}
],
"observables":[
]
},
{
"probability":{
"exp":0.5000000
},
"location":"location",
"assignments":[
{
"ref":"q5",
"value":0
},
{
"ref":"q6",
"value":1
}
],
"observables":[
]
}
]
}
]
},
{
"name":"process6",
"locations":[
{
"name":"location"
}
],
"initial-locations":[
"location"
],
"edges":[
{
"location":"location",
"action":"tau__",
"guard":{
"exp":{
"op":"=",
"left":"q6",
"right":1
}
},
"destinations":[
{
"probability":{
"exp":0.5000000
},
"location":"location",
"assignments":[
{
"ref":"q6",
"value":0
},
{
"ref":"q5",
"value":1
}
],
"observables":[
]
},
{
"probability":{
"exp":0.5000000
},
"location":"location",
"assignments":[
{
"ref":"q6",
"value":0
},
{
"ref":"q7",
"value":1
}
],
"observables":[
]
}
]
}
]
},
{
"name":"process7",
"locations":[
{
"name":"location"
}
],
"initial-locations":[
"location"
],
"edges":[
{
"location":"location",
"action":"tau__",
"guard":{
"exp":{
"op":"=",
"left":"q7",
"right":1
}
},
"destinations":[
{
"probability":{
"exp":0.5000000
},
"location":"location",
"assignments":[
{
"ref":"q7",
"value":0
},
{
"ref":"q6",
"value":1
}
],
"observables":[
]
},
{
"probability":{
"exp":0.5000000
},
"location":"location",
"assignments":[
{
"ref":"q7",
"value":0
},
{
"ref":"q8",
"value":1
}
],
"observables":[
]
}
]
}
]
},
{
"name":"process8",
"locations":[
{
"name":"location"
}
],
"initial-locations":[
"location"
],
"edges":[
{
"location":"location",
"action":"tau__",
"guard":{
"exp":{
"op":"=",
"left":"q8",
"right":1
}
},
"destinations":[
{
"probability":{
"exp":0.5000000
},
"location":"location",
"assignments":[
{
"ref":"q8",
"value":0
},
{
"ref":"q7",
"value":1
}
],
"observables":[
]
},
{
"probability":{
"exp":0.5000000
},
"location":"location",
"assignments":[
{
"ref":"q8",
"value":0
},
{
"ref":"q1",
"value":1
}
],
"observables":[
]
}
]
}
]
}
],
"system":{
"elements":[
{
"automaton":"process1"
},
{
"automaton":"process2"
},
{
"automaton":"process3"
},
{
"automaton":"process4"
},
{
"automaton":"process5"
},
{
"automaton":"process6"
},
{
"automaton":"process7"
},
{
"automaton":"process8"
}
],
"syncs":[
{
"synchronise":[
"tau__",
null,
null,
null,
null,
null,
null,
null
],
"result":"tau__"
},
{
"synchronise":[
null,
"tau__",
null,
null,
null,
null,
null,
null
],
"result":"tau__"
},
{
"synchronise":[
null,
null,
"tau__",
null,
null,
null,
null,
null
],
"result":"tau__"
},
{
"synchronise":[
null,
null,
null,
"tau__",
null,
null,
null,
null
],
"result":"tau__"
},
{
"synchronise":[
null,
null,
null,
null,
"tau__",
null,
null,
null
],
"result":"tau__"
},
{
"synchronise":[
null,
null,
null,
null,
null,
"tau__",
null,
null
],
"result":"tau__"
},
{
"synchronise":[
null,
null,
null,
null,
null,
null,
"tau__",
null
],
"result":"tau__"
},
{
"synchronise":[
null,
null,
null,
null,
null,
null,
null,
"tau__"
],
"result":"tau__"
}
]
}
}

866
examples/exported-jani-models/ij9.jani
View File

@ -1,866 +0,0 @@
{
"jani-version":1,
"features":[
"derived-operators"
],
"name":"Converted from PRISM by IscasMC",
"type":"mdp",
"actions":[
{
"name":"tau__"
}
],
"variables":[
{
"name":"q1",
"type":{
"kind":"bounded",
"base":"int",
"lower-bound":0,
"upper-bound":1
}
},
{
"name":"q2",
"type":{
"kind":"bounded",
"base":"int",
"lower-bound":0,
"upper-bound":1
}
},
{
"name":"q3",
"type":{
"kind":"bounded",
"base":"int",
"lower-bound":0,
"upper-bound":1
}
},
{
"name":"q4",
"type":{
"kind":"bounded",
"base":"int",
"lower-bound":0,
"upper-bound":1
}
},
{
"name":"q5",
"type":{
"kind":"bounded",
"base":"int",
"lower-bound":0,
"upper-bound":1
}
},
{
"name":"q6",
"type":{
"kind":"bounded",
"base":"int",
"lower-bound":0,
"upper-bound":1
}
},
{
"name":"q7",
"type":{
"kind":"bounded",
"base":"int",
"lower-bound":0,
"upper-bound":1
}
},
{
"name":"q8",
"type":{
"kind":"bounded",
"base":"int",
"lower-bound":0,
"upper-bound":1
}
},
{
"name":"q9",
"type":{
"kind":"bounded",
"base":"int",
"lower-bound":0,
"upper-bound":1
}
}
],
"observables":[
{
"name":"\"steps\""
}
],
"initial-states":{
"exp":{
"op":"≥",
"left":{
"op":"+",
"left":{
"op":"+",
"left":{
"op":"+",
"left":{
"op":"+",
"left":{
"op":"+",
"left":{
"op":"+",
"left":{
"op":"+",
"left":{
"op":"+",
"left":"q1",
"right":"q2"
},
"right":"q3"
},
"right":"q4"
},
"right":"q5"
},
"right":"q6"
},
"right":"q7"
},
"right":"q8"
},
"right":"q9"
},
"right":1
}
},
"automata":[
{
"name":"process1",
"locations":[
{
"name":"location",
"observables":[
{
"ref":"\"steps\"",
"value":1
}
]
}
],
"initial-locations":[
"location"
],
"edges":[
{
"location":"location",
"action":"tau__",
"guard":{
"exp":{
"op":"=",
"left":"q1",
"right":1
}
},
"destinations":[
{
"probability":{
"exp":0.5000000
},
"location":"location",
"assignments":[
{
"ref":"q1",
"value":0
},
{
"ref":"q9",
"value":1
}
],
"observables":[
]
},
{
"probability":{
"exp":0.5000000
},
"location":"location",
"assignments":[
{
"ref":"q1",
"value":0
},
{
"ref":"q2",
"value":1
}
],
"observables":[
]
}
]
}
]
},
{
"name":"process2",
"locations":[
{
"name":"location"
}
],
"initial-locations":[
"location"
],
"edges":[
{
"location":"location",
"action":"tau__",
"guard":{
"exp":{
"op":"=",
"left":"q2",
"right":1
}
},
"destinations":[
{
"probability":{
"exp":0.5000000
},
"location":"location",
"assignments":[
{
"ref":"q2",
"value":0
},
{
"ref":"q1",
"value":1
}
],
"observables":[
]
},
{
"probability":{
"exp":0.5000000
},
"location":"location",
"assignments":[
{
"ref":"q2",
"value":0
},
{
"ref":"q3",
"value":1
}
],
"observables":[
]
}
]
}
]
},
{
"name":"process3",
"locations":[
{
"name":"location"
}
],
"initial-locations":[
"location"
],
"edges":[
{
"location":"location",
"action":"tau__",
"guard":{
"exp":{
"op":"=",
"left":"q3",
"right":1
}
},
"destinations":[
{
"probability":{
"exp":0.5000000
},
"location":"location",
"assignments":[
{
"ref":"q3",
"value":0
},
{
"ref":"q2",
"value":1
}
],
"observables":[
]
},
{
"probability":{
"exp":0.5000000
},
"location":"location",
"assignments":[
{
"ref":"q3",
"value":0
},
{
"ref":"q4",
"value":1
}
],
"observables":[
]
}
]
}
]
},
{
"name":"process4",
"locations":[
{
"name":"location"
}
],
"initial-locations":[
"location"
],
"edges":[
{
"location":"location",
"action":"tau__",
"guard":{
"exp":{
"op":"=",
"left":"q4",
"right":1
}
},
"destinations":[
{
"probability":{
"exp":0.5000000
},
"location":"location",
"assignments":[
{
"ref":"q4",
"value":0
},
{
"ref":"q3",
"value":1
}
],
"observables":[
]
},
{
"probability":{
"exp":0.5000000
},
"location":"location",
"assignments":[
{
"ref":"q4",
"value":0
},
{
"ref":"q5",
"value":1
}
],
"observables":[
]
}
]
}
]
},
{
"name":"process5",
"locations":[
{
"name":"location"
}
],
"initial-locations":[
"location"
],
"edges":[
{
"location":"location",
"action":"tau__",
"guard":{
"exp":{
"op":"=",
"left":"q5",
"right":1
}
},
"destinations":[
{
"probability":{
"exp":0.5000000
},
"location":"location",
"assignments":[
{
"ref":"q5",
"value":0
},
{
"ref":"q4",
"value":1
}
],
"observables":[
]
},
{
"probability":{
"exp":0.5000000
},
"location":"location",
"assignments":[
{
"ref":"q5",
"value":0
},
{
"ref":"q6",
"value":1
}
],
"observables":[
]
}
]
}
]
},
{
"name":"process6",
"locations":[
{
"name":"location"
}
],
"initial-locations":[
"location"
],
"edges":[
{
"location":"location",
"action":"tau__",
"guard":{
"exp":{
"op":"=",
"left":"q6",
"right":1
}
},
"destinations":[
{
"probability":{
"exp":0.5000000
},
"location":"location",
"assignments":[
{
"ref":"q6",
"value":0
},
{
"ref":"q5",
"value":1
}
],
"observables":[
]
},
{
"probability":{
"exp":0.5000000
},
"location":"location",
"assignments":[
{
"ref":"q6",
"value":0
},
{
"ref":"q7",
"value":1
}
],
"observables":[
]
}
]
}
]
},
{
"name":"process7",
"locations":[
{
"name":"location"
}
],
"initial-locations":[
"location"
],
"edges":[
{
"location":"location",
"action":"tau__",
"guard":{
"exp":{
"op":"=",
"left":"q7",
"right":1
}
},
"destinations":[
{
"probability":{
"exp":0.5000000
},
"location":"location",
"assignments":[
{
"ref":"q7",
"value":0
},
{
"ref":"q6",
"value":1
}
],
"observables":[
]
},
{
"probability":{
"exp":0.5000000
},
"location":"location",
"assignments":[
{
"ref":"q7",
"value":0
},
{
"ref":"q8",
"value":1
}
],
"observables":[
]
}
]
}
]
},
{
"name":"process8",
"locations":[
{
"name":"location"
}
],
"initial-locations":[
"location"
],
"edges":[
{
"location":"location",
"action":"tau__",
"guard":{
"exp":{
"op":"=",
"left":"q8",
"right":1
}
},
"destinations":[
{
"probability":{
"exp":0.5000000
},
"location":"location",
"assignments":[
{
"ref":"q8",
"value":0
},
{
"ref":"q7",
"value":1
}
],
"observables":[
]
},
{
"probability":{
"exp":0.5000000
},
"location":"location",
"assignments":[
{
"ref":"q8",
"value":0
},
{
"ref":"q9",
"value":1
}
],
"observables":[
]
}
]
}
]
},
{
"name":"process9",
"locations":[
{
"name":"location"
}
],
"initial-locations":[
"location"
],
"edges":[
{
"location":"location",
"action":"tau__",
"guard":{
"exp":{
"op":"=",
"left":"q9",
"right":1
}
},
"destinations":[
{
"probability":{
"exp":0.5000000
},
"location":"location",
"assignments":[
{
"ref":"q9",
"value":0
},
{
"ref":"q8",
"value":1
}
],
"observables":[
]
},
{
"probability":{
"exp":0.5000000
},
"location":"location",
"assignments":[
{
"ref":"q9",
"value":0
},
{
"ref":"q1",
"value":1
}
],
"observables":[
]
}
]
}
]
}
],
"system":{
"elements":[
{
"automaton":"process1"
},
{
"automaton":"process2"
},
{
"automaton":"process3"
},
{
"automaton":"process4"
},
{
"automaton":"process5"
},
{
"automaton":"process6"
},
{
"automaton":"process7"
},
{
"automaton":"process8"
},
{
"automaton":"process9"
}
],
"syncs":[
{
"synchronise":[
"tau__",
null,
null,
null,
null,
null,
null,
null,
null
],
"result":"tau__"
},
{
"synchronise":[
null,
"tau__",
null,
null,
null,
null,
null,
null,
null
],
"result":"tau__"
},
{
"synchronise":[
null,
null,
"tau__",
null,
null,
null,
null,
null,
null
],
"result":"tau__"
},
{
"synchronise":[
null,
null,
null,
"tau__",
null,
null,
null,
null,
null
],
"result":"tau__"
},
{
"synchronise":[
null,
null,
null,
null,
"tau__",
null,
null,
null,
null
],
"result":"tau__"
},
{
"synchronise":[
null,
null,
null,
null,
null,
"tau__",
null,
null,
null
],
"result":"tau__"
},
{
"synchronise":[
null,
null,
null,
null,
null,
null,
"tau__",
null,
null
],
"result":"tau__"
},
{
"synchronise":[
null,
null,
null,
null,
null,
null,
null,
"tau__",
null
],
"result":"tau__"
},
{
"synchronise":[
null,
null,
null,
null,
null,
null,
null,
null,
"tau__"
],
"result":"tau__"
}
]
}
}

835
examples/exported-jani-models/investor.jani
View File

@ -1,835 +0,0 @@
{
"jani-version":1,
"features":[
"derived-operators"
],
"name":"Converted from PRISM by IscasMC",
"type":"mdp",
"actions":[
{
"name":"invest"
},
{
"name":"month"
},
{
"name":"done"
}
],
"variables":[
{
"name":"m",
"type":{
"kind":"bounded",
"base":"int",
"lower-bound":0,
"upper-bound":1
}
},
{
"name":"i",
"type":{
"kind":"bounded",
"base":"int",
"lower-bound":0,
"upper-bound":1
}
},
{
"name":"b",
"type":{
"kind":"bounded",
"base":"int",
"lower-bound":0,
"upper-bound":1
}
},
{
"name":"v",
"type":{
"kind":"bounded",
"base":"int",
"lower-bound":0,
"upper-bound":10
}
},
{
"name":"p",
"type":{
"kind":"bounded",
"base":"int",
"lower-bound":0,
"upper-bound":10
}
},
{
"name":"c",
"type":{
"kind":"bounded",
"base":"int",
"lower-bound":0,
"upper-bound":10
}
}
],
"observables":[
],
"initial-states":{
"exp":{
"op":"∧",
"left":{
"op":"∧",
"left":{
"op":"∧",
"left":{
"op":"∧",
"left":{
"op":"∧",
"left":{
"op":"=",
"left":"m",
"right":0
},
"right":{
"op":"=",
"left":"i",
"right":0
}
},
"right":{
"op":"=",
"left":"b",
"right":1
}
},
"right":{
"op":"=",
"left":"v",
"right":10
}
},
"right":{
"op":"=",
"left":"p",
"right":5
}
},
"right":{
"op":"=",
"left":"c",
"right":10
}
}
},
"automata":[
{
"name":"month",
"locations":[
{
"name":"location"
}
],
"initial-locations":[
"location"
],
"edges":[
{
"location":"location",
"action":"invest",
"guard":{
"exp":{
"op":"=",
"left":"m",
"right":0
}
},
"destinations":[
{
"probability":{
"exp":1
},
"location":"location",
"assignments":[
{
"ref":"m",
"value":1
}
],
"observables":[
]
}
]
},
{
"location":"location",
"action":"month",
"guard":{
"exp":{
"op":"=",
"left":"m",
"right":1
}
},
"destinations":[
{
"probability":{
"exp":1
},
"location":"location",
"assignments":[
{
"ref":"m",
"value":0
}
],
"observables":[
]
}
]
},
{
"location":"location",
"action":"done",
"guard":{
"exp":{
"op":"=",
"left":"m",
"right":0
}
},
"destinations":[
{
"probability":{
"exp":1
},
"location":"location",
"assignments":[
{
"ref":"m",
"value":0
}
],
"observables":[
]
}
]
}
]
},
{
"name":"investor",
"locations":[
{
"name":"location"
}
],
"initial-locations":[
"location"
],
"edges":[
{
"location":"location",
"action":"invest",
"guard":{
"exp":{
"op":"=",
"left":"i",
"right":0
}
},
"destinations":[
{
"probability":{
"exp":1
},
"location":"location",
"assignments":[
{
"ref":"i",
"value":0
}
]
}
]
},
{
"location":"location",
"action":"invest",
"guard":{
"exp":{
"op":"=",
"left":"i",
"right":0
}
},
"destinations":[
{
"probability":{
"exp":1
},
"location":"location",
"assignments":[
{
"ref":"i",
"value":1
}
]
}
]
},
{
"location":"location",
"action":"invest",
"guard":{
"exp":{
"op":"∧",
"left":{
"op":"=",
"left":"i",
"right":1
},
"right":{
"op":"=",
"left":"b",
"right":1
}
}
},
"destinations":[
{
"probability":{
"exp":1
},
"location":"location",
"assignments":[
{
"ref":"i",
"value":0
}
]
}
]
},
{
"location":"location",
"action":"invest",
"guard":{
"exp":{
"op":"∧",
"left":{
"op":"=",
"left":"i",
"right":1
},
"right":{
"op":"=",
"left":"b",
"right":1
}
}
},
"destinations":[
{
"probability":{
"exp":1
},
"location":"location",
"assignments":[
{
"ref":"i",
"value":1
}
]
}
]
},
{
"location":"location",
"action":"done",
"guard":{
"exp":{
"op":"∧",
"left":{
"op":"=",
"left":"i",
"right":1
},
"right":{
"op":"=",
"left":"b",
"right":0
}
}
},
"destinations":[
{
"probability":{
"exp":1
},
"location":"location",
"assignments":[
{
"ref":"i",
"value":1
}
]
}
]
}
]
},
{
"name":"barred",
"locations":[
{
"name":"location"
}
],
"initial-locations":[
"location"
],
"edges":[
{
"location":"location",
"action":"invest",
"guard":{
"exp":true
},
"destinations":[
{
"probability":{
"exp":1
},
"location":"location",
"assignments":[
{
"ref":"b",
"value":0
}
]
}
]
},
{
"location":"location",
"action":"invest",
"guard":{
"exp":{
"op":"=",
"left":"b",
"right":0
}
},
"destinations":[
{
"probability":{
"exp":1
},
"location":"location",
"assignments":[
{
"ref":"b",
"value":1
}
]
}
]
}
]
},
{
"name":"value",
"locations":[
{
"name":"location"
}
],
"initial-locations":[
"location"
],
"edges":[
{
"location":"location",
"action":"month",
"guard":{
"exp":true
},
"destinations":[
{
"probability":{
"exp":{
"op":"/",
"left":"p",
"right":10
}
},
"location":"location",
"assignments":[
{
"ref":"v",
"value":{
"op":"min",
"left":{
"op":"+",
"left":"v",
"right":1
},
"right":"c"
}
}
]
},
{
"probability":{
"exp":{
"op":"-",
"left":1,
"right":{
"op":"/",
"left":"p",
"right":10
}
}
},
"location":"location",
"assignments":[
{
"ref":"v",
"value":{
"op":"min",
"left":{
"op":"max",
"left":{
"op":"-",
"left":"v",
"right":1
},
"right":0
},
"right":"c"
}
}
]
}
]
}
]
},
{
"name":"probability",
"locations":[
{
"name":"location"
}
],
"initial-locations":[
"location"
],
"edges":[
{
"location":"location",
"action":"month",
"guard":{
"exp":{
"op":"<",
"left":"v",
"right":5
}
},
"destinations":[
{
"probability":{
"exp":{
"op":"/",
"left":2,
"right":3
}
},
"location":"location",
"assignments":[
{
"ref":"p",
"value":{
"op":"min",
"left":{
"op":"+",
"left":"p",
"right":1
},
"right":10
}
}
]
},
{
"probability":{
"exp":{
"op":"/",
"left":1,
"right":3
}
},
"location":"location",
"assignments":[
{
"ref":"p",
"value":{
"op":"max",
"left":{
"op":"-",
"left":"p",
"right":1
},
"right":0
}
}
]
}
]
},
{
"location":"location",
"action":"month",
"guard":{
"exp":{
"op":"=",
"left":"v",
"right":5
}
},
"destinations":[
{
"probability":{
"exp":{
"op":"/",
"left":1,
"right":2
}
},
"location":"location",
"assignments":[
{
"ref":"p",
"value":{
"op":"min",
"left":{
"op":"+",
"left":"p",
"right":1
},
"right":10
}
}
]
},
{
"probability":{
"exp":{
"op":"/",
"left":1,
"right":2
}
},
"location":"location",
"assignments":[
{
"ref":"p",
"value":{
"op":"max",
"left":{
"op":"-",
"left":"p",
"right":1
},
"right":0
}
}
]
}
]
},
{
"location":"location",
"action":"month",
"guard":{
"exp":{
"op":">",
"left":"v",
"right":5
}
},
"destinations":[
{
"probability":{
"exp":{
"op":"/",
"left":1,
"right":3
}
},
"location":"location",
"assignments":[
{
"ref":"p",
"value":{
"op":"min",
"left":{
"op":"+",
"left":"p",
"right":1
},
"right":10
}
}
]
},
{
"probability":{
"exp":{
"op":"/",
"left":2,
"right":3
}
},
"location":"location",
"assignments":[
{
"ref":"p",
"value":{
"op":"max",
"left":{
"op":"-",
"left":"p",
"right":1
},
"right":0
}
}
]
}
]
}
]
},
{
"name":"cap",
"locations":[
{
"name":"location"
}
],
"initial-locations":[
"location"
],
"edges":[
{
"location":"location",
"action":"month",
"guard":{
"exp":true
},
"destinations":[
{
"probability":{
"exp":{
"op":"/",
"left":1,
"right":2
}
},
"location":"location",
"assignments":[
{
"ref":"c",
"value":{
"op":"max",
"left":{
"op":"-",
"left":"c",
"right":1
},
"right":0
}
}
]
},
{
"probability":{
"exp":{
"op":"/",
"left":1,
"right":2
}
},
"location":"location",
"assignments":[
{
"ref":"c",
"value":"c"
}
]
}
]
}
]
}
],
"system":{
"elements":[
{
"automaton":"month"
},
{
"automaton":"investor"
},
{
"automaton":"barred"
},
{
"automaton":"value"
},
{
"automaton":"probability"
},
{
"automaton":"cap"
}
],
"syncs":[
{
"synchronise":[
"month",
null,
null,
"month",
"month",
"month"
],
"result":"month"
},
{
"synchronise":[
"invest",
"invest",
"invest",
null,
null,
null
],
"result":"invest"
},
{
"synchronise":[
"done",
"done",
null,
null,
null,
null
],
"result":"done"
}
]
}
}

1584
examples/exported-jani-models/kaminsky.jani
File diff suppressed because it is too large
View File

1580
examples/exported-jani-models/kanban.jani
File diff suppressed because it is too large
View File

683
examples/exported-jani-models/knacl.jani
View File

@ -1,683 +0,0 @@
{
"jani-version":1,
"features":[
"derived-operators"
],
"name":"Converted from PRISM by IscasMC",
"type":"ctmc",
"actions":[
{
"name":"e1"
},
{
"name":"e2"
},
{
"name":"e3"
},
{
"name":"e4"
}
],
"constants":[
{
"name":"N1",
"type":"int"
},
{
"name":"N2",
"type":"int"
},
{
"name":"N3",
"type":"int"
}
],
"variables":[
{
"name":"na",
"type":{
"kind":"bounded",
"base":"int",
"lower-bound":0,
"upper-bound":"N1"
}
},
{
"name":"cl",
"type":{
"kind":"bounded",
"base":"int",
"lower-bound":0,
"upper-bound":"N2"
}
},
{
"name":"k",
"type":{
"kind":"bounded",
"base":"int",
"lower-bound":0,
"upper-bound":"N3"
}
},
{
"name":"dummy",
"type":"bool"
}
],
"observables":[
{
"name":"\"percentage_na\""
},
{
"name":"\"percentage_k\""
}
],
"initial-states":{
"exp":{
"op":"∧",
"left":{
"op":"∧",
"left":{
"op":"∧",
"left":{
"op":"=",
"left":"na",
"right":"N1"
},
"right":{
"op":"=",
"left":"cl",
"right":"N2"
}
},
"right":{
"op":"=",
"left":"k",
"right":"N3"
}
},
"right":{
"op":"=",
"left":"dummy",
"right":false
}
}
},
"automata":[
{
"name":"na",
"locations":[
{
"name":"location",
"observables":[
{
"ref":"\"percentage_na\"",
"value":{
"op":"/",
"left":{
"op":"*",
"left":100,
"right":"na"
},
"right":"N1"
}
},
{
"ref":"\"percentage_k\"",
"value":{
"op":"/",
"left":{
"op":"*",
"left":100,
"right":"k"
},
"right":"N3"
}
}
]
}
],
"initial-locations":[
"location"
],
"edges":[
{
"location":"location",
"action":"e1",
"rate":{
"exp":"na"
},
"guard":{
"exp":{
"op":">",
"left":"na",
"right":0
}
},
"destinations":[
{
"probability":{
"exp":{
"op":"/",
"left":"na",
"right":"na"
}
},
"location":"location",
"assignments":[
{
"ref":"na",
"value":{
"op":"-",
"left":"na",
"right":1
}
}
],
"observables":[
]
}
]
},
{
"location":"location",
"action":"e2",
"rate":{
"exp":{
"op":"-",
"left":"N1",
"right":"na"
}
},
"guard":{
"exp":{
"op":"<",
"left":"na",
"right":"N1"
}
},
"destinations":[
{
"probability":{
"exp":{
"op":"/",
"left":{
"op":"-",
"left":"N1",
"right":"na"
},
"right":{
"op":"-",
"left":"N1",
"right":"na"
}
}
},
"location":"location",
"assignments":[
{
"ref":"na",
"value":{
"op":"+",
"left":"na",
"right":1
}
}
],
"observables":[
]
}
]
}
]
},
{
"name":"cl",
"locations":[
{
"name":"location"
}
],
"initial-locations":[
"location"
],
"edges":[
{
"location":"location",
"action":"e1",
"rate":{
"exp":"cl"
},
"guard":{
"exp":{
"op":">",
"left":"cl",
"right":0
}
},
"destinations":[
{
"probability":{
"exp":{
"op":"/",
"left":"cl",
"right":"cl"
}
},
"location":"location",
"assignments":[
{
"ref":"cl",
"value":{
"op":"-",
"left":"cl",
"right":1
}
}
]
}
]
},
{
"location":"location",
"action":"e3",
"rate":{
"exp":"cl"
},
"guard":{
"exp":{
"op":">",
"left":"cl",
"right":0
}
},
"destinations":[
{
"probability":{
"exp":{
"op":"/",
"left":"cl",
"right":"cl"
}
},
"location":"location",
"assignments":[
{
"ref":"cl",
"value":{
"op":"-",
"left":"cl",
"right":1
}
}
],
"observables":[
]
}
]
},
{
"location":"location",
"action":"e2",
"rate":{
"exp":{
"op":"-",
"left":"N2",
"right":"cl"
}
},
"guard":{
"exp":{
"op":"<",
"left":"cl",
"right":"N2"
}
},
"destinations":[
{
"probability":{
"exp":{
"op":"/",
"left":{
"op":"-",
"left":"N2",
"right":"cl"
},
"right":{
"op":"-",
"left":"N2",
"right":"cl"
}
}
},
"location":"location",
"assignments":[
{
"ref":"cl",
"value":{
"op":"+",
"left":"cl",
"right":1
}
}
]
}
]
},
{
"location":"location",
"action":"e4",
"rate":{
"exp":{
"op":"-",
"left":"N2",
"right":"cl"
}
},
"guard":{
"exp":{
"op":"<",
"left":"cl",
"right":"N2"
}
},
"destinations":[
{
"probability":{
"exp":{
"op":"/",
"left":{
"op":"-",
"left":"N2",
"right":"cl"
},
"right":{
"op":"-",
"left":"N2",
"right":"cl"
}
}
},
"location":"location",
"assignments":[
{
"ref":"cl",
"value":{
"op":"+",
"left":"cl",
"right":1
}
}
],
"observables":[
]
}
]
}
]
},
{
"name":"k",
"locations":[
{
"name":"location"
}
],
"initial-locations":[
"location"
],
"edges":[
{
"location":"location",
"action":"e3",
"rate":{
"exp":"k"
},
"guard":{
"exp":{
"op":">",
"left":"k",
"right":0
}
},
"destinations":[
{
"probability":{
"exp":{
"op":"/",
"left":"k",
"right":"k"
}
},
"location":"location",
"assignments":[
{
"ref":"k",
"value":{
"op":"-",
"left":"k",
"right":1
}
}
]
}
]
},
{
"location":"location",
"action":"e4",
"rate":{
"exp":{
"op":"-",
"left":"N3",
"right":"k"
}
},
"guard":{
"exp":{
"op":"<",
"left":"k",
"right":"N3"
}
},
"destinations":[
{
"probability":{
"exp":{
"op":"/",
"left":{
"op":"-",
"left":"N3",
"right":"k"
},
"right":{
"op":"-",
"left":"N3",
"right":"k"
}
}
},
"location":"location",
"assignments":[
{
"ref":"k",
"value":{
"op":"+",
"left":"k",
"right":1
}
}
]
}
]
}
]
},
{
"name":"base_rates",
"locations":[
{
"name":"location"
}
],
"initial-locations":[
"location"
],
"edges":[
{
"location":"location",
"action":"e1",
"rate":{
"exp":100
},
"guard":{
"exp":true
},
"destinations":[
{
"probability":{
"exp":{
"op":"/",
"left":100,
"right":100
}
},
"location":"location",
"assignments":[
]
}
]
},
{
"location":"location",
"action":"e2",
"rate":{
"exp":10
},
"guard":{
"exp":true
},
"destinations":[
{
"probability":{
"exp":{
"op":"/",
"left":10,
"right":10
}
},
"location":"location",
"assignments":[
]
}
]
},
{
"location":"location",
"action":"e3",
"rate":{
"exp":30
},
"guard":{
"exp":true
},
"destinations":[
{
"probability":{
"exp":{
"op":"/",
"left":30,
"right":30
}
},
"location":"location",
"assignments":[
]
}
]
},
{
"location":"location",
"action":"e4",
"rate":{
"exp":20
},
"guard":{
"exp":true
},
"destinations":[
{
"probability":{
"exp":{
"op":"/",
"left":20,
"right":20
}
},
"location":"location",
"assignments":[
]
}
]
}
]
}
],
"system":{
"elements":[
{
"automaton":"na"
},
{
"automaton":"cl"
},
{
"automaton":"k"
},
{
"automaton":"base_rates"
}
],
"syncs":[
{
"synchronise":[
null,
"e3",
"e3",
"e3"
],
"result":"e3"
},
{
"synchronise":[
null,
"e4",
"e4",
"e4"
],
"result":"e4"
},
{
"synchronise":[
"e1",
"e1",
null,
"e1"
],
"result":"e1"
},
{
"synchronise":[
"e2",
"e2",
null,
"e2"
],
"result":"e2"
}
]
}
}

9214
examples/exported-jani-models/leader_async_10.jani
File diff suppressed because it is too large
View File

2739
examples/exported-jani-models/leader_async_3.jani
File diff suppressed because it is too large
View File

3646
examples/exported-jani-models/leader_async_4.jani
File diff suppressed because it is too large
View File

4559
examples/exported-jani-models/leader_async_5.jani
File diff suppressed because it is too large
View File

5478
examples/exported-jani-models/leader_async_6.jani
File diff suppressed because it is too large
View File

6403
examples/exported-jani-models/leader_async_7.jani
File diff suppressed because it is too large
View File

7334
examples/exported-jani-models/leader_async_8.jani
File diff suppressed because it is too large
View File

8271
examples/exported-jani-models/leader_async_9.jani
File diff suppressed because it is too large
View File

1687
examples/exported-jani-models/leader_sync_3_2.jani
File diff suppressed because it is too large
View File

1777
examples/exported-jani-models/leader_sync_3_3.jani
File diff suppressed because it is too large
View File

1867
examples/exported-jani-models/leader_sync_3_4.jani
File diff suppressed because it is too large
View File

1957
examples/exported-jani-models/leader_sync_3_5.jani
File diff suppressed because it is too large
View File

2047
examples/exported-jani-models/leader_sync_3_6.jani
File diff suppressed because it is too large
View File

2227
examples/exported-jani-models/leader_sync_3_8.jani
File diff suppressed because it is too large
View File

2165
examples/exported-jani-models/leader_sync_4_2.jani
File diff suppressed because it is too large
View File

2283
examples/exported-jani-models/leader_sync_4_3.jani
File diff suppressed because it is too large
View File

2401
examples/exported-jani-models/leader_sync_4_4.jani
File diff suppressed because it is too large
View File

2519
examples/exported-jani-models/leader_sync_4_5.jani
File diff suppressed because it is too large
View File

2637
examples/exported-jani-models/leader_sync_4_6.jani
File diff suppressed because it is too large
View File

2873
examples/exported-jani-models/leader_sync_4_8.jani
File diff suppressed because it is too large
View File

2643
examples/exported-jani-models/leader_sync_5_2.jani
File diff suppressed because it is too large
View File

Some files were not shown because too many files changed in this diff

Write Preview
|||||||
100:0
Loading…
Cancel
Save