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

Merge branch 'future' into jani_support 

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

5
.gitignore
View File

@ -3,7 +3,8 @@ resources/3rdparty/log4cplus-1.1.3-rc1/
resources/3rdparty/gtest-1.7.0/
resources/3rdparty/eigen/
resources/3rdparty/gmm-4.2/
resources/3rdparty/cudd-2.5.0/
resources/3rdparty/cudd-3.0.0/
resources/3rdparty/carl/
resources/3rdparty/xercesc-3.1.2/
#Visual Studio files
*.[Oo]bj
@ -49,4 +50,4 @@ src/utility/storm-version.cpp
nbproject/
.DS_Store
.idea
*.out
*.out

5
CMakeLists.txt
View File

@ -29,13 +29,14 @@ option(USE_BOOST_STATIC_LIBRARIES "Sets whether the Boost libraries should be li
option(STORM_USE_INTELTBB "Sets whether the Intel TBB libraries should be used." OFF)
option(STORM_USE_GUROBI "Sets whether Gurobi should be used." OFF)
option(USE_CARL "Sets whether carl should be included." ON)
option(USE_XERCES "Sets whether xerces should be used." OFF)
option(XML_SUPPORT "Sets whether xml based format parsing should be included." ON)
option(FORCE_COLOR "Force color output" OFF)
mark_as_advanced(FORCE_COLOR)
option(STORM_PYTHON "Builds the API for Python" OFF)
option(STORM_COMPILE_WITH_CCACHE "Compile using CCache [if found]" ON)
mark_as_advanced(STORM_COMPILE_WITH_CCACHE)
option(STORM_LOG_DISABLE_DEBUG "Disable log and trace message support" OFF)
option(STORM_USE_CLN_NUMBERS "Sets whether CLN or GMP numbers should be used" ON)
set(BOOST_ROOT "" CACHE STRING "A hint to the root directory of Boost (optional).")
set(GUROBI_ROOT "" CACHE STRING "A hint to the root directory of Gurobi (optional).")
set(Z3_ROOT "" CACHE STRING "A hint to the root directory of Z3 (optional).")
@ -43,6 +44,8 @@ set(CUDA_ROOT "" CACHE STRING "The hint to the root directory of CUDA (optional)
set(MSAT_ROOT "" CACHE STRING "The hint to the root directory of MathSAT (optional).")
set(ADDITIONAL_INCLUDE_DIRS "" CACHE STRING "Additional directories added to the include directories.")
set(ADDITIONAL_LINK_DIRS "" CACHE STRING "Additional directories added to the link directories.")
set(USE_XERCES ${XML_SUPPORT})
mark_as_advanced(USE_XERCES)
# Set some CMAKE Variables as advanced
mark_as_advanced(CMAKE_OSX_ARCHITECTURES)

5
examples/dft/and_approx.dft
View File

@ -0,0 +1,5 @@
toplevel "A";
"A" and "B" "C" "D";
"B" lambda=1 dorm=0;
"C" lambda=100 dorm=0;
"D" lambda=50 dorm=0;

6
examples/dft/and_approx_param.dft
View File

@ -0,0 +1,6 @@
param x;
toplevel "A";
"A" and "B" "C" "D";
"B" lambda=1 dorm=0;
"C" lambda=100 dorm=0;
"D" lambda=100*x dorm=0;

5
examples/dft/approx.dft
View File

@ -0,0 +1,5 @@
toplevel "A";
"A" and "B" "C" "D";
"B" lambda=0.1 dorm=0;
"C" lambda=10 dorm=0;
"D" lambda=0.1 dorm=0;

7
examples/dft/fdep4.dft
View File

@ -0,0 +1,7 @@
toplevel "A";
"A" or "F" "B";
"F" fdep "E" "C" "D";
"B" wsp "C" "D";
"C" lambda=1 dorm=0;
"D" lambda=1 dorm=0.5;
"E" lambda=0.5 dorm=0;

58
examples/dft/mas.dft
View File

@ -0,0 +1,58 @@
toplevel "MAS";
"MAS" or "CPU" "DB" "MB" "VMB" "MEM" "VMS";
"CPU" or "CW" "SO1" "SO2" "PG" "SM";
"CW" and "CWA" "CWB";
"SO1" and "SO1A" "SO1B";
"SO2" and "SO2A" "SO2B";
"PG" and "PGA" "PGB";
"SM" and "SMA" "SMB";
"CWA" csp "CWAev" "S1" "S2";
"CWB" csp "CWBev" "S1" "S2";
"SO1A" csp "SO1Aev" "S1" "S2";
"SO1B" csp "SO1Bev" "S1" "S2";
"SO2A" csp "SO2Aev" "S1" "S2";
"SO2B" csp "SO2Bev" "S1" "S2";
"PGA" csp "PGAev" "S1" "S2";
"PGB" csp "PGBev" "S1" "S2";
"SMA" csp "SMAev" "S1" "S2";
"SMB" csp "SMBev" "S1" "S2";
"CWAev" lambda=1.0e-6 dorm=0;
"CWBev" lambda=1.0e-6 dorm=0;
"SO1Aev" lambda=1.0e-6 dorm=0;
"SO1Bev" lambda=1.0e-6 dorm=0;
"SO2Aev" lambda=1.0e-6 dorm=0;
"SO2Bev" lambda=1.0e-6 dorm=0;
"PGAev" lambda=1.0e-6 dorm=0;
"PGBev" lambda=1.0e-6 dorm=0;
"SMAev" lambda=1.0e-6 dorm=0;
"SMBev" lambda=1.0e-6 dorm=0;
"S1" lambda=1.0e-6 dorm=0;
"S2" lambda=1.0e-6 dorm=0;
"DB" and "DB1" "DB2" "DB3";
"DB1" lambda=5.0e-6 dorm=0;
"DB2" lambda=5.0e-6 dorm=0;
"DB3" lambda=5.0e-6 dorm=0;
"MB" and "MB1" "MB2" "MB3";
"MB1" lambda=5.0e-6 dorm=0;
"MB2" lambda=5.0e-6 dorm=0;
"MB3" lambda=5.0e-6 dorm=0;
"VMB" and "VMB1" "VMB2";
"VMB1" lambda=5.0e-6 dorm=0;
"VMB2" lambda=5.0e-6 dorm=0;
"MEM" and "MEM1" "MEM2";
"MEM1" lambda=1.0e-5 dorm=0;
"MEM2" lambda=1.0e-5 dorm=0;
"VMS" or "VM1" "VM2";
"VM1" and "VM1A" "VM1B";
"VM2" and "VM2A" "VM2B";
"VM1A" csp "VM1Aev" "VMS1" "VMS2";
"VM1B" csp "VM1Bev" "VMS1" "VMS2";
"VM2A" csp "VM2Aev" "VMS1" "VMS2";
"VM2B" csp "VM2Bev" "VMS1" "VMS2";
"VM1Aev" lambda=1.0e-6 dorm=0;
"VM1Bev" lambda=1.0e-6 dorm=0;
"VM2Aev" lambda=1.0e-6 dorm=0;
"VM2Bev" lambda=1.0e-6 dorm=0;
"VMS1" lambda=1.0e-6 dorm=0;
"VMS2" lambda=1.0e-6 dorm=0;

6
examples/dft/nonmonoton.dft
View File

@ -0,0 +1,6 @@
toplevel "A";
"A" or "B" "Z";
"B" pand "D" "S";
"Z" lambda=1 dorm=0;
"D" lambda=100 dorm=0;
"S" lambda=50 dorm=0;

8
examples/dft/nonmonoton_param.dft
View File

@ -2,7 +2,7 @@ param x;
param y;
toplevel "A";
"A" or "B" "Z";
"B" pand "D" "S";
"Z" lambda=y dorm=0;
"D" lambda=100 dorm=0;
"S" lambda=100*x dorm=0;
"Z" pand "C" "D";
"B" lambda=y dorm=0;
"C" lambda=100 dorm=0;
"D" lambda=100*x dorm=0;

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

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

Write Preview
Loading…
Cancel
Save