Commit 2dfd6027 authored by Hans Vrapi's avatar Hans Vrapi
Browse files

change evidence in survey bif

parent 957e6f55
......@@ -47,8 +47,8 @@ probability ( T | O, R ) {
(self, big) 0.70, 0.21, 0.09;
}
evidence first {
R=0;
E=0;
}
hypothesis second {
T=0;
}
\ No newline at end of file
}
......@@ -400,12 +400,12 @@
]
},
{
"location": "loc3",
"location": "loc0",
"probability": {"exp": 0.25},
"assignments": [
{
"ref": "E",
"value": 1
"value": -1
},
{
"ref": "A",
......@@ -456,12 +456,12 @@
]
},
{
"location": "loc3",
"location": "loc0",
"probability": {"exp": 0.28},
"assignments": [
{
"ref": "E",
"value": 1
"value": -1
},
{
"ref": "A",
......@@ -512,12 +512,12 @@
]
},
{
"location": "loc3",
"location": "loc0",
"probability": {"exp": 0.12},
"assignments": [
{
"ref": "E",
"value": 1
"value": -1
},
{
"ref": "A",
......@@ -568,12 +568,12 @@
]
},
{
"location": "loc3",
"location": "loc0",
"probability": {"exp": 0.36},
"assignments": [
{
"ref": "E",
"value": 1
"value": -1
},
{
"ref": "A",
......@@ -624,12 +624,12 @@
]
},
{
"location": "loc3",
"location": "loc0",
"probability": {"exp": 0.3},
"assignments": [
{
"ref": "E",
"value": 1
"value": -1
},
{
"ref": "A",
......@@ -680,12 +680,12 @@
]
},
{
"location": "loc3",
"location": "loc0",
"probability": {"exp": 0.1},
"assignments": [
{
"ref": "E",
"value": 1
"value": -1
},
{
"ref": "A",
......@@ -788,20 +788,16 @@
]
},
{
"location": "loc0",
"location": "loc5",
"probability": {"exp": 0.75},
"assignments": [
{
"ref": "R",
"value": -1
"value": 1
},
{
"ref": "E",
"value": -1
},
{
"ref": "O",
"value": -1
}
]
}
......@@ -832,20 +828,16 @@
]
},
{
"location": "loc0",
"location": "loc5",
"probability": {"exp": 0.8},
"assignments": [
{
"ref": "R",
"value": -1
"value": 1
},
{
"ref": "E",
"value": -1
},
{
"ref": "O",
"value": -1
}
]
}
......
Storm 1.6.4
Date: Mon Jun 6 19:19:18 2022
Command line arguments: --jani jani_files/no_evidence/survey.jani --prop 'P=? [F(R=1)]'
Date: Tue Jun 7 08:41:54 2022
Command line arguments: --jani jani_files/no_evidence/survey.jani --prop 'P=? [F(E=1)]'
Current working directory: /home/hans/Desktop/Storm-bn/storm_evidence
Time for model input parsing: 0.001s.
......@@ -9,11 +9,20 @@ Time for model input parsing: 0.001s.
WARN (FormulaParserGrammar.cpp:328): Identifier `R' coincides with a reserved keyword or operator. Property expressions using the variable or constant 'R' will not be parsed correctly.
WARN (FormulaParserGrammar.cpp:328): Identifier `S' coincides with a reserved keyword or operator. Property expressions using the variable or constant 'S' will not be parsed correctly.
WARN (FormulaParserGrammar.cpp:331): Identifier `T' coincides with a reserved keyword or operator. Property expressions using the variable or constant 'T' might not be parsed correctly.
ERROR (SpiritErrorHandler.h:27): Parsing error at 1:3: expecting "?", here:
R=1)]
^
Time for model construction: 0.016s.
ERROR (storm.cpp:21): An exception caused Storm to terminate. The message of the exception is: WrongFormatException: Parsing error at 1:3: expecting "?", here:
R=1)]
^
--------------------------------------------------------------
Model type: DTMC (sparse)
States: 20
Transitions: 42
Reward Models: none
State Labels: 3 labels
* deadlock -> 3 item(s)
* init -> 1 item(s)
* (E = 1) -> 1 item(s)
Choice Labels: none
--------------------------------------------------------------
Model checking property "1": P=? [F (E = 1)] ...
Result (for initial states): 0.2546
Time for model checking: 0.000s.
Storm 1.6.4
Date: Mon Jun 6 19:19:18 2022
Command line arguments: --jani jani_files/no_evidence/survey.jani --prop 'P=? [F(R=1|T=1|T=2)]'
Date: Tue Jun 7 08:41:22 2022
Command line arguments: --jani jani_files/no_evidence/survey.jani --prop 'P=? [F(E=1|T=1|T=2)]'
Current working directory: /home/hans/Desktop/Storm-bn/storm_evidence
Time for model input parsing: 0.003s.
Time for model input parsing: 0.001s.
WARN (FormulaParserGrammar.cpp:328): Identifier `R' coincides with a reserved keyword or operator. Property expressions using the variable or constant 'R' will not be parsed correctly.
WARN (FormulaParserGrammar.cpp:328): Identifier `S' coincides with a reserved keyword or operator. Property expressions using the variable or constant 'S' will not be parsed correctly.
WARN (FormulaParserGrammar.cpp:331): Identifier `T' coincides with a reserved keyword or operator. Property expressions using the variable or constant 'T' might not be parsed correctly.
ERROR (SpiritErrorHandler.h:27): Parsing error at 1:3: expecting "?", here:
R=1|T=1|T=2)]
^
Time for model construction: 0.015s.
ERROR (storm.cpp:21): An exception caused Storm to terminate. The message of the exception is: WrongFormatException: Parsing error at 1:3: expecting "?", here:
R=1|T=1|T=2)]
^
--------------------------------------------------------------
Model type: DTMC (sparse)
States: 20
Transitions: 42
Reward Models: none
State Labels: 3 labels
* deadlock -> 1 item(s)
* init -> 1 item(s)
* (((E = 1) | (T = 1)) | (T = 2)) -> 3 item(s)
Choice Labels: none
--------------------------------------------------------------
Model checking property "1": P=? [F (((E = 1) | (T = 1)) | (T = 2))] ...
Result (for initial states): 0.58302324
Time for model checking: 0.000s.
Storm 1.6.4
Date: Mon Jun 6 19:19:18 2022
Date: Tue Jun 7 08:38:31 2022
Command line arguments: --jani jani_files/1/survey.jani --prop 'P=? [G(T=0 | T=-1)]'
Current working directory: /home/hans/Desktop/Storm-bn/storm_evidence
......@@ -13,16 +13,16 @@ Time for model construction: 0.013s.
--------------------------------------------------------------
Model type: DTMC (sparse)
States: 20
States: 19
Transitions: 41
Reward Models: none
State Labels: 3 labels
* deadlock -> 3 item(s)
* init -> 1 item(s)
* ((T = 0) | (T = -(1))) -> 18 item(s)
* ((T = 0) | (T = -(1))) -> 17 item(s)
Choice Labels: none
--------------------------------------------------------------
Model checking property "1": P=? [G ((T = 0) | (T = -(1)))] ...
Result (for initial states): 0.4838867451
Result (for initial states): 0.5594
Time for model checking: 0.000s.
Storm 1.6.4
Date: Mon Jun 6 20:57:12 2022
Date: Tue Jun 7 08:33:57 2022
Command line arguments: --jani jani_files/no_evidence/survey.jani --prop 'P=? [F(E=1)]'
Current working directory: /home/hans/Desktop/Storm-bn/storm_evidence
......
Storm 1.6.4
Date: Mon Jun 6 20:57:12 2022
Date: Tue Jun 7 08:33:57 2022
Command line arguments: --jani jani_files/no_evidence/survey.jani --prop 'P=? [F(E=1|O=1)]'
Current working directory: /home/hans/Desktop/Storm-bn/storm_evidence
......
Storm 1.6.4
Date: Mon Jun 6 20:57:12 2022
Date: Tue Jun 7 08:33:57 2022
Command line arguments: --jani jani_files/5/survey.jani --prop 'P=? [G(O=0 | O=-1)]'
Current working directory: /home/hans/Desktop/Storm-bn/storm_evidence
Time for model input parsing: 0.000s.
Time for model input parsing: 0.019s.
WARN (FormulaParserGrammar.cpp:328): Identifier `S' coincides with a reserved keyword or operator. Property expressions using the variable or constant 'S' will not be parsed correctly.
Time for model construction: 0.012s.
Time for model construction: 0.105s.
--------------------------------------------------------------
Model type: DTMC (sparse)
......@@ -23,4 +23,4 @@ Choice Labels: none
Model checking property "1": P=? [G ((O = 0) | (O = -(1)))] ...
Result (for initial states): 0.96
Time for model checking: 0.000s.
Time for model checking: 0.004s.
storm --jani jani_files/no_evidence/survey.jani --prop "P=? [F(R=1)]"
\ No newline at end of file
storm --jani jani_files/no_evidence/survey.jani --prop "P=? [F(E=1)]"
storm --jani jani_files/no_evidence/survey.jani --prop "P=? [F(R=1|T=1|T=2)]"
\ No newline at end of file
storm --jani jani_files/no_evidence/survey.jani --prop "P=? [F(E=1|T=1|T=2)]"
......@@ -4,7 +4,7 @@ import pandas as pd
networks = ['asia','alarm', 'cancer', 'child', 'earthquake', 'insurance', 'sachs', 'survey', 'andes', 'hepar2']
ev_nodes_percentage = [5]
ev_nodes_percentage = [1,5,10,30]
def run_experiments():
for network in networks:
......
Supports Markdown
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment