Add tests for introduced datatypes

This commit is contained in:
Matej Trojak
2022-07-22 11:11:12 -05:00
parent a6454f0960
commit 5241c609a1
14 changed files with 539 additions and 0 deletions
@@ -0,0 +1,13 @@
VARS: pRB, E2F1
PARAMS: y_pRB,0.001,1; y_E2F1,0.001,1
CONSTS: a,0.04; kp,0.05; k2,1; k1,1
VAR_POINTS: pRB: 1500, 20; E2F1: 1500, 20
EQ: pRB = k1*Hillp(E2F1,0.5,1,0,1)*Hillm(pRB,0.5,1,1,0) - y_pRB*pRB
EQ: E2F1 = kp + k2*a*a*0.0625*Hillm(E2F1,4,2,1,0)*Hillm(pRB,5,1,1,0) + k2*Hillp(E2F1,4,2,0,1)*Hillm(pRB,5,1,1,0) - y_E2F1*E2F1
THRES: pRB: 0, 15
THRES: E2F1: 0, 3, 15
@@ -0,0 +1,10 @@
# high state of E2F1 (observed in cancer cells)
high = E2F1 > 3
# low state of E2F1 (observed in healthy cells)
low = E2F1 < 3
:?stay_low = AG low
:?stay_high = AG high
:?reach_high = EF high
:?reach_low = EF low
:?bistability = reach_and_stay_high && reach_and_stay_low
@@ -0,0 +1 @@
{"variables":["pRB","E2F1"],"parameters":["y_pRB"],"thresholds":[[0.0,0.02334889926617745,0.0466977985323549,0.07004669779853236,0.0933955970647098,0.11674449633088725,0.1400933955970647,0.16344229486324216,0.1867911941294196,0.21014009339559706,0.2334889926617745,0.256837891927952,0.2801867911941294,0.3035356904603069,0.35023348899266177,0.39693128752501666]],"parameter_bounds":[[0.0,1.0]],"states":[{"id":8717,"bounds":[[1.3308872581721147,1.4242828552368245],[11.227484989993329,11.587725150100066]]},{"id":8718,"bounds":[[1.4242828552368245,1.5176784523015343],[11.227484989993329,11.587725150100066]]},{"id":8719,"bounds":[[1.5176784523015343,1.611074049366244],[11.227484989993329,11.587725150100066]]},{"id":8720,"bounds":[[1.611074049366244,1.7044696464309539],[11.227484989993329,11.587725150100066]]},{"id":8721,"bounds":[[1.7044696464309539,1.8212141427618411],[11.227484989993329,11.587725150100066]]}],"type":"rectangular","parameter_values":[[[[0.174655571734003,0.17511282157273875]]],[[[0.15632047914681707,0.17511282157273875]]],[[[0.14055859185879657,0.1567297275502395]]],[[[0.12705696870430946,0.14093038684771772]]],[[[0.12705696870430946,0.1275646137723884]]],[[[0.08037989357199904,0.0807182318621894]]],[[[0.07171486575321386,0.0807182318621894]]],[[[0.06437073836837151,0.07202650145489457]]],[[[0.06437073836837151,0.06465910081655664]]],[[[0.0039941330464278125,0.004253357302638203]]],[[[0.003677177243966719,0.004253357302638203]]]],"results":[{"formula":"1 attractor(s)","data":[[0,0],[1,1],[2,2],[3,3],[4,4],[5,5],[6,6],[7,7],[8,8],[9,9],[10,10],[11,11],[12,12],[13,13],[14,14],[15,15],[16,16],[17,17],[18,18],[19,19],[20,20],[21,21],[22,22],[23,23],[24,24],[25,25],[26,26],[27,27],[28,28],[29,29],[30,30],[31,31],[32,32],[33,33],[34,34],[35,35]]},{"formula":"2 attractor(s)","data":[[197,131],[198,132],[199,133],[33,134],[109,135],[200,136],[111,137]]}]}
@@ -0,0 +1,24 @@
Storm 1.5.2 (dev)
Date: Tue Aug 31 11:52:43 2021
Command line arguments: --explicit /tmp/exp_transitions.tra /tmp/exp_labels.lab --prop 'P <= 0.2 [F "property_0"]'
Current working directory: /home/biodivine
WARN (DeterministicSparseTransitionParser.cpp:114): Warning while parsing /tmp/exp_transitions.tra: state 0 has no outgoing transitions. A self-loop was inserted.
Time for model construction: 0.003s.
--------------------------------------------------------------
Model type: DTMC (sparse)
States: 36
Transitions: 73
Reward Models: none
State Labels: 2 labels
* property_0 -> 7 item(s)
* init -> 1 item(s)
Choice Labels: none
--------------------------------------------------------------
Model checking property "1": P<=1/5 [F "property_0"] ...
Result (for initial states): true
Time for model checking: 0.004s.
@@ -0,0 +1,166 @@
Storm-pars 1.5.2 (dev)
Date: Tue Aug 31 11:53:48 2021
Command line arguments: --prism /tmp/prism-parametric.pm --prop 'P <= 0.2 [F VAR_13 > 0]' --region '0.1<=param_sig<=0.6,0.05<=param_block<=1.0' --refine 0.01 10 --printfullresult
Current working directory: /home/biodivine
Time for model input parsing: 0.049s.
Time for model construction: 0.074s.
--------------------------------------------------------------
Model type: DTMC (sparse)
States: 31
Transitions: 60
Reward Models: none
State Labels: 3 labels
* deadlock -> 0 item(s)
* init -> 1 item(s)
* (VAR_13 > 0) -> 3 item(s)
Choice Labels: none
--------------------------------------------------------------
Analyzing parameter region 1/20<=param_block<=1,1/10<=param_sig<=3/5; using Parameter Lifting with iterative refinement until 99% is covered. Depth limit is 10.
Model checking property "1": P<=1/5 [F (VAR_13 > 0)] ...
WARN (parameterlifting.h:42): The input model contains a non-linear polynomial as transition: '(4)/(5*param_block+4)'. Can not validate that parameter lifting is sound on this model.
WARN (region.h:86): Could not validate whether parameter lifting is applicable. Please validate manually...
Result (initial states): Fraction of satisfied area: 80.8105%
Fraction of unsatisfied area: 18.1946%
Unknown fraction: 0.994873%
Total number of regions: 940
Unknown: 628
ExistsSat: 6
AllSat: 151
AllViolated: 155
Region results:
21/40<=param_block<=1,1/10<=param_sig<=7/20;: AllSat
21/40<=param_block<=1,7/20<=param_sig<=3/5;: AllSat
23/80<=param_block<=21/40,1/10<=param_sig<=9/40;: AllSat
23/80<=param_block<=21/40,9/40<=param_sig<=7/20;: AllSat
23/80<=param_block<=21/40,7/20<=param_sig<=19/40;: AllSat
27/160<=param_block<=23/80,1/10<=param_sig<=13/80;: AllSat
1/20<=param_block<=27/160,9/40<=param_sig<=23/80;: AllViolated
1/20<=param_block<=27/160,23/80<=param_sig<=7/20;: AllViolated
1/20<=param_block<=27/160,7/20<=param_sig<=33/80;: AllViolated
1/20<=param_block<=27/160,33/80<=param_sig<=19/40;: AllViolated
1/20<=param_block<=27/160,19/40<=param_sig<=43/80;: AllViolated
1/20<=param_block<=27/160,43/80<=param_sig<=3/5;: AllViolated
47/256<=param_block<=127/640,31/160<=param_sig<=129/640;: AllSat
47/256<=param_block<=127/640,129/640<=param_sig<=67/320;: AllSat
47/256<=param_block<=127/640,67/320<=param_sig<=139/640;: AllSat
27/160<=param_block<=47/256,9/40<=param_sig<=149/640;: AllViolated
27/160<=param_block<=47/256,149/640<=param_sig<=77/320;: AllViolated
27/160<=param_block<=47/256,77/320<=param_sig<=159/640;: AllViolated
27/160<=param_block<=47/256,159/640<=param_sig<=41/160;: AllViolated
127/640<=param_block<=273/1280,77/320<=param_sig<=159/640;: AllSat
273/1280<=param_block<=73/320,77/320<=param_sig<=159/640;: AllSat
273/1280<=param_block<=73/320,159/640<=param_sig<=41/160;: AllSat
273/1280<=param_block<=73/320,41/160<=param_sig<=169/640;: AllSat
273/1280<=param_block<=73/320,169/640<=param_sig<=87/320;: AllSat
273/1280<=param_block<=73/320,87/320<=param_sig<=179/640;: AllSat
127/640<=param_block<=273/1280,23/80<=param_sig<=189/640;: AllViolated
127/640<=param_block<=273/1280,189/640<=param_sig<=97/320;: AllViolated
273/1280<=param_block<=73/320,209/640<=param_sig<=107/320;: AllViolated
311/1280<=param_block<=33/128,51/160<=param_sig<=209/640;: AllSat
311/1280<=param_block<=33/128,209/640<=param_sig<=107/320;: AllSat
311/1280<=param_block<=33/128,107/320<=param_sig<=219/640;: AllSat
311/1280<=param_block<=33/128,219/640<=param_sig<=7/20;: AllSat
311/1280<=param_block<=33/128,7/20<=param_sig<=229/640;: AllSat
73/320<=param_block<=311/1280,117/320<=param_sig<=239/640;: AllViolated
73/320<=param_block<=311/1280,239/640<=param_sig<=61/160;: AllViolated
73/320<=param_block<=311/1280,61/160<=param_sig<=249/640;: AllViolated
73/320<=param_block<=311/1280,249/640<=param_sig<=127/320;: AllViolated
73/320<=param_block<=311/1280,127/320<=param_sig<=259/640;: AllViolated
73/320<=param_block<=311/1280,259/640<=param_sig<=33/80;: AllViolated
33/128<=param_block<=349/1280,127/320<=param_sig<=259/640;: AllSat
349/1280<=param_block<=23/80,127/320<=param_sig<=259/640;: AllSat
349/1280<=param_block<=23/80,259/640<=param_sig<=33/80;: AllSat
349/1280<=param_block<=23/80,33/80<=param_sig<=269/640;: AllSat
349/1280<=param_block<=23/80,71/160<=param_sig<=289/640;: AllSat
33/128<=param_block<=349/1280,299/640<=param_sig<=19/40;: AllViolated
33/128<=param_block<=349/1280,19/40<=param_sig<=309/640;: AllViolated
33/128<=param_block<=349/1280,309/640<=param_sig<=157/320;: AllViolated
151/512<=param_block<=1529/5120,1501/2560<=param_sig<=753/1280;: Unknown
1529/5120<=param_block<=387/1280,1501/2560<=param_sig<=753/1280;: Unknown
151/512<=param_block<=1529/5120,753/1280<=param_sig<=1511/2560;: Unknown
1529/5120<=param_block<=387/1280,753/1280<=param_sig<=1511/2560;: Unknown
151/512<=param_block<=1529/5120,1511/2560<=param_sig<=379/640;: Unknown
1529/5120<=param_block<=387/1280,1511/2560<=param_sig<=379/640;: Unknown
387/1280<=param_block<=1567/5120,187/320<=param_sig<=1501/2560;: Unknown
1567/5120<=param_block<=793/2560,187/320<=param_sig<=1501/2560;: Unknown
387/1280<=param_block<=1567/5120,1501/2560<=param_sig<=753/1280;: Unknown
1567/5120<=param_block<=793/2560,1501/2560<=param_sig<=753/1280;: Unknown
Region refinement Check result (visualization):
x-axis: param_block y-axis: param_sig S=safe, [ ]=unsafe, -=ambiguous
##################################################################################################################################
# --SSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSS#
# ---SSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSS#
# -SSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSS#
# -SSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSS#
# -SSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSS#
# -SSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSS#
# --SSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSS#
# -SSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSS#
# -SSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSS#
# -SSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSS#
# --SSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSS#
# -SSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSS#
# -SSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSS#
# -SSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSS#
# --SSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSS#
# -SSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSS#
# -SSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSS#
# --SSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSS#
# --SSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSS#
# -SSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSS#
# -SSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSS#
# --SSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSS#
# -SSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSS#
# -SSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSS#
# --SSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSS#
# -SSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSS#
# -SSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSS#
# --SSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSS#
# -SSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSS#
# -SSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSS#
# --SSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSS#
# -SSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSS#
# --SSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSS#
# --SSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSS#
# -SSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSS#
# --SSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSS#
# -SSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSS#
# --SSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSS#
# -SSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSS#
# -SSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSS#
# --SSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSS#
# -SSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSS#
# --SSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSS#
# -SSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSS#
# --SSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSS#
# -SSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSS#
# --SSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSS#
# -SSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSS#
# --SSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSS#
# --SSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSS#
# -SSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSS#
# --SSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSS#
# -SSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSS#
# --SSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSS#
# --SSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSS#
# -SSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSS#
# --SSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSS#
# --SSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSS#
# -SSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSS#
# --SSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSS#
# --SSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSS#
# --SSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSS#
# --SSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSS#
# --SSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSSS#
##################################################################################################################################
Time for model checking: 0.208s.
@@ -0,0 +1,26 @@
Storm-pars 1.5.2 (dev)
Date: Tue Aug 31 11:54:33 2021
Command line arguments: --prism /tmp/prism-parametric.pm --prop 'P=? [F VAR_13 > 0]'
Current working directory: /home/biodivine
Time for model input parsing: 0.054s.
Time for model construction: 0.060s.
--------------------------------------------------------------
Model type: DTMC (sparse)
States: 31
Transitions: 60
Reward Models: none
State Labels: 3 labels
* deadlock -> 0 item(s)
* init -> 1 item(s)
* (VAR_13 > 0) -> 3 item(s)
Choice Labels: none
--------------------------------------------------------------
Model checking property "1": P=? [F (VAR_13 > 0)] ...
Result (initial states): ((param_sig) * (2981688543185870087663495150126244302243211334125913130541472787739802879829617808110453272217978374073720397249812500000000000000000000000000000000*param_block^2*param_sig^4+21333081000995441881478481888623294608561432837600286741218656884283620692512542203861605829532226092102934969442322694750000000000000000000000000000*param_block^2+39132416603004844706196842373313272958271263050686725335537624140954554083030939648762564370066208263332252673796791507500000000000000000000000000000*param_block^3+22725999490705377615041471133908386334886227218171410438914202044860955570751027688763780193895740093693277310924369400000000000000000000000000000000*param_block^4+4245231150311364342612854790676605418253049153545896232307346492306252682008919270223849752504307504320664247517188723800000000000000000000000000000*param_block+3208978818800247399506763118470536036989385423591596173967281127328788493228035015636535956506569555711016320577817679061497326203211080000000000000*param_sig+61337241783765857891013320525639798082527501818023156733982938906674645568072155420853118954216213548904852362777061738609148204736454500000000000000*param_block^2*param_sig+74369918766404647592913928656863192667117420889433781173107741721170856650611346506277604830614523491564585562186305128156035141329240000000000000000*param_block^3*param_sig+29292019838238331850968165043795743170409577972626036193644124317339136456350216875337061516525802454304327791722750500000000000000000000000000000000*param_block^4*param_sig+19902622481499489037239723031085884009390738986142582753983084280681700808413379128470957648933080862881426158617714463694327731092463850000000000000*param_block*param_sig+4988231807874665106368003757977042997192179259217166529296729711205229419890270158470421379470061661981037187602312836044526074892761100000000000000*param_sig^2+59601551364347403569696046187070921651122929428946390382552332230109692835887798717812528775399049540520370596585742609690208728119308750000000000000*param_block^2*param_sig^2+46192170164668265056819074737333877291295544847929182558994672251565820597224197376450246544898952754998090489639395163646243621415550000000000000000*param_block^3*param_sig^2+9377194403932374268124660332452806355725761378949846467347269487253715794857888095086660972929117334709214264218094973175220501423772464357643884000*param_block^3*param_sig^3+8921144215261864428692689196891058971406744515998644847029720979796682460863133143839669201013739000242824402488269161846556804540000000000000000000*param_block^4*param_sig^2+23082287092982285261521833710527899304094126172081965804252830610430812603140429782139624302429880262001526161428768219750503507187973495927296538450*param_block^2*param_sig^3+3033543996110841631945273977359607825154524619770251161191749427292223175220501433419497881797347290488662407111607750000000000000000000000000000000*param_block*param_sig^4+15647645284008923066441148084578465388470746425309070323293366934293856928604775268701474119262030255126624306747492267357542190429822247353486849285*param_block*param_sig^3+28020885305453682349511300346585293159400120608409114630098547684193006645719467786525298339687114470730745853782276038939665742329926375000000000000*param_block*param_sig^2+606060606060606086243026136074268382137648447809459208926545824967618746672222608708252887932032337859781929300646200000000000000000000000000000000*param_sig^4+2976310726310726390537465491247021999587550355313910009812905878666014279171723787491799172194130205204794727808478779511424404472526262240433363428*param_sig^3+549594155844155832063941940412527773883976317799876825897631779983932196027501909876829090909090908960000000000000000000000000000000000000000000000))/(450000000000000000000000000000000000000000000000000000000000000000 * ((5*param_block+4) * (10*param_block+1) * (250000000000000000*param_block+66666666666666663) * (7*param_sig+9) * (2272727272727273*param_sig+5000000000000000*param_block) * (2857142857142857*param_sig+750000000000000) * (3333333333333333*param_sig+4357142857142857) * (33333333333333335*param_sig+68518518518518518)))
Time for model checking: 0.061s.
@@ -0,0 +1,34 @@
#! rules
// signal changes
sig{i}::ext => sig{a}::ext @ k_sig_1
sig{a}::ext => sig{a}::cell @ (k_sig_2*[sig{a}::ext])/(1 + [block{a}::cell])
block{i}::ext => block{a}::ext @ k_block_1
block{a}::ext => block{a}::cell @ (k_block_2*[block{a}::ext])/(1 + [sig{a}::cell])
sig{a}::cell + P1()::cell => sig{a}.P1()::cell @ param_sig*[sig{a}::cell]*[P1()::cell]
sig{_}.P1()::cell => sig{_}::cell + P1()::cell @ k_deg*[sig{_}.P1()::cell]
sig{a}.P1(active{off})::cell => sig{a}.P1(active{on})::cell @ 0.5*[sig{a}.P1(active{off})::cell]
sig{a}.P1()::cell => sig{a}::cell + P1()::cell @ k_deg*[sig{a}.P1()::cell]
block{a}::cell + P1()::cell => block{a}.P1()::cell @ param_block*[block{a}::cell]*[P1()::cell]
P1(active{on})::cell + P2()::cell => P1(active{on}).P2()::cell @ 0.4*[P1(active{on})::cell]*[P2()::cell]
P1().P2()::cell => P1()::cell + P2()::cell @ k_deg*[P1().P2()::cell]
P1().P2(active{off})::cell => P1().P2(active{on})::cell @ k_prod*[P1().P2(active{off})::cell]
#! inits
sig{i}::ext
block{i}::ext
P1(active{off})::cell
P2(active{off})::cell
#! definitions
k_sig_1 = 0.8
k_sig_2 = 0.2
k_block_1 = 0.9
k_block_2 = 0.3
k_deg = 0.3
k_prod = 0.6
param_sig = 0.3
param_block = 0.4
@@ -0,0 +1,155 @@
{
"edges": [
{
"p": 0.22222222222222227,
"t": 9,
"s": 2
},
{
"p": 0.5,
"t": 8,
"s": 4
},
{
"p": 0.25,
"t": 7,
"s": 1
},
{
"p": 0.37499999999999994,
"t": 2,
"s": 1
},
{
"p": 0.5,
"t": 9,
"s": 4
},
{
"p": 1.0,
"t": 5,
"s": 10
},
{
"p": 0.6666666666666667,
"t": 9,
"s": 7
},
{
"p": 0.44444444444444453,
"t": 1,
"s": 2
},
{
"p": 1,
"t": 6,
"s": 6
},
{
"p": 0.37499999999999994,
"t": 3,
"s": 1
},
{
"p": 0.4444444444444445,
"t": 12,
"s": 11
},
{
"p": 0.1764705882352941,
"t": 5,
"s": 9
},
{
"p": 0.36363636363636365,
"t": 10,
"s": 5
},
{
"p": 0.3529411764705882,
"t": 4,
"s": 9
},
{
"p": 0.11111111111111112,
"t": 5,
"s": 11
},
{
"p": 0.25,
"t": 10,
"s": 3
},
{
"p": 0.4444444444444445,
"t": 3,
"s": 11
},
{
"p": 0.47058823529411764,
"t": 7,
"s": 9
},
{
"p": 0.7499999999999999,
"t": 11,
"s": 3
},
{
"p": 0.33333333333333337,
"t": 10,
"s": 7
},
{
"p": 0.36363636363636365,
"t": 6,
"s": 5
},
{
"p": 1.0,
"t": 5,
"s": 8
},
{
"p": 1.0,
"t": 6,
"s": 12
},
{
"p": 0.2727272727272727,
"t": 8,
"s": 5
},
{
"p": 0.33333333333333337,
"t": 11,
"s": 2
}
],
"ordering": [
"P1().P2()::cell",
"P1()::cell",
"P2()::cell",
"block{_}.P1()::cell",
"block{_}::cell",
"block{_}::ext",
"sig{_}.P1()::cell",
"sig{_}::cell",
"sig{_}::ext"
],
"initial": 2,
"nodes": {
"1": "(1, 0, 0, 0, 0, 1, 0, 0, 1)",
"2": "(0, 1, 1, 0, 0, 1, 0, 0, 1)",
"3": "(1, 0, 0, 0, 1, 0, 0, 0, 1)",
"4": "(0, 0, 1, 0, 0, 1, 1, 0, 0)",
"5": "(0, 1, 1, 0, 1, 0, 0, 1, 0)",
"6": "(0, 0, 1, 1, 0, 0, 0, 1, 0)",
"7": "(1, 0, 0, 0, 0, 1, 0, 1, 0)",
"8": "(0, 0, 1, 0, 1, 0, 1, 0, 0)",
"9": "(0, 1, 1, 0, 0, 1, 0, 1, 0)",
"10": "(1, 0, 0, 0, 1, 0, 0, 1, 0)",
"11": "(0, 1, 1, 0, 1, 0, 0, 0, 1)",
"12": "(0, 0, 1, 1, 0, 0, 0, 0, 1)"
}
}
@@ -0,0 +1,2 @@
Result: True
Number of satisfying states: 31
+9
View File
@@ -1093,6 +1093,7 @@ class Yaml(Text):
return False
@build_sniff_from_prefix
class BCSLmodel(Text):
"""BioChemical Space Language model file"""
@@ -1107,6 +1108,7 @@ class BCSLmodel(Text):
return any(keyword in content for keyword in keywords)
@build_sniff_from_prefix
class BCSLts(Json):
"""BioChemical Space Language transition system file"""
@@ -1143,6 +1145,7 @@ class BCSLts(Json):
return False
@build_sniff_from_prefix
class StormRegions(Text):
"""
Storm PCTL parameter synthesis result file
@@ -1168,6 +1171,7 @@ class StormRegions(Text):
dataset.blurb = "file purged from disk"
@build_sniff_from_prefix
class StormSample(Text):
"""
Storm PCTL parameter synthesis result file
@@ -1193,6 +1197,7 @@ class StormSample(Text):
dataset.blurb = "file purged from disk"
@build_sniff_from_prefix
class StormCheck(Text):
"""
Storm PCTL model checking result file
@@ -1223,6 +1228,7 @@ class StormCheck(Text):
dataset.blurb = "file purged from disk"
@build_sniff_from_prefix
class CTLresult(Text):
"""CTL model checking result"""
@@ -1250,6 +1256,7 @@ class CTLresult(Text):
dataset.blurb = "file purged from disk"
@build_sniff_from_prefix
class PithyaProperty(Text):
"""Pithya CTL property format"""
@@ -1265,6 +1272,7 @@ class PithyaProperty(Text):
return False
@build_sniff_from_prefix
class PithyaModel(Text):
"""Pithya model format"""
@@ -1281,6 +1289,7 @@ class PithyaModel(Text):
return False
@build_sniff_from_prefix
class PithyaResult(Json):
"""Pithya result format"""
+36
View File
@@ -0,0 +1,36 @@
import pytest
from galaxy.datatypes.text import (
BCSLmodel,
BCSLts,
CTLresult
)
from .util import (
get_input_files,
MockDataset,
MockDatasetDataset
)
@pytest.mark.parametrize('bcsl_loader, input_file', [
[BCSLmodel, "test_file3.bcsl.model"],
[BCSLts, "test_file3.bcsl.ts"],
[CTLresult, "test_file3.ctl.result"]
])
def test_bcsl_sniff(bcsl_loader, input_file):
loader = bcsl_loader()
with get_input_files(input_file) as input_files:
assert loader.sniff(input_files[0]) is True
@pytest.mark.parametrize('bcsl_loader, input_file, expected_peek', [
[BCSLts, "test_file3.bcsl.ts", "States: 12\nTransitions: 25\nUnique agents: 9\nInitial state: 2"],
[CTLresult, "test_file3.ctl.result", """Model checking result: True"""]
])
def test_bcsl_set_peek(bcsl_loader, input_file, expected_peek):
loader = bcsl_loader()
with get_input_files(input_file) as input_files:
dataset = MockDataset(1)
dataset.file_name = input_files[0]
dataset.dataset = MockDatasetDataset(dataset.file_name)
loader.set_peek(dataset)
assert dataset.peek == expected_peek
+20
View File
@@ -0,0 +1,20 @@
import pytest
from galaxy.datatypes.text import (
PithyaModel,
PithyaProperty,
PithyaResult
)
from .util import (
get_input_files
)
@pytest.mark.parametrize('pithya_loader, input_file', [
[PithyaModel, "test_file1.pithya.model"],
[PithyaProperty, "test_file1.pithya.property"],
[PithyaResult, "test_file1.pithya.result"]
])
def test_pithya_sniff(pithya_loader, input_file):
loader = pithya_loader()
with get_input_files(input_file) as input_files:
assert loader.sniff(input_files[0]) is True
+37
View File
@@ -0,0 +1,37 @@
import pytest
from galaxy.datatypes.text import (
StormRegions,
StormSample,
StormCheck
)
from .util import (
get_input_files,
MockDataset,
MockDatasetDataset
)
@pytest.mark.parametrize('storm_loader, input_file', [
[StormRegions, "test_file2.storm.regions"],
[StormSample, "test_file2.storm.sample"],
[StormCheck, "test_file2.storm.check"]
])
def test_storm_sniff(storm_loader, input_file):
loader = storm_loader()
with get_input_files(input_file) as input_files:
assert loader.sniff(input_files[0]) is True
@pytest.mark.parametrize('storm_loader, input_file, expected_peek', [
[StormRegions, "test_file2.storm.regions", """Storm-pars region results."""],
[StormSample, "test_file2.storm.sample", """Storm-pars sample results."""],
[StormCheck, "test_file2.storm.check", """Model checking result: true"""]
])
def test_storm_set_peek(storm_loader, input_file, expected_peek):
loader = storm_loader()
with get_input_files(input_file) as input_files:
dataset = MockDataset(1)
dataset.file_name = input_files[0]
dataset.dataset = MockDatasetDataset(dataset.file_name)
loader.set_peek(dataset)
assert dataset.peek == expected_peek
+6
View File
@@ -8,6 +8,12 @@ from galaxy.datatypes.sniff import get_test_fname
from galaxy.util.hash_util import md5_hash_file
class MockDatasetDataset:
def __init__(self, file_name):
self.file_name = file_name
self.purged = False
class MockMetadata:
file_name: Optional[str] = None