-
Notifications
You must be signed in to change notification settings - Fork 0
/
ragtimer_output.txt
143 lines (126 loc) · 4.45 KB
/
ragtimer_output.txt
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
admin.sh
artifact.sh
bin
classes
depgraph.py
genbash.py
ignore.txt
main.py
Makefile
prefixes.py
prefix_parser.py
__pycache__
reaction_list.txt
reactions_mod.py
reactions_v5.py
run_lots.sh
src
testprint.txt
test.sh
test_subp.py
test_v2
test_v2.cpp
test_v2.dsc
test_v2.h
test_v2.ivy
test_v2.txt
test_v3
test_v3.cpp
test_v3.dsc
test_v3.h
test_v3.ivy
trace_list.txt
two.sh
================================================================================
Welcome to RAGTIMER for trace generation.
This is a work in progress. Please submit bug reports.
================================================================================
Constructing a dependency graph
Finished constructing a dependency graph, found these prefixes:
R5
R3 R5
R8 R5
/home/landonjefftaylor/combined_ragtimer/_ragtimer
Finding 100
For each prefix: 50
--------------------------------------------------
Testing Prefix R3 R5
--------------------------------------------------
starting to run initial test
finished initial test
The iters recorded for this initial example is 456
Running test for 50 simulation runs in group 1 of 1
finished randomized testing
Run 49 did not reach the target state
The traces recorded and the information on those traces are stored in 'reaction_list.txt'
The traces by themselves (i.e. for simulation and commuting) are found in 'trace_list.txt'
--------------------------------------------------
Testing Prefix R8 R5
--------------------------------------------------
starting to run initial test
finished initial test
The iters recorded for this initial example is 693
Running test for 50 simulation runs in group 1 of 1
finished randomized testing
The traces recorded and the information on those traces are stored in 'reaction_list.txt'
The traces by themselves (i.e. for simulation and commuting) are found in 'trace_list.txt'
================================================================================
Total Sum of Unique Path Probabilities: 0.0
================================================================================
(javac -classpath "/usr/local/bin/prism/classes:/usr/local/bin/prism/lib/*:/usr/local/bin/prism/prism/classes:/usr/local/bin/prism/prism/lib/*" -d classes src/./BuildModel.java)
PRISM_DIR=/usr/local/bin/prism PRISM_MAINCLASS=simulate.BuildModel bin/run
Welcome to the model commutation tool.
Getting Parameters from input file
Model Name: ../model.sm
Trace List Name: ../commute_traces.txt
Property: G_bg>=50
Max Depth: 20
Time Bound: 100000.0
Terminating with depth bound
Cycle length: 4
Cycle initial values for testing: 8
Verbose mode disabled
Prism model and property loaded succesfully.
Iterating through each input trace.
Expect this to run silently for a moment.
Processed 25 paths with a state count of 14591
Processed 50 paths with a state count of 16641
Processed 75 paths with a state count of 18519
Processed 100 paths with a state count of 19438
Processed 100 paths with a state count of 19517
State graph built. Appending cycles where allowable.
Added 19517 cycles, with 4425 new states and 19130 transitions.
Removed 0 dead-end states and 0 probability sink states (total 0 states).
Removed 0 corresponding transitions.
Final Count:
23942 states
84585 transitions
Establishing an absorbing state.
Begin printing model files.
Now printing 100 paths to PRISM model files.
Now printing 100 paths to STORM model files.
---------------------------------------
BEGIN ERROR CHECKING
If an inconsistency is found in the state space, its details will be provided here.
Otherwise, assume the generated state-space is error-free.
This is an added confidence booster for the probability results.
END ERROR CHECKING
---------------------------------------
Finished! Processed 100 paths.
Max Memory: 926229400 bytes
Max Memory: 926229 KB
Max Memory: 926 MB
Max Memory: 0 GB
Welcome to RAGTIMER. At present, this is two tools joined together. We are working on joining them together more seamlessly but appreciate your patience with this prototype tool.
I will generate traces, then commute.
I am assuming you have placed your model in the following files:
model.ragtimer (in the RAGTIMER format; see README)
model.prop (file with property without time constraints in first line, i.e., x=10 )
model.sm (prism model file)
model.csl (prism csl property)
_commute/options.txt
Running RAGTIMER trace generation
/home/landonjefftaylor/combined_ragtimer/_ragtimer
Starting Commuting
Look for output files _commute/prism.* or _commute/storm.*
You can use these files in your favorite model checker.