Browse Source
Merge from future
Merge from future
Former-commit-id:main466833b425[formerly8d2ddbd670] Former-commit-id:39a0249482
Mavo
9 years ago
826 changed files with 163092 additions and 120527 deletions
-
5.gitignore
-
5CMakeLists.txt
-
1examples/dtmc/die/die.pm
-
41034examples/gspn/HypercubeGrid/hc3k4p4b12.pnml
-
87274examples/gspn/HypercubeGrid/hc4k3p3b12.pnml
-
1examples/gspn/HypercubeGrid/hc5k3p3b15.pnml.REMOVED.git-id
-
5554examples/gspn/ibm319/IBM319.pnml
-
14examples/gspn/pnpro_test1/project01.PNPRO
-
148examples/gspn/tiny/tiny01.pnml
-
1236examples/gspn/workflow_cluster/workflow_cluster.pnml
-
2604examples/jani-examples/beb.jani
-
27examples/jani-examples/beb.jani.txt
-
64examples/jani-examples/beb.modest
-
27examples/jani-examples/beb.modest.txt
-
2092examples/jani-examples/brp.jani
-
63examples/jani-examples/brp.jani.txt
-
213examples/jani-examples/brp.modest
-
63examples/jani-examples/brp.modest.txt
-
2129examples/jani-examples/consensus-6.jani
-
27examples/jani-examples/consensus-6.jani.txt
-
157examples/jani-examples/consensus-6.modest
-
27examples/jani-examples/consensus-6.modest.txt
-
354examples/jani-examples/dice.jani
-
29examples/jani-examples/dice.jani.txt
-
87examples/pctmc/polling6.sm
-
3examples/pdtmc/brp/brp.pm
-
2examples/pdtmc/brp/brp16_2.pm
-
2examples/pdtmc/brp_rewards2/brp_rewards16_2.pm
-
3examples/pdtmc/brp_rewards2/brp_rewards2.pm
-
2examples/pdtmc/brp_rewards4/brp_rewards16_2.pm
-
3examples/pdtmc/brp_rewards4/brp_rewards4.pm
-
35examples/pdtmc/die.pm
-
44examples/pdtmc/twodie.pm
-
58examples/pgcl/coupon/coupon10-classic.pgcl
-
60examples/pgcl/coupon/coupon10-cost.pgcl
-
62examples/pgcl/coupon/coupon10-observe.pgcl
-
60examples/pgcl/coupon/coupon10.pgcl
-
24examples/pgcl/coupon/coupon3-classic.pgcl
-
28examples/pgcl/coupon/coupon3-cost.pgcl
-
30examples/pgcl/coupon/coupon3-observe.pgcl
-
28examples/pgcl/coupon/coupon3.pgcl
-
34examples/pgcl/coupon/coupon4-observe.pgcl
-
32examples/pgcl/coupon/coupon5-classic.pgcl
-
36examples/pgcl/coupon/coupon5-cost.pgcl
-
38examples/pgcl/coupon/coupon5-observe.pgcl
-
36examples/pgcl/coupon/coupon5.pgcl
-
40examples/pgcl/coupon/coupon7-classic.pgcl
-
44examples/pgcl/coupon/coupon7-cost.pgcl
-
46examples/pgcl/coupon/coupon7-observe.pgcl
-
44examples/pgcl/coupon/coupon7.pgcl
-
35examples/pgcl/crowds/crowds100-100-observeOther.pgcl
-
34examples/pgcl/crowds/crowds100-100.pgcl
-
35examples/pgcl/crowds/crowds100-60-observeOther.pgcl
-
34examples/pgcl/crowds/crowds100-60-param.pgcl
-
34examples/pgcl/crowds/crowds100-60.pgcl
-
36examples/pgcl/crowds/crowds100-80-observeOther.pgcl
-
34examples/pgcl/crowds/crowds100-80.pgcl
-
34examples/pgcl/crowds/crowds3-3-param.pgcl
-
34examples/pgcl/crowds/crowds3-3.pgcl
-
33examples/pgcl/crowds/crowds3-5-param.pgcl
-
34examples/pgcl/crowds/crowds3-5.pgcl
-
34examples/pgcl/crowds/crowds5-20-param.pgcl
-
34examples/pgcl/crowds/crowds5-20.pgcl
-
108examples/pgcl/herman/herman10-det.pgcl
-
108examples/pgcl/herman/herman10.pgcl
-
138examples/pgcl/herman/herman13-det.pgcl
-
138examples/pgcl/herman/herman13.pgcl
-
178examples/pgcl/herman/herman17-det.pgcl
-
178examples/pgcl/herman/herman17.pgcl
-
218examples/pgcl/herman/herman21-det.pgcl
-
218examples/pgcl/herman/herman21.pgcl
-
77examples/pgcl/herman/herman7-det.pgcl
-
77examples/pgcl/herman/herman7.pgcl
-
49examples/pgcl/lotkavolterra.pgcl
-
26examples/pgcl/robot.pgcl
-
2examples/pmdp/brp/brp.pm
-
5examples/pmdp/coin2/coin2.pm
-
3examples/pmdp/coin4/coin4.pm
-
11examples/pmdp/zeroconf/zeroconf.pm
-
6resources/3rdparty/CMakeLists.txt
-
9resources/3rdparty/include_xerces.cmake
-
4resources/3rdparty/modernjson/CMakeLists.txt
-
59resources/3rdparty/modernjson/ChangeLog.md
-
35resources/3rdparty/modernjson/Makefile
-
178resources/3rdparty/modernjson/README.md
-
3resources/3rdparty/modernjson/appveyor.yml
-
77resources/3rdparty/modernjson/benchmarks/benchmarks.cpp
-
401resources/3rdparty/modernjson/benchmarks/benchpress.hpp
-
1312resources/3rdparty/modernjson/benchmarks/cxxopts.hpp
-
1resources/3rdparty/modernjson/benchmarks/files/jeopardy/jeopardy.json.REMOVED.git-id
-
9resources/3rdparty/modernjson/benchmarks/files/nativejson-benchmark/canada.json
-
50469resources/3rdparty/modernjson/benchmarks/files/nativejson-benchmark/citm_catalog.json
-
15482resources/3rdparty/modernjson/benchmarks/files/nativejson-benchmark/twitter.json
-
317resources/3rdparty/modernjson/doc/Doxyfile
-
82resources/3rdparty/modernjson/doc/Makefile
-
26resources/3rdparty/modernjson/doc/css/mylayout.css
-
27resources/3rdparty/modernjson/doc/css/mylayout_docset.css
-
36resources/3rdparty/modernjson/doc/examples/README.cpp
-
1resources/3rdparty/modernjson/doc/examples/README.link
-
27resources/3rdparty/modernjson/doc/examples/README.output
41034
examples/gspn/HypercubeGrid/hc3k4p4b12.pnml
File diff suppressed because it is too large
View File
File diff suppressed because it is too large
View File
87274
examples/gspn/HypercubeGrid/hc4k3p3b12.pnml
File diff suppressed because it is too large
View File
File diff suppressed because it is too large
View File
@ -0,0 +1 @@ |
|||
1dcc3a0045e4d0f9358f9ee04e70c6f0107929be |
|||
5554
examples/gspn/ibm319/IBM319.pnml
File diff suppressed because it is too large
View File
File diff suppressed because it is too large
View File
@ -0,0 +1,14 @@ |
|||
<?xml version="1.0" encoding="UTF-8" standalone="no"?> |
|||
<!-- This project file has been saved by the New GreatSPN Editor, v.100 --><project name="project01" version="121"> |
|||
<gspn name="gspn_1_1" show-color-cmd="false" show-fluid-cmd="false"> |
|||
<nodes> |
|||
<place marking="1" name="P0" x="3.0" y="2.0"/> |
|||
<transition name="T0" nservers-x="0.5" type="EXP" x="9.55" y="2.0"/> |
|||
<place name="P1" x="14.0" y="2.0"/> |
|||
</nodes> |
|||
<edges> |
|||
<arc head="T0" kind="INPUT" tail="P0"/> |
|||
<arc head="P1" kind="OUTPUT" tail="T0"/> |
|||
</edges> |
|||
</gspn> |
|||
</project> |
|||
@ -0,0 +1,148 @@ |
|||
<pnml> |
|||
<net id="tiny1"> |
|||
<place id="p1"> |
|||
<initialMarking> |
|||
<value>Default,1</value> |
|||
</initialMarking> |
|||
</place> |
|||
<place id="p2"> |
|||
<initialMarking> |
|||
<value>Default,1</value> |
|||
</initialMarking> |
|||
</place> |
|||
<place id="p3"> |
|||
<initialMarking> |
|||
<value>Default,0</value> |
|||
</initialMarking> |
|||
</place> |
|||
<place id="p4"> |
|||
<initialMarking> |
|||
<value>Default,0</value> |
|||
</initialMarking> |
|||
</place> |
|||
<place id="p5"> |
|||
<initialMarking> |
|||
<value>Default,0</value> |
|||
</initialMarking> |
|||
</place> |
|||
<place id="p6"> |
|||
<initialMarking> |
|||
<value>Default,0</value> |
|||
</initialMarking> |
|||
</place> |
|||
<place id="p7"> |
|||
<initialMarking> |
|||
<value>Default,0</value> |
|||
</initialMarking> |
|||
</place> |
|||
<transition id="t1"> |
|||
<rate> |
|||
<value>1</value> |
|||
</rate> |
|||
<timed> |
|||
<value>false</value> |
|||
</timed> |
|||
</transition> |
|||
<transition id="t2"> |
|||
<rate> |
|||
<value>2</value> |
|||
</rate> |
|||
<timed> |
|||
<value>false</value> |
|||
</timed> |
|||
</transition> |
|||
<transition id="t3"> |
|||
<rate> |
|||
<value>3</value> |
|||
</rate> |
|||
<timed> |
|||
<value>false</value> |
|||
</timed> |
|||
</transition> |
|||
<transition id="l1"> |
|||
<rate> |
|||
<value>4</value> |
|||
</rate> |
|||
<timed> |
|||
<value>true</value> |
|||
</timed> |
|||
</transition> |
|||
<transition id="l2"> |
|||
<rate> |
|||
<value>5</value> |
|||
</rate> |
|||
<timed> |
|||
<value>true</value> |
|||
</timed> |
|||
<priority> |
|||
<text>2</text> |
|||
</priority> |
|||
</transition> |
|||
<arc id="arc1" source="p1" target="t1"> |
|||
<inscription> |
|||
<value>Default,1</value> |
|||
</inscription> |
|||
<type value="normal" /> |
|||
</arc> |
|||
<arc id="arc2" source="t1" target="p3"> |
|||
<inscription> |
|||
<value>Default,1</value> |
|||
</inscription> |
|||
<type value="normal" /> |
|||
</arc> |
|||
<arc id="arc3" source="p2" target="t2"> |
|||
<inscription> |
|||
<value>Default,1</value> |
|||
</inscription> |
|||
<type value="normal" /> |
|||
</arc> |
|||
<arc id="arc4" source="t2" target="p5"> |
|||
<inscription> |
|||
<value>Default,1</value> |
|||
</inscription> |
|||
<type value="normal" /> |
|||
</arc> |
|||
<arc id="arc5" source="p2" target="t3"> |
|||
<inscription> |
|||
<value>Default,1</value> |
|||
</inscription> |
|||
<type value="normal" /> |
|||
</arc> |
|||
<arc id="arc6" source="p3" target="t3"> |
|||
<inscription> |
|||
<value>Default,1</value> |
|||
</inscription> |
|||
<type value="normal" /> |
|||
</arc> |
|||
<arc id="arc7" source="t3" target="p4"> |
|||
<inscription> |
|||
<value>Default,1</value> |
|||
</inscription> |
|||
<type value="normal" /> |
|||
</arc> |
|||
<arc id="arc8" source="p4" target="l1"> |
|||
<inscription> |
|||
<value>Default,1</value> |
|||
</inscription> |
|||
<type value="normal" /> |
|||
</arc> |
|||
<arc id="arc9" source="l1" target="p6"> |
|||
<inscription> |
|||
<value>Default,1</value> |
|||
</inscription> |
|||
<type value="normal" /> |
|||
</arc> |
|||
<arc id="arc10" source="p5" target="l2"> |
|||
<inscription> |
|||
<value>Default,1</value> |
|||
</inscription> |
|||
<type value="normal" /> |
|||
</arc> |
|||
<arc id="arc11" source="l2" target="p7"> |
|||
<inscription> |
|||
<value>Default,1</value> |
|||
</inscription> |
|||
<type value="normal" /> |
|||
</arc> |
|||
</net> |
|||
</pnml> |
|||
1236
examples/gspn/workflow_cluster/workflow_cluster.pnml
File diff suppressed because it is too large
View File
File diff suppressed because it is too large
View File
2604
examples/jani-examples/beb.jani
File diff suppressed because it is too large
View File
File diff suppressed because it is too large
View File
@ -1,27 +0,0 @@ |
|||
Peak memory usage: 38 MB |
|||
Analysis results for beb.jani |
|||
|
|||
+ State space exploration |
|||
States: 4528 |
|||
Transitions: 4874 |
|||
Branches: 6899 |
|||
Time: 0.0 s |
|||
Rate: 92408 states/s |
|||
|
|||
+ LineSeized |
|||
Probability: 0.9166259765625 |
|||
Time: 0.1 s |
|||
|
|||
+ Value iteration |
|||
Final error: 0 |
|||
Iterations: 8 |
|||
Time: 0.0 s |
|||
|
|||
+ GaveUp |
|||
Probability: 0.0833740234375 |
|||
Time: 0.0 s |
|||
|
|||
+ Value iteration |
|||
Final error: 0 |
|||
Iterations: 9 |
|||
Time: 0.0 s |
|||
@ -1,64 +0,0 @@ |
|||
// Modest MDP model of the bounded exponential backoff procedure (BEB) |
|||
// [BFHH11] |
|||
action tick, tack, tock; |
|||
|
|||
const int K = 4; // maximum value for backoff |
|||
const int N = 3; // number of tries before giving up |
|||
const int H = 3; // number of hosts (must correspond to the number of Host() instantiations in the global composition) |
|||
|
|||
int(0..2) cr; // count how many hosts attempt to seize the line in a slot (zero, one, many) |
|||
bool line_seized; |
|||
bool gave_up; |
|||
|
|||
property LineSeized = Pmax(<> line_seized); // some host managed to seize the line before any other gave up |
|||
property GaveUp = Pmax(<> gave_up); // some host gave up before any other managed to seize the line (does not work with POR) |
|||
|
|||
process Clock() |
|||
{ |
|||
tick; tack; tau {= cr = 0 =}; tock; Clock() |
|||
} |
|||
|
|||
process Host() |
|||
{ |
|||
int(0..N) na; // nr_attempts 0..N |
|||
int(0..K) ev = 2; // exp_val 0..K |
|||
int(0..K) wt; // slots_to_wait 0..K |
|||
|
|||
do |
|||
{ |
|||
if(wt > 0) |
|||
{ |
|||
// wait this slot |
|||
tick {= wt-- =} |
|||
} |
|||
else |
|||
{ |
|||
tau {= cr = min(2, cr + 1) =}; // attempt to seize the line |
|||
tick; |
|||
if(cr == 1) |
|||
{ |
|||
// someone managed to seize the line |
|||
tau {= line_seized = true =}; stop |
|||
} |
|||
else if(na >= N) |
|||
{ |
|||
// maximum number of attempts exceeded |
|||
tau {= gave_up = true =}; stop |
|||
} |
|||
else |
|||
{ |
|||
// backoff |
|||
tau {= na++, wt = DiscreteUniform(0, max(0, ev - 1)), ev = min(2 * ev, K) =} |
|||
} |
|||
}; |
|||
tack; tock |
|||
} |
|||
} |
|||
|
|||
par |
|||
{ |
|||
:: Clock() |
|||
:: Host() |
|||
:: Host() |
|||
:: Host() |
|||
} |
|||
@ -1,27 +0,0 @@ |
|||
Peak memory usage: 39 MB |
|||
Analysis results for beb.modest |
|||
|
|||
+ State space exploration |
|||
States: 4528 |
|||
Transitions: 4874 |
|||
Branches: 6899 |
|||
Time: 0.0 s |
|||
Rate: 94333 states/s |
|||
|
|||
+ LineSeized |
|||
Probability: 0.9166259765625 |
|||
Time: 0.1 s |
|||
|
|||
+ Value iteration |
|||
Final error: 0 |
|||
Iterations: 8 |
|||
Time: 0.0 s |
|||
|
|||
+ GaveUp |
|||
Probability: 0.0833740234375 |
|||
Time: 0.0 s |
|||
|
|||
+ Value iteration |
|||
Final error: 0 |
|||
Iterations: 9 |
|||
Time: 0.0 s |
|||
2092
examples/jani-examples/brp.jani
File diff suppressed because it is too large
View File
File diff suppressed because it is too large
View File
@ -1,63 +0,0 @@ |
|||
Peak memory usage: 39 MB |
|||
Analysis results for brp.jani |
|||
|
|||
+ State space exploration |
|||
States: 3959 |
|||
Transitions: 4244 |
|||
Branches: 4593 |
|||
Time: 0.1 s |
|||
Rate: 74698 states/s |
|||
|
|||
+ P_A |
|||
Probability: 0 |
|||
Time: 0.0 s |
|||
|
|||
+ Value iteration |
|||
Final error: 0 |
|||
Iterations: 1 |
|||
Time: 0.0 s |
|||
|
|||
+ P_B |
|||
Probability: 0 |
|||
Time: 0.0 s |
|||
|
|||
+ Value iteration |
|||
Final error: 0 |
|||
Iterations: 1 |
|||
Time: 0.0 s |
|||
|
|||
+ P_1 |
|||
Probability: 0.000423333443357766 |
|||
Time: 0.0 s |
|||
|
|||
+ Value iteration |
|||
Final error: 2.35005704803786E-07 |
|||
Iterations: 13 |
|||
Time: 0.0 s |
|||
|
|||
+ P_2 |
|||
Probability: 2.64530890961023E-05 |
|||
Time: 0.0 s |
|||
|
|||
+ Value iteration |
|||
Final error: 2.05561452068843E-07 |
|||
Iterations: 14 |
|||
Time: 0.0 s |
|||
|
|||
+ P_3 |
|||
Probability: 0.000185191226393368 |
|||
Time: 0.0 s |
|||
|
|||
+ Value iteration |
|||
Final error: 3.32462409056221E-07 |
|||
Iterations: 13 |
|||
Time: 0.0 s |
|||
|
|||
+ P_4 |
|||
Probability: 8E-06 |
|||
Time: 0.0 s |
|||
|
|||
+ Value iteration |
|||
Final error: 0 |
|||
Iterations: 2 |
|||
Time: 0.0 s |
|||
@ -1,213 +0,0 @@ |
|||
// Modest PTA model of the bounded retransmission protocol (BRP) |
|||
// [HH09], http://www.modestchecker.net/CaseStudies/BRP/ |
|||
action put, get, put_k, get_k, put_l, get_l; |
|||
action new_file; |
|||
action s_ok, s_dk, s_nok, s_restart; |
|||
action r_ok, r_inc, r_fst, r_nok, r_timeout; |
|||
exception error; |
|||
|
|||
const int N = 16; // number of frames per file |
|||
const int MAX = 2; // maximum number of retransmissions per frame |
|||
const int TD = 1; // transmission delay |
|||
const int TS = 2 * TD + 1; // sender timeout |
|||
const int TR = 2 * MAX * TS + 3 * TD; // receiver timeout |
|||
const int SYNC = TR; |
|||
|
|||
bool ff, lf, ab; // channel data: first/last frame, alternating bit |
|||
int(0..N) i; // sender chunk counter |
|||
bool inTransitK = false; |
|||
bool inTransitL = false; |
|||
|
|||
bool first_file_done = false; |
|||
bool get_k_seen, s_ok_seen, s_nok_seen, s_dk_seen, s_restart_seen, r_ok_seen, r_timeout_seen; |
|||
|
|||
// Invariant (timed) properties (from [BrpOnTime], the TA model) |
|||
bool premature_timeout, channel_k_overflow, channel_l_overflow; |
|||
// "there is at most one message in transit for each channel" |
|||
property T_1 = A[] (!(channel_k_overflow || channel_l_overflow)); |
|||
// "there is at most one message in transit in total" |
|||
property T_2 = A[] (!(inTransitK && inTransitL)); |
|||
// Assumption (A1): "no premature timeouts" |
|||
property T_A1 = A[] (!premature_timeout); |
|||
// Assumption (A2): "sender starts new file only after receiver reacted to failure" |
|||
// Note that receiver can only notice failure if it received at least one chunk, i.e. get_k_seen |
|||
property T_A2 = A[] (!s_restart_seen || !get_k_seen || r_timeout_seen); |
|||
|
|||
// Probabilistic reachability properties (from [D'AJJL01], the RAPTURE/PRISM model) |
|||
// property A of [D'AJJL01]: "the maximum probability that eventually the sender reports |
|||
// a certain unsuccessful transmission but the receiver got the complete file" |
|||
property P_A = Pmax(<>(s_nok_seen && r_ok_seen)); |
|||
// property B of [D'AJJL01]: "the maximum probability that eventually the sender reports |
|||
// a certain successful transmission but the receiver did not get the complete file" |
|||
property P_B = Pmax(<>(s_ok_seen && !r_ok_seen)); |
|||
// property 1 of [D'AJJL01]: "the maximum probability that eventually the sender |
|||
// does not report a successful transmission" |
|||
property P_1 = Pmax(<>(s_nok_seen || s_dk_seen)); |
|||
// property 2 of [D'AJJL01]: "the maximum probability that eventually the sender |
|||
// reports an uncertainty on the success of the transmission" |
|||
property P_2 = Pmax(<>(s_dk_seen)); |
|||
// property 3 of [D'AJJL01]: "the maximum probability that eventually the sender |
|||
// reports an unsuccessful transmission after more than 8 chunks have been sent successfully" |
|||
property P_3 = Pmax(<>(s_nok_seen && i > 8)); |
|||
// property 4 of [D'AJJL01]: "the maximum probability that eventually the receiver |
|||
// does not receive any chunk and the sender tried to send a chunk" |
|||
property P_4 = Pmax(<>((s_ok_seen || s_nok_seen || s_dk_seen) && !get_k_seen)); |
|||
|
|||
|
|||
process Sender() |
|||
{ |
|||
bool bit; |
|||
int(0..MAX) rc; |
|||
clock c; |
|||
|
|||
try |
|||
{ |
|||
do { |
|||
:: when urgent(i < N) {= i++ =}; |
|||
do |
|||
{ |
|||
// send frame |
|||
invariant(c <= 0) put_k {= ff = (i == 1), lf = (i == N), ab = bit, c = 0 =}; |
|||
invariant(c <= TS) alt { |
|||
:: // receive ack |
|||
get_l {= bit = !bit, rc = 0, c = 0 =}; |
|||
urgent break |
|||
:: // timeout |
|||
when(c >= TS) |
|||
if(rc < MAX) |
|||
{ |
|||
// retry |
|||
{= rc++, c = 0 =} |
|||
} |
|||
else if(i < N) |
|||
{ |
|||
// no retries left |
|||
s_nok {= rc = 0, c = 0 =}; |
|||
urgent throw(error) |
|||
} |
|||
else |
|||
{ |
|||
// no retries left |
|||
s_dk {= rc = 0, c = 0 =}; |
|||
urgent throw(error) |
|||
} |
|||
} |
|||
} |
|||
:: when(i == N) |
|||
// file transmission successfully completed |
|||
invariant(c <= 0) s_ok {= first_file_done = true =}; |
|||
urgent break |
|||
} |
|||
} |
|||
catch error |
|||
{ |
|||
// File transfer did not succeed: wait, then restart with next file |
|||
invariant(c <= SYNC) when(c >= SYNC) |
|||
s_restart {= bit = false, first_file_done = true =} |
|||
} |
|||
} |
|||
|
|||
process Receiver() |
|||
{ |
|||
bool r_ff, r_lf, r_ab; |
|||
bool bit; |
|||
clock c; |
|||
|
|||
// receive first frame |
|||
if(ff) { get_k {= c = 0, bit = ab, r_ff = ff, r_lf = lf, r_ab = ab =} } |
|||
else { get_k {= c = 0, premature_timeout = true =}; stop }; |
|||
do |
|||
{ |
|||
invariant(c <= 0) |
|||
{ |
|||
if(r_ab != bit) |
|||
{ |
|||
// repetition, re-ack |
|||
put_l |
|||
} |
|||
else |
|||
{ |
|||
// report frame |
|||
if(r_lf) { r_ok } |
|||
else if(r_ff) { r_fst } |
|||
else { r_inc }; |
|||
put_l {= bit = !bit =} |
|||
} |
|||
}; |
|||
invariant(c <= TR) |
|||
{ |
|||
alt { |
|||
:: // receive next frame |
|||
get_k {= c = 0, r_ff = ff, r_lf = lf, r_ab = ab =} |
|||
:: // timeout |
|||
when(c == TR) |
|||
if(r_lf) |
|||
{ |
|||
// we just got the last frame, though |
|||
r_timeout; break |
|||
} |
|||
else |
|||
{ |
|||
r_nok; |
|||
// abort transfer |
|||
r_timeout; break |
|||
} |
|||
} |
|||
} |
|||
}; |
|||
Receiver() |
|||
} |
|||
|
|||
process ChannelK() |
|||
{ |
|||
clock c; |
|||
|
|||
put_k palt |
|||
{ |
|||
:98: {= c = 0, inTransitK = true =}; |
|||
invariant(c <= TD) alt { |
|||
:: get_k {= inTransitK = false =} |
|||
:: put_k {= channel_k_overflow = true =}; stop |
|||
} |
|||
: 2: {==} |
|||
}; |
|||
ChannelK() |
|||
} |
|||
|
|||
process ChannelL() |
|||
{ |
|||
clock c; |
|||
|
|||
put_l palt |
|||
{ |
|||
:99: {= c = 0, inTransitL = true =}; |
|||
invariant(c <= TD) alt { |
|||
:: get_l {= inTransitL = false =} |
|||
:: put_l {= channel_l_overflow = true =}; stop |
|||
} |
|||
: 1: {==} |
|||
}; |
|||
ChannelL() |
|||
} |
|||
|
|||
process Observer() |
|||
{ |
|||
alt { |
|||
:: get_k {= get_k_seen = true =} |
|||
:: s_ok {= s_ok_seen = true =} |
|||
:: s_nok {= s_nok_seen = true =} |
|||
:: s_dk {= s_dk_seen = true =} |
|||
:: s_restart {= s_restart_seen = true =} |
|||
:: r_ok {= r_ok_seen = true =} |
|||
:: r_timeout {= r_timeout_seen = true =} |
|||
}; |
|||
Observer() |
|||
} |
|||
|
|||
par { |
|||
:: Sender() |
|||
:: Receiver() |
|||
:: ChannelK() |
|||
:: ChannelL() |
|||
:: Observer() |
|||
} |
|||
@ -1,63 +0,0 @@ |
|||
Peak memory usage: 40 MB |
|||
Analysis results for brp.modest |
|||
|
|||
+ State space exploration |
|||
States: 3959 |
|||
Transitions: 4244 |
|||
Branches: 4593 |
|||
Time: 0.1 s |
|||
Rate: 73315 states/s |
|||
|
|||
+ P_A |
|||
Probability: 0 |
|||
Time: 0.1 s |
|||
|
|||
+ Value iteration |
|||
Final error: 0 |
|||
Iterations: 1 |
|||
Time: 0.0 s |
|||
|
|||
+ P_B |
|||
Probability: 0 |
|||
Time: 0.0 s |
|||
|
|||
+ Value iteration |
|||
Final error: 0 |
|||
Iterations: 1 |
|||
Time: 0.0 s |
|||
|
|||
+ P_1 |
|||
Probability: 0.000423333443357766 |
|||
Time: 0.0 s |
|||
|
|||
+ Value iteration |
|||
Final error: 2.35005704803786E-07 |
|||
Iterations: 13 |
|||
Time: 0.0 s |
|||
|
|||
+ P_2 |
|||
Probability: 2.64530890961023E-05 |
|||
Time: 0.0 s |
|||
|
|||
+ Value iteration |
|||
Final error: 2.05561452068843E-07 |
|||
Iterations: 14 |
|||
Time: 0.0 s |
|||
|
|||
+ P_3 |
|||
Probability: 0.000185191226393368 |
|||
Time: 0.0 s |
|||
|
|||
+ Value iteration |
|||
Final error: 3.32462409056221E-07 |
|||
Iterations: 13 |
|||
Time: 0.0 s |
|||
|
|||
+ P_4 |
|||
Probability: 8E-06 |
|||
Time: 0.0 s |
|||
|
|||
+ Value iteration |
|||
Final error: 0 |
|||
Iterations: 2 |
|||
Time: 0.0 s |
|||
2129
examples/jani-examples/consensus-6.jani
File diff suppressed because it is too large
View File
File diff suppressed because it is too large
View File
@ -1,27 +0,0 @@ |
|||
Peak memory usage: 530 MB |
|||
Analysis results for consensus-6.jani |
|||
|
|||
+ State space exploration |
|||
States: 2345194 |
|||
Transitions: 9418584 |
|||
Branches: 13891248 |
|||
Time: 8.7 s |
|||
Rate: 270964 states/s |
|||
|
|||
+ C1 |
|||
Result: True |
|||
Time for min. prob. 0 states: 1.6 s |
|||
Time for min. prob. 1 states: 0.1 s |
|||
Time: 1.7 s |
|||
Min. probability: 1 |
|||
|
|||
+ C2 |
|||
Probability: 0.395776147642961 |
|||
Time for min. prob. 0 states: 2.0 s |
|||
Time for min. prob. 1 states: 0.1 s |
|||
Time: 125.8 s |
|||
|
|||
+ Value iteration |
|||
Final error: 9.96634356860147E-07 |
|||
Iterations: 2137 |
|||
Time: 123.8 s |
|||
@ -1,157 +0,0 @@ |
|||
// Modest version of http://www.prismmodelchecker.org/casestudies/consensus_prism.php |
|||
// Command line: mcsta.exe consensus-6.modest -S Memory --nochainopt --bounded-alg StateElimination -E "K=2" |
|||
|
|||
action done; |
|||
|
|||
// constants |
|||
const int N = 6; |
|||
const int K = 4; |
|||
const int range = 2 * (K + 1) * N; |
|||
const int counter_init = (K + 1) * N; |
|||
const int left = N; |
|||
const int right = 2 * (K + 1) * N - N; |
|||
|
|||
// shared coin |
|||
int(0..range) counter = counter_init; |
|||
reward coin_flips; |
|||
|
|||
property C1 = P(<> (fin1 == 1 && fin2 == 1 && fin3 == 1 && fin4 == 1 && fin5 == 1 && fin6 == 1)) >= 1; |
|||
property C2 = Pmin(<> (fin1 == 1 && fin2 == 1 && fin3 == 1 && fin4 == 1 && fin5 == 1 && fin6 == 1 && coin1 == 1 && coin2 == 1 && coin3 == 1 && coin4 == 1 && coin5 == 1 && coin6 == 1)); |
|||
|
|||
int(0..1) fin1, fin2, fin3, fin4, fin5, fin6; |
|||
int(0..1) coin1, coin2, coin3, coin4, coin5, coin6; |
|||
|
|||
process Tourist1() |
|||
{ |
|||
process Flip() { palt { :1: {= coin1 = 0, coin_flips++ =} :1: {= coin1 = 1, coin_flips++ =} }; Write() } |
|||
process Write() { |
|||
alt { |
|||
:: when(coin1 == 0 && counter > 0) {= counter-- =}; Check() |
|||
:: when(coin1 == 1 && counter < range) {= counter++, coin1 = 0 =}; Check() |
|||
} |
|||
} |
|||
process Check() { |
|||
alt { |
|||
:: when(counter <= left) {= coin1 = 0, fin1 = 1 =}; Finished() |
|||
:: when(counter >= right) {= coin1 = 1, fin1 = 1 =}; Finished() |
|||
:: when(counter > left && counter < right) Tourist1() |
|||
} |
|||
} |
|||
process Finished() { done; Finished() } |
|||
|
|||
Flip() |
|||
} |
|||
|
|||
process Tourist2() |
|||
{ |
|||
process Flip() { palt { :1: {= coin2 = 0, coin_flips++ =} :1: {= coin2 = 1, coin_flips++ =} }; Write() } |
|||
process Write() { |
|||
alt { |
|||
:: when(coin2 == 0 && counter > 0) {= counter-- =}; Check() |
|||
:: when(coin2 == 1 && counter < range) {= counter++, coin2 = 0 =}; Check() |
|||
} |
|||
} |
|||
process Check() { |
|||
alt { |
|||
:: when(counter <= left) {= coin2 = 0, fin2 = 1 =}; Finished() |
|||
:: when(counter >= right) {= coin2 = 1, fin2 = 1 =}; Finished() |
|||
:: when(counter > left && counter < right) Tourist2() |
|||
} |
|||
} |
|||
process Finished() { done; Finished() } |
|||
|
|||
Flip() |
|||
} |
|||
|
|||
process Tourist3() |
|||
{ |
|||
process Flip() { palt { :1: {= coin3 = 0, coin_flips++ =} :1: {= coin3 = 1, coin_flips++ =} }; Write() } |
|||
process Write() { |
|||
alt { |
|||
:: when(coin3 == 0 && counter > 0) {= counter-- =}; Check() |
|||
:: when(coin3 == 1 && counter < range) {= counter++, coin3 = 0 =}; Check() |
|||
} |
|||
} |
|||
process Check() { |
|||
alt { |
|||
:: when(counter <= left) {= coin3 = 0, fin3 = 1 =}; Finished() |
|||
:: when(counter >= right) {= coin3 = 1, fin3 = 1 =}; Finished() |
|||
:: when(counter > left && counter < right) Tourist3() |
|||
} |
|||
} |
|||
process Finished() { done; Finished() } |
|||
|
|||
Flip() |
|||
} |
|||
|
|||
process Tourist4() |
|||
{ |
|||
process Flip() { palt { :1: {= coin4 = 0, coin_flips++ =} :1: {= coin4 = 1, coin_flips++ =} }; Write() } |
|||
process Write() { |
|||
alt { |
|||
:: when(coin4 == 0 && counter > 0) {= counter-- =}; Check() |
|||
:: when(coin4 == 1 && counter < range) {= counter++, coin4 = 0 =}; Check() |
|||
} |
|||
} |
|||
process Check() { |
|||
alt { |
|||
:: when(counter <= left) {= coin4 = 0, fin4 = 1 =}; Finished() |
|||
:: when(counter >= right) {= coin4 = 1, fin4 = 1 =}; Finished() |
|||
:: when(counter > left && counter < right) Tourist4() |
|||
} |
|||
} |
|||
process Finished() { done; Finished() } |
|||
|
|||
Flip() |
|||
} |
|||
|
|||
process Tourist5() |
|||
{ |
|||
process Flip() { palt { :1: {= coin5 = 0, coin_flips++ =} :1: {= coin5 = 1, coin_flips++ =} }; Write() } |
|||
process Write() { |
|||
alt { |
|||
:: when(coin5 == 0 && counter > 0) {= counter-- =}; Check() |
|||
:: when(coin5 == 1 && counter < range) {= counter++, coin5 = 0 =}; Check() |
|||
} |
|||
} |
|||
process Check() { |
|||
alt { |
|||
:: when(counter <= left) {= coin5 = 0, fin5 = 1 =}; Finished() |
|||
:: when(counter >= right) {= coin5 = 1, fin5 = 1 =}; Finished() |
|||
:: when(counter > left && counter < right) Tourist5() |
|||
} |
|||
} |
|||
process Finished() { done; Finished() } |
|||
|
|||
Flip() |
|||
} |
|||
|
|||
process Tourist6() |
|||
{ |
|||
process Flip() { palt { :1: {= coin6 = 0, coin_flips++ =} :1: {= coin6 = 1, coin_flips++ =} }; Write() } |
|||
process Write() { |
|||
alt { |
|||
:: when(coin6 == 0 && counter > 0) {= counter-- =}; Check() |
|||
:: when(coin6 == 1 && counter < range) {= counter++, coin6 = 0 =}; Check() |
|||
} |
|||
} |
|||
process Check() { |
|||
alt { |
|||
:: when(counter <= left) {= coin6 = 0, fin6 = 1 =}; Finished() |
|||
:: when(counter >= right) {= coin6 = 1, fin6 = 1 =}; Finished() |
|||
:: when(counter > left && counter < right) Tourist6() |
|||
} |
|||
} |
|||
process Finished() { done; Finished() } |
|||
|
|||
Flip() |
|||
} |
|||
|
|||
par { |
|||
:: Tourist1() |
|||
:: Tourist2() |
|||
:: Tourist3() |
|||
:: Tourist4() |
|||
:: Tourist5() |
|||
:: Tourist6() |
|||
} |
|||
@ -1,27 +0,0 @@ |
|||
Peak memory usage: 531 MB |
|||
Analysis results for consensus-6.modest |
|||
|
|||
+ State space exploration |
|||
States: 2345194 |
|||
Transitions: 9418584 |
|||
Branches: 13891248 |
|||
Time: 8.2 s |
|||
Rate: 287507 states/s |
|||
|
|||
+ C1 |
|||
Result: True |
|||
Time for min. prob. 0 states: 1.5 s |
|||
Time for min. prob. 1 states: 0.2 s |
|||
Time: 1.7 s |
|||
Min. probability: 1 |
|||
|
|||
+ C2 |
|||
Probability: 0.395776147642961 |
|||
Time for min. prob. 0 states: 2.0 s |
|||
Time for min. prob. 1 states: 0.1 s |
|||
Time: 126.8 s |
|||
|
|||
+ Value iteration |
|||
Final error: 9.96634356860147E-07 |
|||
Iterations: 2137 |
|||
Time: 124.7 s |
|||
@ -1,354 +0,0 @@ |
|||
{ |
|||
"jani-version": 1, |
|||
"name": "dice", |
|||
"type" : "mdp", |
|||
"actions" : [], |
|||
"variables" : [ |
|||
{ |
|||
"name": "thrownSix", |
|||
"type": "bool", |
|||
"initial-value": false |
|||
}, |
|||
{ |
|||
"name": "terminated", |
|||
"type": "bool", |
|||
"initial-value": false |
|||
} |
|||
], |
|||
"rewards" : [ |
|||
{ |
|||
"name" : "step" |
|||
} |
|||
], |
|||
"properties" : [ |
|||
{ |
|||
"name" : "ProbThrowSix", |
|||
"reach" : "thrownSix", |
|||
"type": "probability-max-query" |
|||
}, |
|||
{ |
|||
"name" : "StepsUntilReach", |
|||
"reach" : "terminated", |
|||
"reward": "step", |
|||
"type": "expected-reachability-reward-max-query" |
|||
} |
|||
], |
|||
"automata" : [ |
|||
{ |
|||
"name" : "dice", |
|||
"variables" : [ |
|||
{ |
|||
"name" : "d", |
|||
"type" : { |
|||
"kind": "bounded", |
|||
"base": "int", |
|||
"lower-bound" : 0, |
|||
"upper-bound" : 6 |
|||
}, |
|||
"initial-value" : 0 |
|||
} |
|||
], |
|||
"locations" : [ |
|||
{ |
|||
"name" : "s0" |
|||
}, |
|||
{ |
|||
"name" : "s1" |
|||
}, |
|||
{ |
|||
"name" : "s2" |
|||
}, |
|||
{ |
|||
"name" : "s3" |
|||
}, |
|||
{ |
|||
"name" : "s4" |
|||
}, |
|||
{ |
|||
"name" : "s5" |
|||
}, |
|||
{ |
|||
"name" : "s6" |
|||
}, |
|||
{ |
|||
"name" : "s7" |
|||
} |
|||
], |
|||
"initial-location" : "s0", |
|||
"edges" : [ |
|||
{ |
|||
"location" : "s0", |
|||
"guard" : true, |
|||
"destinations" : [ |
|||
{ |
|||
"probability" : 0.5, |
|||
"location" : "s1", |
|||
"assignments" : [], |
|||
"rewards" : [ |
|||
{ |
|||
"ref" : "step", |
|||
"value" : 1 |
|||
} |
|||
] |
|||
}, |
|||
{ |
|||
"probability" : 0.5, |
|||
"location" : "s2", |
|||
"assignments" : [], |
|||
"rewards" : [ |
|||
{ |
|||
"ref" : "step", |
|||
"value" : 1 |
|||
} |
|||
] |
|||
} |
|||
] |
|||
}, |
|||
{ |
|||
"location" : "s1", |
|||
"guard" : true, |
|||
"destinations" : [ |
|||
{ |
|||
"probability" : 0.5, |
|||
"location" : "s3", |
|||
"assignments" : [], |
|||
"rewards" : [ |
|||
{ |
|||
"ref" : "step", |
|||
"value" : 1 |
|||
} |
|||
] |
|||
}, |
|||
{ |
|||
"probability" : 0.5, |
|||
"location" : "s4", |
|||
"assignments" : [], |
|||
"rewards" : [ |
|||
{ |
|||
"ref" : "step", |
|||
"value" : 1 |
|||
} |
|||
] |
|||
} |
|||
] |
|||
}, |
|||
{ |
|||
"location" : "s2", |
|||
"guard" : true, |
|||
"destinations" : [ |
|||
{ |
|||
"probability" : 0.5, |
|||
"location" : "s5", |
|||
"assignments" : [], |
|||
"rewards" : [ |
|||
{ |
|||
"ref" : "step", |
|||
"value" : 1 |
|||
} |
|||
] |
|||
}, |
|||
{ |
|||
"probability" : 0.5, |
|||
"location" : "s6", |
|||
"assignments" : [], |
|||
"rewards" : [ |
|||
{ |
|||
"ref" : "step", |
|||
"value" : 1 |
|||
} |
|||
] |
|||
} |
|||
] |
|||
}, |
|||
{ |
|||
"location" : "s3", |
|||
"guard" : true, |
|||
"destinations" : [ |
|||
{ |
|||
"probability" : 0.5, |
|||
"location" : "s1", |
|||
"assignments" : [], |
|||
"rewards" : [ |
|||
{ |
|||
"ref" : "step", |
|||
"value" : 1 |
|||
} |
|||
] |
|||
}, |
|||
{ |
|||
"probability" : 0.5, |
|||
"location" : "s7", |
|||
"assignments" : [ |
|||
{ |
|||
"ref" : "d", |
|||
"value" : 1 |
|||
}, |
|||
{ |
|||
"ref" : "terminated", |
|||
"value" : true |
|||
} |
|||
], |
|||
"rewards" : [ |
|||
{ |
|||
"ref" : "step", |
|||
"value" : 1 |
|||
} |
|||
] |
|||
} |
|||
] |
|||
}, |
|||
{ |
|||
"location" : "s4", |
|||
"guard" : true, |
|||
"destinations" : [ |
|||
{ |
|||
"probability" : 0.5, |
|||
"location" : "s7", |
|||
"assignments" : [ |
|||
{ |
|||
"ref" : "d", |
|||
"value" : 2 |
|||
}, |
|||
{ |
|||
"ref" : "terminated", |
|||
"value" : true |
|||
} |
|||
], |
|||
"rewards" : [ |
|||
{ |
|||
"ref" : "step", |
|||
"value" : 1 |
|||
} |
|||
] |
|||
}, |
|||
{ |
|||
"probability" : 0.5, |
|||
"location" : "s7", |
|||
"assignments" : [ |
|||
{ |
|||
"ref" : "d", |
|||
"value" : 3 |
|||
}, |
|||
{ |
|||
"ref" : "terminated", |
|||
"value" : true |
|||
} |
|||
], |
|||
"rewards" : [ |
|||
{ |
|||
"ref" : "step", |
|||
"value" : 1 |
|||
} |
|||
] |
|||
} |
|||
] |
|||
}, |
|||
{ |
|||
"location" : "s5", |
|||
"guard" : true, |
|||
"destinations" : [ |
|||
{ |
|||
"probability" : 0.5, |
|||
"location" : "s7", |
|||
"assignments" : [ |
|||
{ |
|||
"ref" : "d", |
|||
"value" : 4 |
|||
}, |
|||
{ |
|||
"ref" : "terminated", |
|||
"value" : true |
|||
} |
|||
], |
|||
"rewards" : [ |
|||
{ |
|||
"ref" : "step", |
|||
"value" : 1 |
|||
} |
|||
] |
|||
}, |
|||
{ |
|||
"probability" : 0.5, |
|||
"location" : "s7", |
|||
"assignments" : [ |
|||
{ |
|||
"ref" : "d", |
|||
"value" : 5 |
|||
}, |
|||
{ |
|||
"ref" : "terminated", |
|||
"value" : true |
|||
} |
|||
], |
|||
"rewards" : [ |
|||
{ |
|||
"ref" : "step", |
|||
"value" : 1 |
|||
} |
|||
] |
|||
} |
|||
] |
|||
}, |
|||
{ |
|||
"location" : "s6", |
|||
"guard" : true, |
|||
"destinations" : [ |
|||
{ |
|||
"probability" : 0.5, |
|||
"location" : "s2", |
|||
"assignments" : [], |
|||
"rewards" : [ |
|||
{ |
|||
"ref" : "step", |
|||
"value" : 1 |
|||
} |
|||
] |
|||
}, |
|||
{ |
|||
"probability" : 0.5, |
|||
"location" : "s7", |
|||
"assignments" : [ |
|||
{ |
|||
"ref" : "d", |
|||
"value" : 6 |
|||
}, |
|||
{ |
|||
"ref" : "thrownSix", |
|||
"value" : true |
|||
}, |
|||
{ |
|||
"ref" : "terminated", |
|||
"value" : true |
|||
} |
|||
], |
|||
"rewards" : [ |
|||
{ |
|||
"ref" : "step", |
|||
"value" : 1 |
|||
} |
|||
] |
|||
} |
|||
] |
|||
}, |
|||
{ |
|||
"location" : "s7", |
|||
"guard" : true, |
|||
"destinations" : [ |
|||
{ |
|||
"probability" : 1, |
|||
"location" : "s7", |
|||
"assignments" : [], |
|||
"rewards" : [ |
|||
{ |
|||
"ref" : "step", |
|||
"value" : 1 |
|||
} |
|||
] |
|||
} |
|||
] |
|||
} |
|||
] |
|||
} |
|||
], |
|||
"system" : "dice" |
|||
} |
|||
@ -1,29 +0,0 @@ |
|||
Peak memory usage: 36 MB |
|||
Analysis results for dice.jani |
|||
|
|||
+ State space exploration |
|||
States: 8 |
|||
Transitions: 8 |
|||
Branches: 14 |
|||
Time: 0.0 s |
|||
Rate: 190 states/s |
|||
|
|||
+ ProbThrowSix |
|||
Probability: 0.166666626930237 |
|||
Time: 0.0 s |
|||
|
|||
+ Value iteration |
|||
Final error: 7.15255907834985E-07 |
|||
Iterations: 11 |
|||
Time: 0.0 s |
|||
|
|||
+ StepsUntilReach |
|||
Value: 3.66666650772095 |
|||
Time for min. prob. 0 states: 0.0 s |
|||
Time for min. prob. 1 states: 0.0 s |
|||
Time: 0.0 s |
|||
|
|||
+ Value iteration |
|||
Final error: 4.08717619857464E-07 |
|||
Iterations: 12 |
|||
Time: 0.0 s |
|||
@ -0,0 +1,87 @@ |
|||
// polling example [IT90] |
|||
// gxn/dxp 26/01/00 |
|||
|
|||
ctmc |
|||
|
|||
const int N=6; |
|||
|
|||
const double mu; |
|||
const double gamma; |
|||
|
|||
//const double mu= 1; |
|||
//const double gamma= 200; |
|||
//const double lambda= mu/N; |
|||
|
|||
module server |
|||
|
|||
s : [1..6]; // station |
|||
a : [0..1]; // action: 0=polling, 1=serving |
|||
|
|||
[loop1a] (s=1)&(a=0) -> gamma : (s'=s+1); |
|||
[loop1b] (s=1)&(a=0) -> gamma : (a'=1); |
|||
[serve1] (s=1)&(a=1) -> mu : (s'=s+1)&(a'=0); |
|||
|
|||
[loop2a] (s=2)&(a=0) -> gamma : (s'=s+1); |
|||
[loop2b] (s=2)&(a=0) -> gamma : (a'=1); |
|||
[serve2] (s=2)&(a=1) -> mu : (s'=s+1)&(a'=0); |
|||
|
|||
[loop3a] (s=3)&(a=0) -> gamma : (s'=s+1); |
|||
[loop3b] (s=3)&(a=0) -> gamma : (a'=1); |
|||
[serve3] (s=3)&(a=1) -> mu : (s'=s+1)&(a'=0); |
|||
|
|||
[loop4a] (s=4)&(a=0) -> gamma : (s'=s+1); |
|||
[loop4b] (s=4)&(a=0) -> gamma : (a'=1); |
|||
[serve4] (s=4)&(a=1) -> mu : (s'=s+1)&(a'=0); |
|||
|
|||
[loop5a] (s=5)&(a=0) -> gamma : (s'=s+1); |
|||
[loop5b] (s=5)&(a=0) -> gamma : (a'=1); |
|||
[serve5] (s=5)&(a=1) -> mu : (s'=s+1)&(a'=0); |
|||
|
|||
[loop6a] (s=6)&(a=0) -> gamma : (s'=1); |
|||
[loop6b] (s=6)&(a=0) -> gamma : (a'=1); |
|||
[serve6] (s=6)&(a=1) -> mu : (s'=1)&(a'=0); |
|||
|
|||
endmodule |
|||
|
|||
module station1 |
|||
|
|||
s1 : [0..1]; |
|||
|
|||
[loop1a] (s1=0) -> 1 : (s1'=0); |
|||
[] (s1=0) -> mu/N : (s1'=1); |
|||
[loop1b] (s1=1) -> 1 : (s1'=1); |
|||
[serve1] (s1=1) -> 1 : (s1'=0); |
|||
|
|||
endmodule |
|||
|
|||
// construct further stations through renaming |
|||
module station2 = station1 [s1=s2, loop1a=loop2a, loop1b=loop2b, serve1=serve2] endmodule |
|||
module station3 = station1 [s1=s3, loop1a=loop3a, loop1b=loop3b, serve1=serve3] endmodule |
|||
module station4 = station1 [s1=s4, loop1a=loop4a, loop1b=loop4b, serve1=serve4] endmodule |
|||
module station5 = station1 [s1=s5, loop1a=loop5a, loop1b=loop5b, serve1=serve5] endmodule |
|||
module station6 = station1 [s1=s6, loop1a=loop6a, loop1b=loop6b, serve1=serve6] endmodule |
|||
|
|||
// cumulative rewards |
|||
|
|||
rewards "waiting" // expected time the station 1 is waiting to be served |
|||
s1=1 & !(s=1 & a=1) : 1; |
|||
endrewards |
|||
|
|||
rewards "served" // expected number of times station1 is served |
|||
[serve1] true : 1; |
|||
endrewards |
|||
|
|||
label "server1serving" = s=1 & a=1; |
|||
label "server5polling" = s=5 & a=0; |
|||
label "server5serving" = s=5 & a=1; |
|||
|
|||
init |
|||
s = 1 & |
|||
a = 0 & |
|||
s1 = 0 & |
|||
s2 = 0 & |
|||
s3 = 0 & |
|||
s4 = 0 & |
|||
s5 = 0 & |
|||
s6 = 0 |
|||
endinit |
|||
@ -0,0 +1,35 @@ |
|||
// Knuth's model of a fair die using only fair coins |
|||
dtmc |
|||
|
|||
const double p; |
|||
const double q; |
|||
|
|||
module die |
|||
|
|||
// local state |
|||
s : [0..7] init 0; |
|||
// value of the dice |
|||
d : [0..6] init 0; |
|||
|
|||
[] s=0 -> p : (s'=1) + 1-p : (s'=2); |
|||
[] s=1 -> q : (s'=3) + 1-q : (s'=4); |
|||
[] s=2 -> q : (s'=5) + 1-q : (s'=6); |
|||
[] s=3 -> p : (s'=1) + 1-p : (s'=7) & (d'=1); |
|||
[] s=4 -> p : (s'=7) & (d'=3) + 1-p : (s'=7) & (d'=2); |
|||
[] s=5 -> p : (s'=2) + 1-p : (s'=7) & (d'=4); |
|||
[] s=6 -> p : (s'=7) & (d'=6) + 1-p : (s'=7) & (d'=5); |
|||
[] s=7 -> 1: (s'=7); |
|||
|
|||
endmodule |
|||
|
|||
rewards "coin_flips" |
|||
[] s<7 : 1; |
|||
endrewards |
|||
|
|||
label "one" = s=7&d=1; |
|||
label "two" = s=7&d=2; |
|||
label "three" = s=7&d=3; |
|||
label "four" = s=7&d=4; |
|||
label "five" = s=7&d=5; |
|||
label "six" = s=7&d=6; |
|||
label "end" = s=7; |
|||
@ -0,0 +1,44 @@ |
|||
// Knuth's model of a fair die using only fair coins |
|||
dtmc |
|||
|
|||
const double p; |
|||
const double q; |
|||
|
|||
module die1 |
|||
|
|||
// local state |
|||
s1 : [0..7] init 0; |
|||
// value of the dice |
|||
d1 : [0..6] init 0; |
|||
|
|||
[] s1=0 -> p : (s1'=1) + 1-p : (s1'=2); |
|||
[] s1=1 -> q : (s1'=3) + 1-q : (s1'=4); |
|||
[] s1=2 -> q : (s1'=5) + 1-q : (s1'=6); |
|||
[] s1=3 -> p : (s1'=1) + 1-p : (s1'=7) & (d1'=1); |
|||
[] s1=4 -> p : (s1'=7) & (d1'=3) + 1-p : (s1'=7) & (d1'=2); |
|||
[] s1=5 -> p : (s1'=2) + 1-p : (s1'=7) & (d1'=4); |
|||
[] s1=6 -> p : (s1'=7) & (d1'=6) + 1-p : (s1'=7) & (d1'=5); |
|||
[] s1=7 -> 1: (s1'=7); |
|||
|
|||
endmodule |
|||
|
|||
module die2 = die1 [ s1=s2, s2=s1, d1=d2 ] endmodule |
|||
|
|||
rewards "coin_flips" |
|||
[] s1<7 | s2<7 : 1; |
|||
endrewards |
|||
|
|||
label "two" = s1=7 & s2=7 & d1+d2=2; |
|||
label "three" = s1=7 & s2=7 & d1+d2=3; |
|||
label "four" = s1=7 & s2=7 & d1+d2=4; |
|||
label "five" = s1=7 & s2=7 & d1+d2=5; |
|||
label "six" = s1=7 & s2=7 & d1+d2=6; |
|||
label "seven" = s1=7 & s2=7 & d1+d2=7; |
|||
label "eight" = s1=7 & s2=7 & d1+d2=8; |
|||
label "nine" = s1=7 & s2=7 & d1+d2=9; |
|||
label "ten" = s1=7 & s2=7 & d1+d2=10; |
|||
label "eleven" = s1=7 & s2=7 & d1+d2=11; |
|||
label "twelve" = s1=7 & s2=7 & d1+d2=12; |
|||
label "same" = s1=7 & s2=7 & d1=d2; |
|||
|
|||
label "end" = s1=7 & s2=7; |
|||
@ -0,0 +1,58 @@ |
|||
function coupon10() { |
|||
int coup0 := 0; |
|||
int coup1 := 0; |
|||
int coup2 := 0; |
|||
int coup3 := 0; |
|||
int coup4 := 0; |
|||
int coup5 := 0; |
|||
int coup6 := 0; |
|||
int coup7 := 0; |
|||
int coup8 := 0; |
|||
int coup9 := 0; |
|||
int coup10 := 0; |
|||
|
|||
int draw := 0; |
|||
|
|||
int numberDraws := 0; |
|||
|
|||
while (!(coup0 = 1) | !(coup1 = 1) | !(coup2 = 1) | !(coup3 = 1) | !(coup4 = 1) | !(coup5= 1) | !(coup6 = 1) | !(coup7 = 1) | !(coup8 = 1) | !(coup9 = 1) | !(coup10 = 1)) { |
|||
draw := unif(0,10); |
|||
draw2 := unif(0,10); |
|||
draw3 := unif(0,10); |
|||
numberDraws := numberDraws + 1; |
|||
|
|||
if(draw = 0) { |
|||
coup0 := 1; |
|||
} |
|||
if(draw = 1) { |
|||
coup1 := 1; |
|||
} |
|||
if(draw = 2) { |
|||
coup2 := 1; |
|||
} |
|||
if(draw = 3) { |
|||
coup3 := 1; |
|||
} |
|||
if(draw = 4) { |
|||
coup4 := 1; |
|||
} |
|||
if(draw = 5) { |
|||
coup5 := 1; |
|||
} |
|||
if(draw = 6) { |
|||
coup6 := 1; |
|||
} |
|||
if(draw = 7) { |
|||
coup7 := 1; |
|||
} |
|||
if(draw = 8) { |
|||
coup8 := 1; |
|||
} |
|||
if(draw = 9) { |
|||
coup9 := 1; |
|||
} |
|||
if(draw = 10) { |
|||
coup10 := 1; |
|||
} |
|||
} |
|||
} |
|||
@ -0,0 +1,60 @@ |
|||
function coupon10() { |
|||
int coup0 := 0; |
|||
int coup1 := 0; |
|||
int coup2 := 0; |
|||
int coup3 := 0; |
|||
int coup4 := 0; |
|||
int coup5 := 0; |
|||
int coup6 := 0; |
|||
int coup7 := 0; |
|||
int coup8 := 0; |
|||
int coup9 := 0; |
|||
int coup10 := 0; |
|||
|
|||
int draw1 := 0; |
|||
int draw2 := 0; |
|||
int draw3 := 0; |
|||
|
|||
int cost := 1; |
|||
|
|||
while (!(coup0 = 1) | !(coup1 = 1) | !(coup2 = 1) | !(coup3 = 1) | !(coup4 = 1) | !(coup5= 1) | !(coup6 = 1) | !(coup7 = 1) | !(coup8 = 1) | !(coup9 = 1) | !(coup10 = 1)) { |
|||
draw1 := unif(0,10); |
|||
draw2 := unif(0,10); |
|||
draw3 := unif(0,10); |
|||
cost := ceil(1.02 * cost); |
|||
|
|||
if(draw1 = 0 | draw2 = 0 | draw3 = 0) { |
|||
coup0 := 1; |
|||
} |
|||
if(draw1 = 1 | draw2 = 1 | draw3 = 1) { |
|||
coup1 := 1; |
|||
} |
|||
if(draw1 = 2 | draw2 = 2 | draw3 = 2) { |
|||
coup2 := 1; |
|||
} |
|||
if (draw1 = 3 | draw2 = 3 | draw3 = 3) { |
|||
coup3 := 1; |
|||
} |
|||
if (draw1 = 4 | draw2 = 4 | draw3 = 4) { |
|||
coup4 := 1; |
|||
} |
|||
if (draw1 = 5 | draw2 = 5 | draw3 = 5) { |
|||
coup5 := 1; |
|||
} |
|||
if (draw1 = 6 | draw2 = 6 | draw3 = 6) { |
|||
coup6 := 1; |
|||
} |
|||
if (draw1 = 7 | draw2 = 7 | draw3 = 7) { |
|||
coup7 := 1; |
|||
} |
|||
if (draw1 = 8 | draw2 = 8 | draw3 = 8) { |
|||
coup8 := 1; |
|||
} |
|||
if (draw1 = 9 | draw2 = 9 | draw3 = 9) { |
|||
coup9 := 1; |
|||
} |
|||
if (draw1 = 10 | draw2 = 10 | draw3 = 10) { |
|||
coup10 := 1; |
|||
} |
|||
} |
|||
} |
|||
@ -0,0 +1,62 @@ |
|||
function coupon10() { |
|||
int coup0 := 0; |
|||
int coup1 := 0; |
|||
int coup2 := 0; |
|||
int coup3 := 0; |
|||
int coup4 := 0; |
|||
int coup5 := 0; |
|||
int coup6 := 0; |
|||
int coup7 := 0; |
|||
int coup8 := 0; |
|||
int coup9 := 0; |
|||
int coup10 := 0; |
|||
|
|||
int draw1 := 0; |
|||
int draw2 := 0; |
|||
int draw3 := 0; |
|||
|
|||
int numberDraws := 0; |
|||
|
|||
while (!(coup0 = 1) | !(coup1 = 1) | !(coup2 = 1) | !(coup3 = 1) | !(coup4 = 1) | !(coup5= 1) | !(coup6 = 1) | !(coup7 = 1) | !(coup8 = 1) | !(coup9 = 1) | !(coup10 = 1)) { |
|||
draw1 := unif(0,10); |
|||
draw2 := unif(0,10); |
|||
draw3 := unif(0,10); |
|||
numberDraws := numberDraws + 1; |
|||
|
|||
observe (draw1 != draw2 & draw1 != draw3 & draw2 != draw3); |
|||
|
|||
if(draw1 = 0 | draw2 = 0 | draw3 = 0) { |
|||
coup0 := 1; |
|||
} |
|||
if(draw1 = 1 | draw2 = 1 | draw3 = 1) { |
|||
coup1 := 1; |
|||
} |
|||
if(draw1 = 2 | draw2 = 2 | draw3 = 2) { |
|||
coup2 := 1; |
|||
} |
|||
if (draw1 = 3 | draw2 = 3 | draw3 = 3) { |
|||
coup3 := 1; |
|||
} |
|||
if (draw1 = 4 | draw2 = 4 | draw3 = 4) { |
|||
coup4 := 1; |
|||
} |
|||
if (draw1 = 5 | draw2 = 5 | draw3 = 5) { |
|||
coup5 := 1; |
|||
} |
|||
if (draw1 = 6 | draw2 = 6 | draw3 = 6) { |
|||
coup6 := 1; |
|||
} |
|||
if (draw1 = 7 | draw2 = 7 | draw3 = 7) { |
|||
coup7 := 1; |
|||
} |
|||
if (draw1 = 8 | draw2 = 8 | draw3 = 8) { |
|||
coup8 := 1; |
|||
} |
|||
if (draw1 = 9 | draw2 = 9 | draw3 = 9) { |
|||
coup9 := 1; |
|||
} |
|||
if (draw1 = 10 | draw2 = 10 | draw3 = 10) { |
|||
coup10 := 1; |
|||
} |
|||
} |
|||
} |
|||
@ -0,0 +1,60 @@ |
|||
function coupon10() { |
|||
int coup0 := 0; |
|||
int coup1 := 0; |
|||
int coup2 := 0; |
|||
int coup3 := 0; |
|||
int coup4 := 0; |
|||
int coup5 := 0; |
|||
int coup6 := 0; |
|||
int coup7 := 0; |
|||
int coup8 := 0; |
|||
int coup9 := 0; |
|||
int coup10 := 0; |
|||
|
|||
int draw1 := 0; |
|||
int draw2 := 0; |
|||
int draw3 := 0; |
|||
|
|||
int numberDraws := 0; |
|||
|
|||
while (!(coup0 = 1) | !(coup1 = 1) | !(coup2 = 1) | !(coup3 = 1) | !(coup4 = 1) | !(coup5= 1) | !(coup6 = 1) | !(coup7 = 1) | !(coup8 = 1) | !(coup9 = 1) | !(coup10 = 1)) { |
|||
draw1 := unif(0,10); |
|||
draw2 := unif(0,10); |
|||
draw3 := unif(0,10); |
|||
numberDraws := numberDraws + 1; |
|||
|
|||
if(draw1 = 0 | draw2 = 0 | draw3 = 0) { |
|||
coup0 := 1; |
|||
} |
|||
if(draw1 = 1 | draw2 = 1 | draw3 = 1) { |
|||
coup1 := 1; |
|||
} |
|||
if(draw1 = 2 | draw2 = 2 | draw3 = 2) { |
|||
coup2 := 1; |
|||
} |
|||
if (draw1 = 3 | draw2 = 3 | draw3 = 3) { |
|||
coup3 := 1; |
|||
} |
|||
if (draw1 = 4 | draw2 = 4 | draw3 = 4) { |
|||
coup4 := 1; |
|||
} |
|||
if (draw1 = 5 | draw2 = 5 | draw3 = 5) { |
|||
coup5 := 1; |
|||
} |
|||
if (draw1 = 6 | draw2 = 6 | draw3 = 6) { |
|||
coup6 := 1; |
|||
} |
|||
if (draw1 = 7 | draw2 = 7 | draw3 = 7) { |
|||
coup7 := 1; |
|||
} |
|||
if (draw1 = 8 | draw2 = 8 | draw3 = 8) { |
|||
coup8 := 1; |
|||
} |
|||
if (draw1 = 9 | draw2 = 9 | draw3 = 9) { |
|||
coup9 := 1; |
|||
} |
|||
if (draw1 = 10 | draw2 = 10 | draw3 = 10) { |
|||
coup10 := 1; |
|||
} |
|||
} |
|||
} |
|||
@ -0,0 +1,24 @@ |
|||
function coupon3() { |
|||
int coup0 := 0; |
|||
int coup1 := 0; |
|||
int coup2 := 0; |
|||
|
|||
int draw := 0; |
|||
|
|||
int numberDraws := 0; |
|||
|
|||
while (!(coup0 = 1) | !(coup1 = 1) | !(coup2 = 1)) { |
|||
draw := unif(0,2); |
|||
numberDraws := numberDraws + 1; |
|||
|
|||
if(draw = 0) { |
|||
coup0 := 1; |
|||
} |
|||
if(draw = 1) { |
|||
coup1 := 1; |
|||
} |
|||
if(draw = 2) { |
|||
coup2 := 1; |
|||
} |
|||
} |
|||
} |
|||
@ -0,0 +1,28 @@ |
|||
function coupon3() { |
|||
int coup0 := 0; |
|||
int coup1 := 0; |
|||
int coup2 := 0; |
|||
|
|||
int draw1 := 0; |
|||
int draw2 := 0; |
|||
int draw3 := 0; |
|||
|
|||
int cost := 1; |
|||
|
|||
while (!(coup0 = 1) | !(coup1 = 1) | !(coup2 = 1)) { |
|||
draw1 := unif(0,2); |
|||
draw2 := unif(0,2); |
|||
draw3 := unif(0,2); |
|||
cost := ceil(1.02 * cost); |
|||
|
|||
if(draw1 = 0 | draw2 = 0 | draw3 = 0) { |
|||
coup0 := 1; |
|||
} |
|||
if(draw1 = 1 | draw2 = 1 | draw3 = 1) { |
|||
coup1 := 1; |
|||
} |
|||
if(draw1 = 2 | draw2 = 2 | draw3 = 2) { |
|||
coup2 := 1; |
|||
} |
|||
} |
|||
} |
|||
@ -0,0 +1,30 @@ |
|||
function coupon3() { |
|||
int coup0 := 0; |
|||
int coup1 := 0; |
|||
int coup2 := 0; |
|||
|
|||
int draw1 := 0; |
|||
int draw2 := 0; |
|||
int draw3 := 0; |
|||
|
|||
int numberDraws := 0; |
|||
|
|||
while (!(coup0 = 1) | !(coup1 = 1) | !(coup2 = 1)) { |
|||
draw1 := unif(0,2); |
|||
draw2 := unif(0,2); |
|||
draw3 := unif(0,2); |
|||
numberDraws := numberDraws + 1; |
|||
|
|||
observe (draw1 != draw2 & draw1 != draw3 & draw2 != draw3); |
|||
|
|||
if(draw1 = 0 | draw2 = 0 | draw3 = 0) { |
|||
coup0 := 1; |
|||
} |
|||
if(draw1 = 1 | draw2 = 1 | draw3 = 1) { |
|||
coup1 := 1; |
|||
} |
|||
if(draw1 = 2 | draw2 = 2 | draw3 = 2) { |
|||
coup2 := 1; |
|||
} |
|||
} |
|||
} |
|||
@ -0,0 +1,28 @@ |
|||
function coupon3() { |
|||
int coup0 := 0; |
|||
int coup1 := 0; |
|||
int coup2 := 0; |
|||
|
|||
int draw1 := 0; |
|||
int draw2 := 0; |
|||
int draw3 := 0; |
|||
|
|||
int numberDraws := 0; |
|||
|
|||
while (!(coup0 = 1) | !(coup1 = 1) | !(coup2 = 1)) { |
|||
draw1 := unif(0,2); |
|||
draw2 := unif(0,2); |
|||
draw3 := unif(0,2); |
|||
numberDraws := numberDraws + 1; |
|||
|
|||
if(draw1 = 0 | draw2 = 0 | draw3 = 0) { |
|||
coup0 := 1; |
|||
} |
|||
if(draw1 = 1 | draw2 = 1 | draw3 = 1) { |
|||
coup1 := 1; |
|||
} |
|||
if(draw1 = 2 | draw2 = 2 | draw3 = 2) { |
|||
coup2 := 1; |
|||
} |
|||
} |
|||
} |
|||
@ -0,0 +1,34 @@ |
|||
function coupon4() { |
|||
int coup0 := 0; |
|||
int coup1 := 0; |
|||
int coup2 := 0; |
|||
int coup3 := 0; |
|||
|
|||
int draw1 := 0; |
|||
int draw2 := 0; |
|||
int draw3 := 0; |
|||
|
|||
int numberDraws := 0; |
|||
|
|||
while (!(coup0 = 1) | !(coup1 = 1) | !(coup2 = 1) | !(coup3 = 1)) { |
|||
draw1 := unif(0,4); |
|||
draw2 := unif(0,4); |
|||
draw3 := unif(0,4); |
|||
numberDraws := numberDraws + 1; |
|||
|
|||
observe (draw1 != draw2 & draw1 != draw3 & draw2 != draw3); |
|||
|
|||
if(draw1 = 0 | draw2 = 0 | draw3 = 0) { |
|||
coup0 := 1; |
|||
} |
|||
if(draw1 = 1 | draw2 = 1 | draw3 = 1) { |
|||
coup1 := 1; |
|||
} |
|||
if(draw1 = 2 | draw2 = 2 | draw3 = 2) { |
|||
coup2 := 1; |
|||
} |
|||
if (draw1 = 3 | draw2 = 3 | draw3 = 3) { |
|||
coup3 := 1; |
|||
} |
|||
} |
|||
} |
|||
@ -0,0 +1,32 @@ |
|||
function coupon5() { |
|||
int coup0 := 0; |
|||
int coup1 := 0; |
|||
int coup2 := 0; |
|||
int coup3 := 0; |
|||
int coup4 := 0; |
|||
|
|||
int draw := 0; |
|||
|
|||
int numberDraws := 0; |
|||
|
|||
while (!(coup0 = 1) | !(coup1 = 1) | !(coup2 = 1) | !(coup3 = 1) | !(coup4 = 1)) { |
|||
draw := unif(0,4); |
|||
numberDraws := numberDraws + 1; |
|||
|
|||
if(draw = 0) { |
|||
coup0 := 1; |
|||
} |
|||
if(draw = 1) { |
|||
coup1 := 1; |
|||
} |
|||
if(draw = 2) { |
|||
coup2 := 1; |
|||
} |
|||
if(draw = 3) { |
|||
coup3 := 1; |
|||
} |
|||
if(draw = 4) { |
|||
coup4 := 1; |
|||
} |
|||
} |
|||
} |
|||
@ -0,0 +1,36 @@ |
|||
function coupon5() { |
|||
int coup0 := 0; |
|||
int coup1 := 0; |
|||
int coup2 := 0; |
|||
int coup3 := 0; |
|||
int coup4 := 0; |
|||
|
|||
int draw1 := 0; |
|||
int draw2 := 0; |
|||
int draw3 := 0; |
|||
|
|||
int cost := 1; |
|||
|
|||
while (!(coup0 = 1) | !(coup1 = 1) | !(coup2 = 1) | !(coup3 = 1) | !(coup4 = 1)) { |
|||
draw1 := unif(0,4); |
|||
draw2 := unif(0,4); |
|||
draw3 := unif(0,4); |
|||
cost := ceil(1.02 * cost); |
|||
|
|||
if(draw1 = 0 | draw2 = 0 | draw3 = 0) { |
|||
coup0 := 1; |
|||
} |
|||
if(draw1 = 1 | draw2 = 1 | draw3 = 1) { |
|||
coup1 := 1; |
|||
} |
|||
if(draw1 = 2 | draw2 = 2 | draw3 = 2) { |
|||
coup2 := 1; |
|||
} |
|||
if (draw1 = 3 | draw2 = 3 | draw3 = 3) { |
|||
coup3 := 1; |
|||
} |
|||
if (draw1 = 4 | draw2 = 4 | draw3 = 4) { |
|||
coup4 := 1; |
|||
} |
|||
} |
|||
} |
|||
@ -0,0 +1,38 @@ |
|||
function coupon5() { |
|||
int coup0 := 0; |
|||
int coup1 := 0; |
|||
int coup2 := 0; |
|||
int coup3 := 0; |
|||
int coup4 := 0; |
|||
|
|||
int draw1 := 0; |
|||
int draw2 := 0; |
|||
int draw3 := 0; |
|||
|
|||
int numberDraws := 0; |
|||
|
|||
while (!(coup0 = 1) | !(coup1 = 1) | !(coup2 = 1) | !(coup3 = 1) | !(coup4 = 1)) { |
|||
draw1 := unif(0,4); |
|||
draw2 := unif(0,4); |
|||
draw3 := unif(0,4); |
|||
numberDraws := numberDraws + 1; |
|||
|
|||
observe (draw1 != draw2 & draw1 != draw3 & draw2 != draw3); |
|||
|
|||
if(draw1 = 0 | draw2 = 0 | draw3 = 0) { |
|||
coup0 := 1; |
|||
} |
|||
if(draw1 = 1 | draw2 = 1 | draw3 = 1) { |
|||
coup1 := 1; |
|||
} |
|||
if(draw1 = 2 | draw2 = 2 | draw3 = 2) { |
|||
coup2 := 1; |
|||
} |
|||
if (draw1 = 3 | draw2 = 3 | draw3 = 3) { |
|||
coup3 := 1; |
|||
} |
|||
if (draw1 = 4 | draw2 = 4 | draw3 = 4) { |
|||
coup4 := 1; |
|||
} |
|||
} |
|||
} |
|||
@ -0,0 +1,36 @@ |
|||
function coupon5() { |
|||
int coup0 := 0; |
|||
int coup1 := 0; |
|||
int coup2 := 0; |
|||
int coup3 := 0; |
|||
int coup4 := 0; |
|||
|
|||
int draw1 := 0; |
|||
int draw2 := 0; |
|||
int draw3 := 0; |
|||
|
|||
int numberDraws := 0; |
|||
|
|||
while (!(coup0 = 1) | !(coup1 = 1) | !(coup2 = 1) | !(coup3 = 1) | !(coup4 = 1)) { |
|||
draw1 := unif(0,4); |
|||
draw2 := unif(0,4); |
|||
draw3 := unif(0,4); |
|||
numberDraws := numberDraws + 1; |
|||
|
|||
if(draw1 = 0 | draw2 = 0 | draw3 = 0) { |
|||
coup0 := 1; |
|||
} |
|||
if(draw1 = 1 | draw2 = 1 | draw3 = 1) { |
|||
coup1 := 1; |
|||
} |
|||
if(draw1 = 2 | draw2 = 2 | draw3 = 2) { |
|||
coup2 := 1; |
|||
} |
|||
if (draw1 = 3 | draw2 = 3 | draw3 = 3) { |
|||
coup3 := 1; |
|||
} |
|||
if (draw1 = 4 | draw2 = 4 | draw3 = 4) { |
|||
coup4 := 1; |
|||
} |
|||
} |
|||
} |
|||
@ -0,0 +1,40 @@ |
|||
function coupon7() { |
|||
int coup0 := 0; |
|||
int coup1 := 0; |
|||
int coup2 := 0; |
|||
int coup3 := 0; |
|||
int coup4 := 0; |
|||
int coup5 := 0; |
|||
int coup6 := 0; |
|||
|
|||
int draw := 0; |
|||
|
|||
int numberDraws := 0; |
|||
|
|||
while (!(coup0 = 1) | !(coup1 = 1) | !(coup2 = 1) | !(coup3 = 1) | !(coup4 = 1) | !(coup5= 1) | !(coup6 = 1)) { |
|||
draw := unif(0,6); |
|||
numberDraws := numberDraws + 1; |
|||
|
|||
if(draw = 0) { |
|||
coup0 := 1; |
|||
} |
|||
if(draw = 1) { |
|||
coup1 := 1; |
|||
} |
|||
if(draw = 2) { |
|||
coup2 := 1; |
|||
} |
|||
if(draw = 3) { |
|||
coup3 := 1; |
|||
} |
|||
if(draw = 4) { |
|||
coup4 := 1; |
|||
} |
|||
if(draw = 5) { |
|||
coup5 := 1; |
|||
} |
|||
if(draw = 6) { |
|||
coup6 := 1; |
|||
} |
|||
} |
|||
} |
|||
@ -0,0 +1,44 @@ |
|||
function coupon7() { |
|||
int coup0 := 0; |
|||
int coup1 := 0; |
|||
int coup2 := 0; |
|||
int coup3 := 0; |
|||
int coup4 := 0; |
|||
int coup5 := 0; |
|||
int coup6 := 0; |
|||
|
|||
int draw1 := 0; |
|||
int draw2 := 0; |
|||
int draw3 := 0; |
|||
|
|||
int cost := 1; |
|||
|
|||
while (!(coup0 = 1) | !(coup1 = 1) | !(coup2 = 1) | !(coup3 = 1) | !(coup4 = 1) | !(coup5= 1) | !(coup6 = 1)) { |
|||
draw1 := unif(0,6); |
|||
draw2 := unif(0,6); |
|||
draw3 := unif(0,6); |
|||
cost := ceil(1.02 * cost); |
|||
|
|||
if(draw1 = 0 | draw2 = 0 | draw3 = 0) { |
|||
coup0 := 1; |
|||
} |
|||
if(draw1 = 1 | draw2 = 1 | draw3 = 1) { |
|||
coup1 := 1; |
|||
} |
|||
if(draw1 = 2 | draw2 = 2 | draw3 = 2) { |
|||
coup2 := 1; |
|||
} |
|||
if (draw1 = 3 | draw2 = 3 | draw3 = 3) { |
|||
coup3 := 1; |
|||
} |
|||
if (draw1 = 4 | draw2 = 4 | draw3 = 4) { |
|||
coup4 := 1; |
|||
} |
|||
if (draw1 = 5 | draw2 = 5 | draw3 = 5) { |
|||
coup5 := 1; |
|||
} |
|||
if (draw1 = 6 | draw2 = 6 | draw3 = 6) { |
|||
coup6 := 1; |
|||
} |
|||
} |
|||
} |
|||
@ -0,0 +1,46 @@ |
|||
function coupon7() { |
|||
int coup0 := 0; |
|||
int coup1 := 0; |
|||
int coup2 := 0; |
|||
int coup3 := 0; |
|||
int coup4 := 0; |
|||
int coup5 := 0; |
|||
int coup6 := 0; |
|||
|
|||
int draw1 := 0; |
|||
int draw2 := 0; |
|||
int draw3 := 0; |
|||
|
|||
int numberDraws := 0; |
|||
|
|||
while (!(coup0 = 1) | !(coup1 = 1) | !(coup2 = 1) | !(coup3 = 1) | !(coup4 = 1) | !(coup5= 1) | !(coup6 = 1)) { |
|||
draw1 := unif(0,6); |
|||
draw2 := unif(0,6); |
|||
draw3 := unif(0,6); |
|||
numberDraws := numberDraws + 1; |
|||
|
|||
observe (draw1 != draw2 & draw1 != draw3 & draw2 != draw3); |
|||
|
|||
if(draw1 = 0 | draw2 = 0 | draw3 = 0) { |
|||
coup0 := 1; |
|||
} |
|||
if(draw1 = 1 | draw2 = 1 | draw3 = 1) { |
|||
coup1 := 1; |
|||
} |
|||
if(draw1 = 2 | draw2 = 2 | draw3 = 2) { |
|||
coup2 := 1; |
|||
} |
|||
if (draw1 = 3 | draw2 = 3 | draw3 = 3) { |
|||
coup3 := 1; |
|||
} |
|||
if (draw1 = 4 | draw2 = 4 | draw3 = 4) { |
|||
coup4 := 1; |
|||
} |
|||
if (draw1 = 5 | draw2 = 5 | draw3 = 5) { |
|||
coup5 := 1; |
|||
} |
|||
if (draw1 = 6 | draw2 = 6 | draw3 = 6) { |
|||
coup6 := 1; |
|||
} |
|||
} |
|||
} |
|||
@ -0,0 +1,44 @@ |
|||
function coupon7() { |
|||
int coup0 := 0; |
|||
int coup1 := 0; |
|||
int coup2 := 0; |
|||
int coup3 := 0; |
|||
int coup4 := 0; |
|||
int coup5 := 0; |
|||
int coup6 := 0; |
|||
|
|||
int draw1 := 0; |
|||
int draw2 := 0; |
|||
int draw3 := 0; |
|||
|
|||
int numberDraws := 0; |
|||
|
|||
while (!(coup0 = 1) | !(coup1 = 1) | !(coup2 = 1) | !(coup3 = 1) | !(coup4 = 1) | !(coup5= 1) | !(coup6 = 1)) { |
|||
draw1 := unif(0,6); |
|||
draw2 := unif(0,6); |
|||
draw3 := unif(0,6); |
|||
numberDraws := numberDraws + 1; |
|||
|
|||
if(draw1 = 0 | draw2 = 0 | draw3 = 0) { |
|||
coup0 := 1; |
|||
} |
|||
if(draw1 = 1 | draw2 = 1 | draw3 = 1) { |
|||
coup1 := 1; |
|||
} |
|||
if(draw1 = 2 | draw2 = 2 | draw3 = 2) { |
|||
coup2 := 1; |
|||
} |
|||
if (draw1 = 3 | draw2 = 3 | draw3 = 3) { |
|||
coup3 := 1; |
|||
} |
|||
if (draw1 = 4 | draw2 = 4 | draw3 = 4) { |
|||
coup4 := 1; |
|||
} |
|||
if (draw1 = 5 | draw2 = 5 | draw3 = 5) { |
|||
coup5 := 1; |
|||
} |
|||
if (draw1 = 6 | draw2 = 6 | draw3 = 6) { |
|||
coup6 := 1; |
|||
} |
|||
} |
|||
} |
|||
@ -0,0 +1,35 @@ |
|||
function crowds() { |
|||
int delivered := 0; |
|||
int lastSender := 0; |
|||
int remainingRuns := 100; |
|||
int observeSender := 0; |
|||
int observeOther := 0; |
|||
|
|||
while(remainingRuns > 0) { |
|||
while(delivered = 0) { |
|||
{ |
|||
if(lastSender = 0) { |
|||
observeSender := observeSender + 1; |
|||
} else { |
|||
observeOther := observeOther + 1; |
|||
} |
|||
lastSender := 0; |
|||
delivered := 1; |
|||
} [0.091] { |
|||
{ |
|||
{ lastSender:=0; } [1/100] { lastSender := 1; } |
|||
} |
|||
[0.8] |
|||
{ |
|||
lastSender := 0; |
|||
// When not forwarding, the message is delivered here. |
|||
delivered := 1; |
|||
} |
|||
} |
|||
} |
|||
delivered := 0; |
|||
// Set up new run. |
|||
remainingRuns := remainingRuns - 1; |
|||
} |
|||
observe(observeOther > 25); |
|||
} |
|||
@ -0,0 +1,34 @@ |
|||
function crowds() { |
|||
int delivered := 0; |
|||
int lastSender := 0; |
|||
int remainingRuns := 100; |
|||
int observeSender := 0; |
|||
int observeOther := 0; |
|||
|
|||
while(remainingRuns > 0) { |
|||
while(delivered = 0) { |
|||
{ |
|||
if(lastSender = 0) { |
|||
observeSender := observeSender + 1; |
|||
} else { |
|||
observeOther := observeOther + 1; |
|||
} |
|||
lastSender := 0; |
|||
delivered := 1; |
|||
} [0.091] { |
|||
{ |
|||
{ lastSender:=0; } [1/100] { lastSender := 1; } |
|||
} |
|||
[0.8] |
|||
{ |
|||
lastSender := 0; |
|||
// When not forwarding, the message is delivered here. |
|||
delivered := 1; |
|||
} |
|||
} |
|||
} |
|||
delivered := 0; |
|||
// Set up new run. |
|||
remainingRuns := remainingRuns - 1; |
|||
} |
|||
} |
|||
@ -0,0 +1,35 @@ |
|||
function crowds() { |
|||
int delivered := 0; |
|||
int lastSender := 0; |
|||
int remainingRuns := 60; |
|||
int observeSender := 0; |
|||
int observeOther := 0; |
|||
|
|||
while(remainingRuns > 0) { |
|||
while(delivered = 0) { |
|||
{ |
|||
if(lastSender = 0) { |
|||
observeSender := observeSender + 1; |
|||
} else { |
|||
observeOther := observeOther + 1; |
|||
} |
|||
lastSender := 0; |
|||
delivered := 1; |
|||
} [0.091] { |
|||
{ |
|||
{ lastSender:=0; } [1/100] { lastSender := 1; } |
|||
} |
|||
[0.8] |
|||
{ |
|||
lastSender := 0; |
|||
// When not forwarding, the message is delivered here. |
|||
delivered := 1; |
|||
} |
|||
} |
|||
} |
|||
delivered := 0; |
|||
// Set up new run. |
|||
remainingRuns := remainingRuns - 1; |
|||
} |
|||
observe(observeOther > 15); |
|||
} |
|||
@ -0,0 +1,34 @@ |
|||
function crowds(double PF, double bad) { |
|||
int delivered := 0; |
|||
int lastSender := 0; |
|||
int remainingRuns := 60; |
|||
int observeSender := 0; // in [0, TotalRuns] |
|||
int observeOther := 0; // in [0, TotalRuns] |
|||
|
|||
while(remainingRuns > 0) { |
|||
while(delivered = 0) { |
|||
{ |
|||
if(lastSender = 0) { |
|||
observeSender := observeSender + 1; |
|||
} else { |
|||
observeOther := observeOther + 1; |
|||
} |
|||
lastSender := 0; |
|||
delivered := 1; |
|||
} [bad] { |
|||
{ |
|||
{ lastSender:=0; } [1/100] { lastSender := 1; } |
|||
} |
|||
[PF] |
|||
{ |
|||
lastSender := 0; |
|||
// When not forwarding, the message is delivered here. |
|||
delivered := 1; |
|||
} |
|||
} |
|||
} |
|||
delivered := 0; |
|||
// Set up new run. |
|||
remainingRuns := remainingRuns - 1; |
|||
} |
|||
} |
|||
@ -0,0 +1,34 @@ |
|||
function crowds() { |
|||
int delivered := 0; |
|||
int lastSender := 0; |
|||
int remainingRuns := 60; |
|||
int observeSender := 0; |
|||
int observeOther := 0; |
|||
|
|||
while(remainingRuns > 0) { |
|||
while(delivered = 0) { |
|||
{ |
|||
if(lastSender = 0) { |
|||
observeSender := observeSender + 1; |
|||
} else { |
|||
observeOther := observeOther + 1; |
|||
} |
|||
lastSender := 0; |
|||
delivered := 1; |
|||
} [0.091] { |
|||
{ |
|||
{ lastSender:=0; } [1/100] { lastSender := 1; } |
|||
} |
|||
[0.8] |
|||
{ |
|||
lastSender := 0; |
|||
// When not forwarding, the message is delivered here. |
|||
delivered := 1; |
|||
} |
|||
} |
|||
} |
|||
delivered := 0; |
|||
// Set up new run. |
|||
remainingRuns := remainingRuns - 1; |
|||
} |
|||
} |
|||
@ -0,0 +1,36 @@ |
|||
function crowds() { |
|||
int delivered := 0; |
|||
int lastSender := 0; |
|||
int remainingRuns := 80; |
|||
int observeSender := 0; |
|||
int observeOther := 0; |
|||
|
|||
while(remainingRuns > 0) { |
|||
while(delivered = 0) { |
|||
{ |
|||
if(lastSender = 0) { |
|||
observeSender := observeSender + 1; |
|||
} else { |
|||
observeOther := observeOther + 1; |
|||
} |
|||
lastSender := 0; |
|||
delivered := 1; |
|||
} [0.091] { |
|||
{ |
|||
// lastSender := unif(0, 24); |
|||
{ lastSender:=0; } [1/100] { lastSender := 1; } |
|||
} |
|||
[0.8] |
|||
{ |
|||
lastSender := 0; |
|||
// When not forwarding, the message is delivered here. |
|||
delivered := 1; |
|||
} |
|||
} |
|||
} |
|||
delivered := 0; |
|||
// Set up new run. |
|||
remainingRuns := remainingRuns - 1; |
|||
} |
|||
observe(observeOther > 20); |
|||
} |
|||
@ -0,0 +1,34 @@ |
|||
function crowds() { |
|||
int delivered := 0; |
|||
int lastSender := 0; |
|||
int remainingRuns := 80; |
|||
int observeSender := 0; |
|||
int observeOther := 0; |
|||
|
|||
while(remainingRuns > 0) { |
|||
while(delivered = 0) { |
|||
{ |
|||
if(lastSender = 0) { |
|||
observeSender := observeSender + 1; |
|||
} else { |
|||
observeOther := observeOther + 1; |
|||
} |
|||
lastSender := 0; |
|||
delivered := 1; |
|||
} [0.091] { |
|||
{ |
|||
{ lastSender:=0; } [1/100] { lastSender := 1; } |
|||
} |
|||
[0.8] |
|||
{ |
|||
lastSender := 0; |
|||
// When not forwarding, the message is delivered here. |
|||
delivered := 1; |
|||
} |
|||
} |
|||
} |
|||
delivered := 0; |
|||
// Set up new run. |
|||
remainingRuns := remainingRuns - 1; |
|||
} |
|||
} |
|||
@ -0,0 +1,34 @@ |
|||
function crowds(double PF, double bad) { |
|||
int delivered := 0; |
|||
int lastSender := 0; |
|||
int remainingRuns := 3; |
|||
int observeSender := 0; // in [0, TotalRuns] |
|||
int observeOther := 0; // in [0, TotalRuns] |
|||
|
|||
while(remainingRuns > 0) { |
|||
while(delivered = 0) { |
|||
{ |
|||
if(lastSender = 0) { |
|||
observeSender := observeSender + 1; |
|||
} else { |
|||
observeOther := observeOther + 1; |
|||
} |
|||
lastSender := 0; |
|||
delivered := 1; |
|||
} [bad] { |
|||
{ |
|||
{ lastSender:=0; } [1/3] { lastSender := 1; } |
|||
} |
|||
[PF] |
|||
{ |
|||
lastSender := 0; |
|||
// When not forwarding, the message is delivered here. |
|||
delivered := 1; |
|||
} |
|||
} |
|||
} |
|||
delivered := 0; |
|||
// Set up new run. |
|||
remainingRuns := remainingRuns - 1; |
|||
} |
|||
} |
|||
@ -0,0 +1,34 @@ |
|||
function crowds() { |
|||
int delivered := 0; |
|||
int lastSender := 0; |
|||
int remainingRuns := 3; |
|||
int observeSender := 0; |
|||
int observeOther := 0; |
|||
|
|||
while(remainingRuns > 0) { |
|||
while(delivered = 0) { |
|||
{ |
|||
if(lastSender = 0) { |
|||
observeSender := observeSender + 1; |
|||
} else { |
|||
observeOther := observeOther + 1; |
|||
} |
|||
lastSender := 0; |
|||
delivered := 1; |
|||
} [0.091] { |
|||
{ |
|||
{ lastSender:=0; } [1/3] { lastSender := 1; } |
|||
} |
|||
[0.8] |
|||
{ |
|||
lastSender := 0; |
|||
// When not forwarding, the message is delivered here. |
|||
delivered := 1; |
|||
} |
|||
} |
|||
} |
|||
delivered := 0; |
|||
// Set up new run. |
|||
remainingRuns := remainingRuns - 1; |
|||
} |
|||
} |
|||
@ -0,0 +1,33 @@ |
|||
function crowds(double PF, double bad) { |
|||
int delivered := 0; |
|||
int lastSender := 0; |
|||
int remainingRuns := 5; |
|||
int observeSender := 0; |
|||
int observeOther := 0; |
|||
|
|||
while(remainingRuns > 0) { |
|||
while(delivered = 0) { |
|||
{ |
|||
if(lastSender = 0) { |
|||
observeSender := observeSender + 1; |
|||
} else { |
|||
observeOther := observeOther + 1; |
|||
} |
|||
lastSender := 0; |
|||
delivered := 1; |
|||
} [bad] { |
|||
{ lastSender:=0; } [1/3] { lastSender := 1; } |
|||
} |
|||
[PF] |
|||
{ |
|||
lastSender := 0; |
|||
// When not forwarding, the message is delivered here. |
|||
delivered := 1; |
|||
} |
|||
} |
|||
} |
|||
delivered := 0; |
|||
// Set up new run. |
|||
remainingRuns := remainingRuns - 1; |
|||
} |
|||
} |
|||
@ -0,0 +1,34 @@ |
|||
function crowds() { |
|||
int delivered := 0; |
|||
int lastSender := 0; |
|||
int remainingRuns := 5; |
|||
int observeSender := 0; |
|||
int observeOther := 0; |
|||
|
|||
while(remainingRuns > 0) { |
|||
while(delivered = 0) { |
|||
{ |
|||
if(lastSender = 0) { |
|||
observeSender := observeSender + 1; |
|||
} else { |
|||
observeOther := observeOther + 1; |
|||
} |
|||
lastSender := 0; |
|||
delivered := 1; |
|||
} [0.091] { |
|||
{ |
|||
{ lastSender:=0; } [1/3] { lastSender := 1; } |
|||
} |
|||
[0.8] |
|||
{ |
|||
lastSender := 0; |
|||
// When not forwarding, the message is delivered here. |
|||
delivered := 1; |
|||
} |
|||
} |
|||
} |
|||
delivered := 0; |
|||
// Set up new run. |
|||
remainingRuns := remainingRuns - 1; |
|||
} |
|||
} |
|||
@ -0,0 +1,34 @@ |
|||
function crowds(double PF, double bad) { |
|||
int delivered := 0; |
|||
int lastSender := 0; |
|||
int remainingRuns := 20; |
|||
int observeSender := 0; |
|||
int observeOther := 0; |
|||
|
|||
while(remainingRuns > 0) { |
|||
while(delivered = 0) { |
|||
{ |
|||
if(lastSender = 0) { |
|||
observeSender := observeSender + 1; |
|||
} else { |
|||
observeOther := observeOther + 1; |
|||
} |
|||
lastSender := 0; |
|||
delivered := 1; |
|||
} [bad] { |
|||
{ |
|||
{ lastSender:=0; } [1/5] { lastSender := 1; } |
|||
} |
|||
[PF] |
|||
{ |
|||
lastSender := 0; |
|||
// When not forwarding, the message is delivered here. |
|||
delivered := 1; |
|||
} |
|||
} |
|||
} |
|||
// Set up new run. |
|||
delivered := 0; |
|||
remainingRuns := remainingRuns - 1; |
|||
} |
|||
} |
|||
@ -0,0 +1,34 @@ |
|||
function crowds() { |
|||
int delivered := 0; |
|||
int lastSender := 0; |
|||
int remainingRuns := 20; |
|||
int observeSender := 0; |
|||
int observeOther := 0; |
|||
|
|||
while(remainingRuns > 0) { |
|||
while(delivered = 0) { |
|||
{ |
|||
if(lastSender = 0) { |
|||
observeSender := observeSender + 1; |
|||
} else { |
|||
observeOther := observeOther + 1; |
|||
} |
|||
lastSender := 0; |
|||
delivered := 1; |
|||
} [0.091] { |
|||
{ |
|||
{ lastSender:=0; } [1/5] { lastSender := 1; } |
|||
} |
|||
[0.8] |
|||
{ |
|||
lastSender := 0; |
|||
// When not forwarding, the message is delivered here. |
|||
delivered := 1; |
|||
} |
|||
} |
|||
} |
|||
delivered := 0; |
|||
// Set up new run. |
|||
remainingRuns := remainingRuns - 1; |
|||
} |
|||
} |
|||
@ -0,0 +1,108 @@ |
|||
function herman() { |
|||
int x1 := 0; |
|||
int x2 := 0; |
|||
int x3 := 0; |
|||
int x4 := 0; |
|||
int x5 := 0; |
|||
int x6 := 0; |
|||
int x7 := 0; |
|||
int x8 := 0; |
|||
int x9 := 0; |
|||
int x10 := 0; |
|||
int oldx1 := 0; |
|||
int oldx2 := 0; |
|||
int oldx3 := 0; |
|||
int oldx4 := 0; |
|||
int oldx5 := 0; |
|||
int oldx6 := 0; |
|||
int oldx7 := 0; |
|||
int oldx8 := 0; |
|||
int oldx9 := 0; |
|||
int oldx10 := 0; |
|||
|
|||
// determine starting token setup on the ring. |
|||
{x1 := 0;} [0.5] {x1 := 1;} |
|||
{x2 := 0;} [0.5] {x2 := 1;} |
|||
{x3 := 0;} [0.5] {x3 := 1;} |
|||
{x4 := 0;} [0.5] {x4 := 1;} |
|||
{x5 := 0;} [0.5] {x5 := 1;} |
|||
{x6 := 0;} [0.5] {x6 := 1;} |
|||
{x7 := 0;} [0.5] {x7 := 1;} |
|||
{x8 := 0;} [0.5] {x8 := 1;} |
|||
{x9 := 0;} [0.5] {x9 := 1;} |
|||
{x10 := 0;} [0.5] {x10 := 1;} |
|||
|
|||
// finds a ring configuration with exactly one token in the ring. |
|||
while((x1 + x2 + x3 + x4 + x5 + x6 + x7 + x8 + x9 + x10) != 1) { |
|||
oldx1 := x1; |
|||
oldx2 := x2; |
|||
oldx3 := x3; |
|||
oldx4 := x4; |
|||
oldx5 := x5; |
|||
oldx6 := x6; |
|||
oldx7 := x7; |
|||
oldx8 := x8; |
|||
oldx9 := x9; |
|||
oldx10 := x10; |
|||
if(x1 = oldx10) { |
|||
{x1 := 0;} [0.5] {x1 := 1;} |
|||
} else { |
|||
x1 := oldx10; |
|||
} |
|||
oldx10 := 0; |
|||
if(x2 = oldx1) { |
|||
{x2 := 0;} [0.5] {x2 := 1;} |
|||
} else { |
|||
x2 := oldx1; |
|||
} |
|||
oldx1 := 0; |
|||
if(x3 = oldx2) { |
|||
{x3 := 0;} [0.5] {x3 := 1;} |
|||
} else { |
|||
x3 := oldx2; |
|||
} |
|||
oldx2 := 0; |
|||
if(x4 = oldx3) { |
|||
{x4 := 0;} [0.5] {x4 := 1;} |
|||
} else { |
|||
x4 := oldx3; |
|||
} |
|||
oldx3 := 0; |
|||
if(x5 = oldx4) { |
|||
{x5 := 0;} [0.5] {x5 := 1;} |
|||
} else { |
|||
x5 := oldx4; |
|||
} |
|||
oldx4 := 0; |
|||
if(x6 = oldx5) { |
|||
{x6 := 0;} [0.5] {x6 := 1;} |
|||
} else { |
|||
x6 := oldx5; |
|||
} |
|||
oldx5 := 0; |
|||
if(x7 = oldx6) { |
|||
{x7 := 0;} [0.5] {x7 := 1;} |
|||
} else { |
|||
x7 := oldx6; |
|||
} |
|||
oldx6 := 0; |
|||
if(x8 = oldx7) { |
|||
{x7 := 0;} [0.5] {x7 := 1;} |
|||
} else { |
|||
x8 := oldx7; |
|||
} |
|||
oldx7 := 0; |
|||
if(x9 = oldx8) { |
|||
{x9 := 0;} [0.5] {x9 := 1;} |
|||
} else { |
|||
x9 := oldx8; |
|||
} |
|||
oldx8 := 0; |
|||
if(x10 = oldx9) { |
|||
{x10 := 0;} [0.5] {x10 := 1;} |
|||
} else { |
|||
x10 := oldx9; |
|||
} |
|||
oldx9 := 0; |
|||
} |
|||
} |
|||
@ -0,0 +1,108 @@ |
|||
function herman() { |
|||
int x1 := 0; |
|||
int x2 := 0; |
|||
int x3 := 0; |
|||
int x4 := 0; |
|||
int x5 := 0; |
|||
int x6 := 0; |
|||
int x7 := 0; |
|||
int x8 := 0; |
|||
int x9 := 0; |
|||
int x10 := 0; |
|||
int oldx1 := 0; |
|||
int oldx2 := 0; |
|||
int oldx3 := 0; |
|||
int oldx4 := 0; |
|||
int oldx5 := 0; |
|||
int oldx6 := 0; |
|||
int oldx7 := 0; |
|||
int oldx8 := 0; |
|||
int oldx9 := 0; |
|||
int oldx10 := 0; |
|||
|
|||
// determine starting token setup on the ring. |
|||
{x1 := 0;} [] {x1 := 1;} |
|||
{x2 := 0;} [] {x2 := 1;} |
|||
{x3 := 0;} [] {x3 := 1;} |
|||
{x4 := 0;} [] {x4 := 1;} |
|||
{x5 := 0;} [] {x5 := 1;} |
|||
{x6 := 0;} [] {x6 := 1;} |
|||
{x7 := 0;} [] {x7 := 1;} |
|||
{x8 := 0;} [] {x8 := 1;} |
|||
{x9 := 0;} [] {x9 := 1;} |
|||
{x10 := 0;} [] {x10 := 1;} |
|||
|
|||
// finds a ring configuration with exactly one token in the ring. |
|||
while((x1 + x2 + x3 + x4 + x5 + x6 + x7 + x8 + x9 + x10) != 1) { |
|||
oldx1 := x1; |
|||
oldx2 := x2; |
|||
oldx3 := x3; |
|||
oldx4 := x4; |
|||
oldx5 := x5; |
|||
oldx6 := x6; |
|||
oldx7 := x7; |
|||
oldx8 := x8; |
|||
oldx9 := x9; |
|||
oldx10 := x10; |
|||
if(x1 = oldx10) { |
|||
{x1 := 0;} [0.5] {x1 := 1;} |
|||
} else { |
|||
x1 := oldx10; |
|||
} |
|||
oldx10 := 0; |
|||
if(x2 = oldx1) { |
|||
{x2 := 0;} [0.5] {x2 := 1;} |
|||
} else { |
|||
x2 := oldx1; |
|||
} |
|||
oldx1 := 0; |
|||
if(x3 = oldx2) { |
|||
{x3 := 0;} [0.5] {x3 := 1;} |
|||
} else { |
|||
x3 := oldx2; |
|||
} |
|||
oldx2 := 0; |
|||
if(x4 = oldx3) { |
|||
{x4 := 0;} [0.5] {x4 := 1;} |
|||
} else { |
|||
x4 := oldx3; |
|||
} |
|||
oldx3 := 0; |
|||
if(x5 = oldx4) { |
|||
{x5 := 0;} [0.5] {x5 := 1;} |
|||
} else { |
|||
x5 := oldx4; |
|||
} |
|||
oldx4 := 0; |
|||
if(x6 = oldx5) { |
|||
{x6 := 0;} [0.5] {x6 := 1;} |
|||
} else { |
|||
x6 := oldx5; |
|||
} |
|||
oldx5 := 0; |
|||
if(x7 = oldx6) { |
|||
{x7 := 0;} [0.5] {x7 := 1;} |
|||
} else { |
|||
x7 := oldx6; |
|||
} |
|||
oldx6 := 0; |
|||
if(x8 = oldx7) { |
|||
{x7 := 0;} [0.5] {x7 := 1;} |
|||
} else { |
|||
x8 := oldx7; |
|||
} |
|||
oldx7 := 0; |
|||
if(x9 = oldx8) { |
|||
{x9 := 0;} [0.5] {x9 := 1;} |
|||
} else { |
|||
x9 := oldx8; |
|||
} |
|||
oldx8 := 0; |
|||
if(x10 = oldx9) { |
|||
{x10 := 0;} [0.5] {x10 := 1;} |
|||
} else { |
|||
x10 := oldx9; |
|||
} |
|||
oldx9 := 0; |
|||
} |
|||
} |
|||
@ -0,0 +1,138 @@ |
|||
function herman() { |
|||
int x1 := 0; |
|||
int x2 := 0; |
|||
int x3 := 0; |
|||
int x4 := 0; |
|||
int x5 := 0; |
|||
int x6 := 0; |
|||
int x7 := 0; |
|||
int x8 := 0; |
|||
int x9 := 0; |
|||
int x10 := 0; |
|||
int x11 := 0; |
|||
int x12 := 0; |
|||
int x13 := 0; |
|||
int oldx1 := 0; |
|||
int oldx2 := 0; |
|||
int oldx3 := 0; |
|||
int oldx4 := 0; |
|||
int oldx5 := 0; |
|||
int oldx6 := 0; |
|||
int oldx7 := 0; |
|||
int oldx8 := 0; |
|||
int oldx9 := 0; |
|||
int oldx10 := 0; |
|||
int oldx11 := 0; |
|||
int oldx12 := 0; |
|||
int oldx13 := 0; |
|||
|
|||
// determine starting token setup on the ring. |
|||
{x1 := 0;} [0.5] {x1 := 1;} |
|||
{x2 := 0;} [0.5] {x2 := 1;} |
|||
{x3 := 0;} [0.5] {x3 := 1;} |
|||
{x4 := 0;} [0.5] {x4 := 1;} |
|||
{x5 := 0;} [0.5] {x5 := 1;} |
|||
{x6 := 0;} [0.5] {x6 := 1;} |
|||
{x7 := 0;} [0.5] {x7 := 1;} |
|||
{x8 := 0;} [0.5] {x8 := 1;} |
|||
{x9 := 0;} [0.5] {x9 := 1;} |
|||
{x10 := 0;} [0.5] {x10 := 1;} |
|||
{x11 := 0;} [0.5] {x11 := 1;} |
|||
{x12 := 0;} [0.5] {x12 := 1;} |
|||
{x13 := 0;} [0.5] {x13 := 1;} |
|||
|
|||
// finds a ring configuration with exactly one token in the ring. |
|||
while((x1 + x2 + x3 + x4 + x5 + x6 + x7 + x8 + x9 + x10 + x11 + x12 + x13) != 1) { |
|||
oldx1 := x1; |
|||
oldx2 := x2; |
|||
oldx3 := x3; |
|||
oldx4 := x4; |
|||
oldx5 := x5; |
|||
oldx6 := x6; |
|||
oldx7 := x7; |
|||
oldx8 := x8; |
|||
oldx9 := x9; |
|||
oldx10 := x10; |
|||
oldx11 := x11; |
|||
oldx12 := x12; |
|||
oldx13 := x13; |
|||
if(x1 = oldx13) { |
|||
{x1 := 0;} [0.5] {x1 := 1;} |
|||
} else { |
|||
x1 := oldx13; |
|||
} |
|||
oldx13 := 0; |
|||
if(x2 = oldx1) { |
|||
{x2 := 0;} [0.5] {x2 := 1;} |
|||
} else { |
|||
x2 := oldx1; |
|||
} |
|||
oldx1 := 0; |
|||
if(x3 = oldx2) { |
|||
{x3 := 0;} [0.5] {x3 := 1;} |
|||
} else { |
|||
x3 := oldx2; |
|||
} |
|||
oldx2 := 0; |
|||
if(x4 = oldx3) { |
|||
{x4 := 0;} [0.5] {x4 := 1;} |
|||
} else { |
|||
x4 := oldx3; |
|||
} |
|||
oldx3 := 0; |
|||
if(x5 = oldx4) { |
|||
{x5 := 0;} [0.5] {x5 := 1;} |
|||
} else { |
|||
x5 := oldx4; |
|||
} |
|||
oldx4 := 0; |
|||
if(x6 = oldx5) { |
|||
{x6 := 0;} [0.5] {x6 := 1;} |
|||
} else { |
|||
x6 := oldx5; |
|||
} |
|||
oldx5 := 0; |
|||
if(x7 = oldx6) { |
|||
{x7 := 0;} [0.5] {x7 := 1;} |
|||
} else { |
|||
x7 := oldx6; |
|||
} |
|||
oldx6 := 0; |
|||
if(x8 = oldx7) { |
|||
{x7 := 0;} [0.5] {x7 := 1;} |
|||
} else { |
|||
x8 := oldx7; |
|||
} |
|||
oldx7 := 0; |
|||
if(x9 = oldx8) { |
|||
{x9 := 0;} [0.5] {x9 := 1;} |
|||
} else { |
|||
x9 := oldx8; |
|||
} |
|||
oldx8 := 0; |
|||
if(x10 = oldx9) { |
|||
{x10 := 0;} [0.5] {x10 := 1;} |
|||
} else { |
|||
x10 := oldx9; |
|||
} |
|||
oldx9 := 0; |
|||
if(x11 = oldx10) { |
|||
{x11 := 0;} [0.5] {x11 := 1;} |
|||
} else { |
|||
x11 := oldx10; |
|||
} |
|||
oldx10 := 0; |
|||
if(x12 = oldx11) { |
|||
{x12 := 0;} [0.5] {x12 := 1;} |
|||
} else { |
|||
x12 := oldx11; |
|||
} |
|||
oldx11 := 0; |
|||
if(x13 = oldx12) { |
|||
{x13 := 0;} [0.5] {x13 := 1;} |
|||
} else { |
|||
x13 := oldx12; |
|||
} |
|||
oldx12 := 0; |
|||
} |
|||
} |
|||
@ -0,0 +1,138 @@ |
|||
function herman() { |
|||
int x1 := 0; |
|||
int x2 := 0; |
|||
int x3 := 0; |
|||
int x4 := 0; |
|||
int x5 := 0; |
|||
int x6 := 0; |
|||
int x7 := 0; |
|||
int x8 := 0; |
|||
int x9 := 0; |
|||
int x10 := 0; |
|||
int x11 := 0; |
|||
int x12 := 0; |
|||
int x13 := 0; |
|||
int oldx1 := 0; |
|||
int oldx2 := 0; |
|||
int oldx3 := 0; |
|||
int oldx4 := 0; |
|||
int oldx5 := 0; |
|||
int oldx6 := 0; |
|||
int oldx7 := 0; |
|||
int oldx8 := 0; |
|||
int oldx9 := 0; |
|||
int oldx10 := 0; |
|||
int oldx11 := 0; |
|||
int oldx12 := 0; |
|||
int oldx13 := 0; |
|||
|
|||
// determine starting token setup on the ring. |
|||
{x1 := 0;} [] {x1 := 1;} |
|||
{x2 := 0;} [] {x2 := 1;} |
|||
{x3 := 0;} [] {x3 := 1;} |
|||
{x4 := 0;} [] {x4 := 1;} |
|||
{x5 := 0;} [] {x5 := 1;} |
|||
{x6 := 0;} [] {x6 := 1;} |
|||
{x7 := 0;} [] {x7 := 1;} |
|||
{x8 := 0;} [] {x8 := 1;} |
|||
{x9 := 0;} [] {x9 := 1;} |
|||
{x10 := 0;} [] {x10 := 1;} |
|||
{x11 := 0;} [] {x11 := 1;} |
|||
{x12 := 0;} [] {x12 := 1;} |
|||
{x13 := 0;} [] {x13 := 1;} |
|||
|
|||
// finds a ring configuration with exactly one token in the ring. |
|||
while((x1 + x2 + x3 + x4 + x5 + x6 + x7 + x8 + x9 + x10 + x11 + x12 + x13) != 1) { |
|||
oldx1 := x1; |
|||
oldx2 := x2; |
|||
oldx3 := x3; |
|||
oldx4 := x4; |
|||
oldx5 := x5; |
|||
oldx6 := x6; |
|||
oldx7 := x7; |
|||
oldx8 := x8; |
|||
oldx9 := x9; |
|||
oldx10 := x10; |
|||
oldx11 := x11; |
|||
oldx12 := x12; |
|||
oldx13 := x13; |
|||
if(x1 = oldx13) { |
|||
{x1 := 0;} [0.5] {x1 := 1;} |
|||
} else { |
|||
x1 := oldx13; |
|||
} |
|||
oldx13 := 0; |
|||
if(x2 = oldx1) { |
|||
{x2 := 0;} [0.5] {x2 := 1;} |
|||
} else { |
|||
x2 := oldx1; |
|||
} |
|||
oldx1 := 0; |
|||
if(x3 = oldx2) { |
|||
{x3 := 0;} [0.5] {x3 := 1;} |
|||
} else { |
|||
x3 := oldx2; |
|||
} |
|||
oldx2 := 0; |
|||
if(x4 = oldx3) { |
|||
{x4 := 0;} [0.5] {x4 := 1;} |
|||
} else { |
|||
x4 := oldx3; |
|||
} |
|||
oldx3 := 0; |
|||
if(x5 = oldx4) { |
|||
{x5 := 0;} [0.5] {x5 := 1;} |
|||
} else { |
|||
x5 := oldx4; |
|||
} |
|||
oldx4 := 0; |
|||
if(x6 = oldx5) { |
|||
{x6 := 0;} [0.5] {x6 := 1;} |
|||
} else { |
|||
x6 := oldx5; |
|||
} |
|||
oldx5 := 0; |
|||
if(x7 = oldx6) { |
|||
{x7 := 0;} [0.5] {x7 := 1;} |
|||
} else { |
|||
x7 := oldx6; |
|||
} |
|||
oldx6 := 0; |
|||
if(x8 = oldx7) { |
|||
{x7 := 0;} [0.5] {x7 := 1;} |
|||
} else { |
|||
x8 := oldx7; |
|||
} |
|||
oldx7 := 0; |
|||
if(x9 = oldx8) { |
|||
{x9 := 0;} [0.5] {x9 := 1;} |
|||
} else { |
|||
x9 := oldx8; |
|||
} |
|||
oldx8 := 0; |
|||
if(x10 = oldx9) { |
|||
{x10 := 0;} [0.5] {x10 := 1;} |
|||
} else { |
|||
x10 := oldx9; |
|||
} |
|||
oldx9 := 0; |
|||
if(x11 = oldx10) { |
|||
{x11 := 0;} [0.5] {x11 := 1;} |
|||
} else { |
|||
x11 := oldx10; |
|||
} |
|||
oldx10 := 0; |
|||
if(x12 = oldx11) { |
|||
{x12 := 0;} [0.5] {x12 := 1;} |
|||
} else { |
|||
x12 := oldx11; |
|||
} |
|||
oldx11 := 0; |
|||
if(x13 = oldx12) { |
|||
{x13 := 0;} [0.5] {x13 := 1;} |
|||
} else { |
|||
x13 := oldx12; |
|||
} |
|||
oldx12 := 0; |
|||
} |
|||
} |
|||
@ -0,0 +1,178 @@ |
|||
function herman() { |
|||
int x1 := 0; |
|||
int x2 := 0; |
|||
int x3 := 0; |
|||
int x4 := 0; |
|||
int x5 := 0; |
|||
int x6 := 0; |
|||
int x7 := 0; |
|||
int x8 := 0; |
|||
int x9 := 0; |
|||
int x10 := 0; |
|||
int x11 := 0; |
|||
int x12 := 0; |
|||
int x13 := 0; |
|||
int x14 := 0; |
|||
int x15 := 0; |
|||
int x16 := 0; |
|||
int x17 := 0; |
|||
int oldx1 := 0; |
|||
int oldx2 := 0; |
|||
int oldx3 := 0; |
|||
int oldx4 := 0; |
|||
int oldx5 := 0; |
|||
int oldx6 := 0; |
|||
int oldx7 := 0; |
|||
int oldx8 := 0; |
|||
int oldx9 := 0; |
|||
int oldx10 := 0; |
|||
int oldx11 := 0; |
|||
int oldx12 := 0; |
|||
int oldx13 := 0; |
|||
int oldx14 := 0; |
|||
int oldx15 := 0; |
|||
int oldx16 := 0; |
|||
int oldx17 := 0; |
|||
|
|||
// determine starting token setup on the ring. |
|||
{x1 := 0;} [0.5] {x1 := 1;} |
|||
{x2 := 0;} [0.5] {x2 := 1;} |
|||
{x3 := 0;} [0.5] {x3 := 1;} |
|||
{x4 := 0;} [0.5] {x4 := 1;} |
|||
{x5 := 0;} [0.5] {x5 := 1;} |
|||
{x6 := 0;} [0.5] {x6 := 1;} |
|||
{x7 := 0;} [0.5] {x7 := 1;} |
|||
{x8 := 0;} [0.5] {x8 := 1;} |
|||
{x9 := 0;} [0.5] {x9 := 1;} |
|||
{x10 := 0;} [0.5] {x10 := 1;} |
|||
{x11 := 0;} [0.5] {x11 := 1;} |
|||
{x12 := 0;} [0.5] {x12 := 1;} |
|||
{x13 := 0;} [0.5] {x13 := 1;} |
|||
{x14 := 0;} [0.5] {x14 := 1;} |
|||
{x15 := 0;} [0.5] {x15 := 1;} |
|||
{x16 := 0;} [0.5] {x16 := 1;} |
|||
{x17 := 0;} [0.5] {x17 := 1;} |
|||
|
|||
// finds a ring configuration with exactly one token in the ring. |
|||
while((x1 + x2 + x3 + x4 + x5 + x6 + x7 + x8 + x9 + x10 + x11 + x12 + x13 + x14 + x15 + x16 + x17) != 1) { |
|||
oldx1 := x1; |
|||
oldx2 := x2; |
|||
oldx3 := x3; |
|||
oldx4 := x4; |
|||
oldx5 := x5; |
|||
oldx6 := x6; |
|||
oldx7 := x7; |
|||
oldx8 := x8; |
|||
oldx9 := x9; |
|||
oldx10 := x10; |
|||
oldx11 := x11; |
|||
oldx12 := x12; |
|||
oldx13 := x13; |
|||
oldx14 := x14; |
|||
oldx15 := x15; |
|||
oldx16 := x16; |
|||
oldx17 := x17; |
|||
if(x1 = oldx17) { |
|||
{x1 := 0;} [0.5] {x1 := 1;} |
|||
} else { |
|||
x1 := oldx17; |
|||
} |
|||
oldx17 := 0; |
|||
if(x2 = oldx1) { |
|||
{x2 := 0;} [0.5] {x2 := 1;} |
|||
} else { |
|||
x2 := oldx1; |
|||
} |
|||
oldx1 := 0; |
|||
if(x3 = oldx2) { |
|||
{x3 := 0;} [0.5] {x3 := 1;} |
|||
} else { |
|||
x3 := oldx2; |
|||
} |
|||
oldx2 := 0; |
|||
if(x4 = oldx3) { |
|||
{x4 := 0;} [0.5] {x4 := 1;} |
|||
} else { |
|||
x4 := oldx3; |
|||
} |
|||
oldx3 := 0; |
|||
if(x5 = oldx4) { |
|||
{x5 := 0;} [0.5] {x5 := 1;} |
|||
} else { |
|||
x5 := oldx4; |
|||
} |
|||
oldx4 := 0; |
|||
if(x6 = oldx5) { |
|||
{x6 := 0;} [0.5] {x6 := 1;} |
|||
} else { |
|||
x6 := oldx5; |
|||
} |
|||
oldx5 := 0; |
|||
if(x7 = oldx6) { |
|||
{x7 := 0;} [0.5] {x7 := 1;} |
|||
} else { |
|||
x7 := oldx6; |
|||
} |
|||
oldx6 := 0; |
|||
if(x8 = oldx7) { |
|||
{x7 := 0;} [0.5] {x7 := 1;} |
|||
} else { |
|||
x8 := oldx7; |
|||
} |
|||
oldx7 := 0; |
|||
if(x9 = oldx8) { |
|||
{x9 := 0;} [0.5] {x9 := 1;} |
|||
} else { |
|||
x9 := oldx8; |
|||
} |
|||
oldx8 := 0; |
|||
if(x10 = oldx9) { |
|||
{x10 := 0;} [0.5] {x10 := 1;} |
|||
} else { |
|||
x10 := oldx9; |
|||
} |
|||
oldx9 := 0; |
|||
if(x11 = oldx10) { |
|||
{x11 := 0;} [0.5] {x11 := 1;} |
|||
} else { |
|||
x11 := oldx10; |
|||
} |
|||
oldx10 := 0; |
|||
if(x12 = oldx11) { |
|||
{x12 := 0;} [0.5] {x12 := 1;} |
|||
} else { |
|||
x12 := oldx11; |
|||
} |
|||
oldx11 := 0; |
|||
if(x13 = oldx12) { |
|||
{x13 := 0;} [0.5] {x13 := 1;} |
|||
} else { |
|||
x13 := oldx12; |
|||
} |
|||
oldx12 := 0; |
|||
if(x14 = oldx13) { |
|||
{x14 := 0;} [0.5] {x14 := 1;} |
|||
} else { |
|||
x14 := oldx13; |
|||
} |
|||
oldx13 := 0; |
|||
if(x15 = oldx14) { |
|||
{x15 := 0;} [0.5] {x15 := 1;} |
|||
} else { |
|||
x15 := oldx14; |
|||
} |
|||
oldx14 := 0; |
|||
if(x16 = oldx15) { |
|||
{x16 := 0;} [0.5] {x16 := 1;} |
|||
} else { |
|||
x16 := oldx15; |
|||
} |
|||
oldx15 := 0; |
|||
if(x17 = oldx16) { |
|||
{x17 := 0;} [0.5] {x17 := 1;} |
|||
} else { |
|||
x17 := oldx16; |
|||
} |
|||
oldx16 := 0; |
|||
} |
|||
} |
|||
@ -0,0 +1,178 @@ |
|||
function herman() { |
|||
int x1 := 0; |
|||
int x2 := 0; |
|||
int x3 := 0; |
|||
int x4 := 0; |
|||
int x5 := 0; |
|||
int x6 := 0; |
|||
int x7 := 0; |
|||
int x8 := 0; |
|||
int x9 := 0; |
|||
int x10 := 0; |
|||
int x11 := 0; |
|||
int x12 := 0; |
|||
int x13 := 0; |
|||
int x14 := 0; |
|||
int x15 := 0; |
|||
int x16 := 0; |
|||
int x17 := 0; |
|||
int oldx1 := 0; |
|||
int oldx2 := 0; |
|||
int oldx3 := 0; |
|||
int oldx4 := 0; |
|||
int oldx5 := 0; |
|||
int oldx6 := 0; |
|||
int oldx7 := 0; |
|||
int oldx8 := 0; |
|||
int oldx9 := 0; |
|||
int oldx10 := 0; |
|||
int oldx11 := 0; |
|||
int oldx12 := 0; |
|||
int oldx13 := 0; |
|||
int oldx14 := 0; |
|||
int oldx15 := 0; |
|||
int oldx16 := 0; |
|||
int oldx17 := 0; |
|||
|
|||
// determine starting token setup on the ring. |
|||
{x1 := 0;} [] {x1 := 1;} |
|||
{x2 := 0;} [] {x2 := 1;} |
|||
{x3 := 0;} [] {x3 := 1;} |
|||
{x4 := 0;} [] {x4 := 1;} |
|||
{x5 := 0;} [] {x5 := 1;} |
|||
{x6 := 0;} [] {x6 := 1;} |
|||
{x7 := 0;} [] {x7 := 1;} |
|||
{x8 := 0;} [] {x8 := 1;} |
|||
{x9 := 0;} [] {x9 := 1;} |
|||
{x10 := 0;} [] {x10 := 1;} |
|||
{x11 := 0;} [] {x11 := 1;} |
|||
{x12 := 0;} [] {x12 := 1;} |
|||
{x13 := 0;} [] {x13 := 1;} |
|||
{x14 := 0;} [] {x14 := 1;} |
|||
{x15 := 0;} [] {x15 := 1;} |
|||
{x16 := 0;} [] {x16 := 1;} |
|||
{x17 := 0;} [] {x17 := 1;} |
|||
|
|||
// finds a ring configuration with exactly one token in the ring. |
|||
while((x1 + x2 + x3 + x4 + x5 + x6 + x7 + x8 + x9 + x10 + x11 + x12 + x13 + x14 + x15 + x16 + x17) != 1) { |
|||
oldx1 := x1; |
|||
oldx2 := x2; |
|||
oldx3 := x3; |
|||
oldx4 := x4; |
|||
oldx5 := x5; |
|||
oldx6 := x6; |
|||
oldx7 := x7; |
|||
oldx8 := x8; |
|||
oldx9 := x9; |
|||
oldx10 := x10; |
|||
oldx11 := x11; |
|||
oldx12 := x12; |
|||
oldx13 := x13; |
|||
oldx14 := x14; |
|||
oldx15 := x15; |
|||
oldx16 := x16; |
|||
oldx17 := x17; |
|||
if(x1 = oldx17) { |
|||
{x1 := 0;} [0.5] {x1 := 1;} |
|||
} else { |
|||
x1 := oldx17; |
|||
} |
|||
oldx17 := 0; |
|||
if(x2 = oldx1) { |
|||
{x2 := 0;} [0.5] {x2 := 1;} |
|||
} else { |
|||
x2 := oldx1; |
|||
} |
|||
oldx1 := 0; |
|||
if(x3 = oldx2) { |
|||
{x3 := 0;} [0.5] {x3 := 1;} |
|||
} else { |
|||
x3 := oldx2; |
|||
} |
|||
oldx2 := 0; |
|||
if(x4 = oldx3) { |
|||
{x4 := 0;} [0.5] {x4 := 1;} |
|||
} else { |
|||
x4 := oldx3; |
|||
} |
|||
oldx3 := 0; |
|||
if(x5 = oldx4) { |
|||
{x5 := 0;} [0.5] {x5 := 1;} |
|||
} else { |
|||
x5 := oldx4; |
|||
} |
|||
oldx4 := 0; |
|||
if(x6 = oldx5) { |
|||
{x6 := 0;} [0.5] {x6 := 1;} |
|||
} else { |
|||
x6 := oldx5; |
|||
} |
|||
oldx5 := 0; |
|||
if(x7 = oldx6) { |
|||
{x7 := 0;} [0.5] {x7 := 1;} |
|||
} else { |
|||
x7 := oldx6; |
|||
} |
|||
oldx6 := 0; |
|||
if(x8 = oldx7) { |
|||
{x7 := 0;} [0.5] {x7 := 1;} |
|||
} else { |
|||
x8 := oldx7; |
|||
} |
|||
oldx7 := 0; |
|||
if(x9 = oldx8) { |
|||
{x9 := 0;} [0.5] {x9 := 1;} |
|||
} else { |
|||
x9 := oldx8; |
|||
} |
|||
oldx8 := 0; |
|||
if(x10 = oldx9) { |
|||
{x10 := 0;} [0.5] {x10 := 1;} |
|||
} else { |
|||
x10 := oldx9; |
|||
} |
|||
oldx9 := 0; |
|||
if(x11 = oldx10) { |
|||
{x11 := 0;} [0.5] {x11 := 1;} |
|||
} else { |
|||
x11 := oldx10; |
|||
} |
|||
oldx10 := 0; |
|||
if(x12 = oldx11) { |
|||
{x12 := 0;} [0.5] {x12 := 1;} |
|||
} else { |
|||
x12 := oldx11; |
|||
} |
|||
oldx11 := 0; |
|||
if(x13 = oldx12) { |
|||
{x13 := 0;} [0.5] {x13 := 1;} |
|||
} else { |
|||
x13 := oldx12; |
|||
} |
|||
oldx12 := 0; |
|||
if(x14 = oldx13) { |
|||
{x14 := 0;} [0.5] {x14 := 1;} |
|||
} else { |
|||
x14 := oldx13; |
|||
} |
|||
oldx13 := 0; |
|||
if(x15 = oldx14) { |
|||
{x15 := 0;} [0.5] {x15 := 1;} |
|||
} else { |
|||
x15 := oldx14; |
|||
} |
|||
oldx14 := 0; |
|||
if(x16 = oldx15) { |
|||
{x16 := 0;} [0.5] {x16 := 1;} |
|||
} else { |
|||
x16 := oldx15; |
|||
} |
|||
oldx15 := 0; |
|||
if(x17 = oldx16) { |
|||
{x17 := 0;} [0.5] {x17 := 1;} |
|||
} else { |
|||
x17 := oldx16; |
|||
} |
|||
oldx16 := 0; |
|||
} |
|||
} |
|||
@ -0,0 +1,218 @@ |
|||
function herman() { |
|||
int x1 := 0; |
|||
int x2 := 0; |
|||
int x3 := 0; |
|||
int x4 := 0; |
|||
int x5 := 0; |
|||
int x6 := 0; |
|||
int x7 := 0; |
|||
int x8 := 0; |
|||
int x9 := 0; |
|||
int x10 := 0; |
|||
int x11 := 0; |
|||
int x12 := 0; |
|||
int x13 := 0; |
|||
int x14 := 0; |
|||
int x15 := 0; |
|||
int x16 := 0; |
|||
int x17 := 0; |
|||
int x18 := 0; |
|||
int x19 := 0; |
|||
int x20 := 0; |
|||
int x21 := 0; |
|||
int oldx1 := 0; |
|||
int oldx2 := 0; |
|||
int oldx3 := 0; |
|||
int oldx4 := 0; |
|||
int oldx5 := 0; |
|||
int oldx6 := 0; |
|||
int oldx7 := 0; |
|||
int oldx8 := 0; |
|||
int oldx9 := 0; |
|||
int oldx10 := 0; |
|||
int oldx11 := 0; |
|||
int oldx12 := 0; |
|||
int oldx13 := 0; |
|||
int oldx14 := 0; |
|||
int oldx15 := 0; |
|||
int oldx16 := 0; |
|||
int oldx17 := 0; |
|||
int oldx18 := 0; |
|||
int oldx19 := 0; |
|||
int oldx20 := 0; |
|||
int oldx21 := 0; |
|||
|
|||
// determine starting token setup on the ring. |
|||
{x1 := 0;} [0.5] {x1 := 1;} |
|||
{x2 := 0;} [0.5] {x2 := 1;} |
|||
{x3 := 0;} [0.5] {x3 := 1;} |
|||
{x4 := 0;} [0.5] {x4 := 1;} |
|||
{x5 := 0;} [0.5] {x5 := 1;} |
|||
{x6 := 0;} [0.5] {x6 := 1;} |
|||
{x7 := 0;} [0.5] {x7 := 1;} |
|||
{x8 := 0;} [0.5] {x8 := 1;} |
|||
{x9 := 0;} [0.5] {x9 := 1;} |
|||
{x10 := 0;} [0.5] {x10 := 1;} |
|||
{x11 := 0;} [0.5] {x11 := 1;} |
|||
{x12 := 0;} [0.5] {x12 := 1;} |
|||
{x13 := 0;} [0.5] {x13 := 1;} |
|||
{x14 := 0;} [0.5] {x14 := 1;} |
|||
{x15 := 0;} [0.5] {x15 := 1;} |
|||
{x16 := 0;} [0.5] {x16 := 1;} |
|||
{x17 := 0;} [0.5] {x17 := 1;} |
|||
{x18 := 0;} [0.5] {x18 := 1;} |
|||
{x19 := 0;} [0.5] {x19 := 1;} |
|||
{x20 := 0;} [0.5] {x20 := 1;} |
|||
{x21 := 0;} [0.5] {x21 := 1;} |
|||
|
|||
// finds a ring configuration with exactly one token in the ring. |
|||
while((x1 + x2 + x3 + x4 + x5 + x6 + x7 + x8 + x9 + x10 + x11 + x12 + x13 + x14 + x15 + x16 + x17 + x18 + x19 + x20 + x21) != 1) { |
|||
oldx1 := x1; |
|||
oldx2 := x2; |
|||
oldx3 := x3; |
|||
oldx4 := x4; |
|||
oldx5 := x5; |
|||
oldx6 := x6; |
|||
oldx7 := x7; |
|||
oldx8 := x8; |
|||
oldx9 := x9; |
|||
oldx10 := x10; |
|||
oldx11 := x11; |
|||
oldx12 := x12; |
|||
oldx13 := x13; |
|||
oldx14 := x14; |
|||
oldx15 := x15; |
|||
oldx16 := x16; |
|||
oldx17 := x17; |
|||
oldx18 := x18; |
|||
oldx19 := x19; |
|||
oldx20 := x20; |
|||
oldx21 := x21; |
|||
if(x1 = oldx21) { |
|||
{x1 := 0;} [0.5] {x1 := 1;} |
|||
} else { |
|||
x1 := oldx21; |
|||
} |
|||
oldx21 := 0; |
|||
if(x2 = oldx1) { |
|||
{x2 := 0;} [0.5] {x2 := 1;} |
|||
} else { |
|||
x2 := oldx1; |
|||
} |
|||
oldx1 := 0; |
|||
if(x3 = oldx2) { |
|||
{x3 := 0;} [0.5] {x3 := 1;} |
|||
} else { |
|||
x3 := oldx2; |
|||
} |
|||
oldx2 := 0; |
|||
if(x4 = oldx3) { |
|||
{x4 := 0;} [0.5] {x4 := 1;} |
|||
} else { |
|||
x4 := oldx3; |
|||
} |
|||
oldx3 := 0; |
|||
if(x5 = oldx4) { |
|||
{x5 := 0;} [0.5] {x5 := 1;} |
|||
} else { |
|||
x5 := oldx4; |
|||
} |
|||
oldx4 := 0; |
|||
if(x6 = oldx5) { |
|||
{x6 := 0;} [0.5] {x6 := 1;} |
|||
} else { |
|||
x6 := oldx5; |
|||
} |
|||
oldx5 := 0; |
|||
if(x7 = oldx6) { |
|||
{x7 := 0;} [0.5] {x7 := 1;} |
|||
} else { |
|||
x7 := oldx6; |
|||
} |
|||
oldx6 := 0; |
|||
if(x8 = oldx7) { |
|||
{x7 := 0;} [0.5] {x7 := 1;} |
|||
} else { |
|||
x8 := oldx7; |
|||
} |
|||
oldx7 := 0; |
|||
if(x9 = oldx8) { |
|||
{x9 := 0;} [0.5] {x9 := 1;} |
|||
} else { |
|||
x9 := oldx8; |
|||
} |
|||
oldx8 := 0; |
|||
if(x10 = oldx9) { |
|||
{x10 := 0;} [0.5] {x10 := 1;} |
|||
} else { |
|||
x10 := oldx9; |
|||
} |
|||
oldx9 := 0; |
|||
if(x11 = oldx10) { |
|||
{x11 := 0;} [0.5] {x11 := 1;} |
|||
} else { |
|||
x11 := oldx10; |
|||
} |
|||
oldx10 := 0; |
|||
if(x12 = oldx11) { |
|||
{x12 := 0;} [0.5] {x12 := 1;} |
|||
} else { |
|||
x12 := oldx11; |
|||
} |
|||
oldx11 := 0; |
|||
if(x13 = oldx12) { |
|||
{x13 := 0;} [0.5] {x13 := 1;} |
|||
} else { |
|||
x13 := oldx12; |
|||
} |
|||
oldx12 := 0; |
|||
if(x14 = oldx13) { |
|||
{x14 := 0;} [0.5] {x14 := 1;} |
|||
} else { |
|||
x14 := oldx13; |
|||
} |
|||
oldx13 := 0; |
|||
if(x15 = oldx14) { |
|||
{x15 := 0;} [0.5] {x15 := 1;} |
|||
} else { |
|||
x15 := oldx14; |
|||
} |
|||
oldx14 := 0; |
|||
if(x16 = oldx15) { |
|||
{x16 := 0;} [0.5] {x16 := 1;} |
|||
} else { |
|||
x16 := oldx15; |
|||
} |
|||
oldx15 := 0; |
|||
if(x17 = oldx16) { |
|||
{x17 := 0;} [0.5] {x17 := 1;} |
|||
} else { |
|||
x17 := oldx16; |
|||
} |
|||
oldx16 := 0; |
|||
if(x18 = oldx17) { |
|||
{x18 := 0;} [0.5] {x18 := 1;} |
|||
} else { |
|||
x18 := oldx17; |
|||
} |
|||
oldx17 := 0; |
|||
if(x19 = oldx18) { |
|||
{x19 := 0;} [0.5] {x19 := 1;} |
|||
} else { |
|||
x19 := oldx18; |
|||
} |
|||
oldx18 := 0; |
|||
if(x20 = oldx19) { |
|||
{x20 := 0;} [0.5] {x20 := 1;} |
|||
} else { |
|||
x20 := oldx19; |
|||
} |
|||
oldx19 := 0; |
|||
if(x21 = oldx20) { |
|||
{x21 := 0;} [0.5] {x21 := 1;} |
|||
} else { |
|||
x21 := oldx20; |
|||
} |
|||
oldx20 := 0; |
|||
} |
|||
} |
|||
@ -0,0 +1,218 @@ |
|||
function herman() { |
|||
int x1 := 0; |
|||
int x2 := 0; |
|||
int x3 := 0; |
|||
int x4 := 0; |
|||
int x5 := 0; |
|||
int x6 := 0; |
|||
int x7 := 0; |
|||
int x8 := 0; |
|||
int x9 := 0; |
|||
int x10 := 0; |
|||
int x11 := 0; |
|||
int x12 := 0; |
|||
int x13 := 0; |
|||
int x14 := 0; |
|||
int x15 := 0; |
|||
int x16 := 0; |
|||
int x17 := 0; |
|||
int x18 := 0; |
|||
int x19 := 0; |
|||
int x20 := 0; |
|||
int x21 := 0; |
|||
int oldx1 := 0; |
|||
int oldx2 := 0; |
|||
int oldx3 := 0; |
|||
int oldx4 := 0; |
|||
int oldx5 := 0; |
|||
int oldx6 := 0; |
|||
int oldx7 := 0; |
|||
int oldx8 := 0; |
|||
int oldx9 := 0; |
|||
int oldx10 := 0; |
|||
int oldx11 := 0; |
|||
int oldx12 := 0; |
|||
int oldx13 := 0; |
|||
int oldx14 := 0; |
|||
int oldx15 := 0; |
|||
int oldx16 := 0; |
|||
int oldx17 := 0; |
|||
int oldx18 := 0; |
|||
int oldx19 := 0; |
|||
int oldx20 := 0; |
|||
int oldx21 := 0; |
|||
|
|||
// determine starting token setup on the ring. |
|||
{x1 := 0;} [] {x1 := 1;} |
|||
{x2 := 0;} [] {x2 := 1;} |
|||
{x3 := 0;} [] {x3 := 1;} |
|||
{x4 := 0;} [] {x4 := 1;} |
|||
{x5 := 0;} [] {x5 := 1;} |
|||
{x6 := 0;} [] {x6 := 1;} |
|||
{x7 := 0;} [] {x7 := 1;} |
|||
{x8 := 0;} [] {x8 := 1;} |
|||
{x9 := 0;} [] {x9 := 1;} |
|||
{x10 := 0;} [] {x10 := 1;} |
|||
{x11 := 0;} [] {x11 := 1;} |
|||
{x12 := 0;} [] {x12 := 1;} |
|||
{x13 := 0;} [] {x13 := 1;} |
|||
{x14 := 0;} [] {x14 := 1;} |
|||
{x15 := 0;} [] {x15 := 1;} |
|||
{x16 := 0;} [] {x16 := 1;} |
|||
{x17 := 0;} [] {x17 := 1;} |
|||
{x18 := 0;} [] {x18 := 1;} |
|||
{x19 := 0;} [] {x19 := 1;} |
|||
{x20 := 0;} [] {x20 := 1;} |
|||
{x21 := 0;} [] {x21 := 1;} |
|||
|
|||
// finds a ring configuration with exactly one token in the ring. |
|||
while((x1 + x2 + x3 + x4 + x5 + x6 + x7 + x8 + x9 + x10 + x11 + x12 + x13 + x14 + x15 + x16 + x17 + x18 + x19 + x20 + x21) != 1) { |
|||
oldx1 := x1; |
|||
oldx2 := x2; |
|||
oldx3 := x3; |
|||
oldx4 := x4; |
|||
oldx5 := x5; |
|||
oldx6 := x6; |
|||
oldx7 := x7; |
|||
oldx8 := x8; |
|||
oldx9 := x9; |
|||
oldx10 := x10; |
|||
oldx11 := x11; |
|||
oldx12 := x12; |
|||
oldx13 := x13; |
|||
oldx14 := x14; |
|||
oldx15 := x15; |
|||
oldx16 := x16; |
|||
oldx17 := x17; |
|||
oldx18 := x18; |
|||
oldx19 := x19; |
|||
oldx20 := x20; |
|||
oldx21 := x21; |
|||
if(x1 = oldx21) { |
|||
{x1 := 0;} [0.5] {x1 := 1;} |
|||
} else { |
|||
x1 := oldx21; |
|||
} |
|||
oldx21 := 0; |
|||
if(x2 = oldx1) { |
|||
{x2 := 0;} [0.5] {x2 := 1;} |
|||
} else { |
|||
x2 := oldx1; |
|||
} |
|||
oldx1 := 0; |
|||
if(x3 = oldx2) { |
|||
{x3 := 0;} [0.5] {x3 := 1;} |
|||
} else { |
|||
x3 := oldx2; |
|||
} |
|||
oldx2 := 0; |
|||
if(x4 = oldx3) { |
|||
{x4 := 0;} [0.5] {x4 := 1;} |
|||
} else { |
|||
x4 := oldx3; |
|||
} |
|||
oldx3 := 0; |
|||
if(x5 = oldx4) { |
|||
{x5 := 0;} [0.5] {x5 := 1;} |
|||
} else { |
|||
x5 := oldx4; |
|||
} |
|||
oldx4 := 0; |
|||
if(x6 = oldx5) { |
|||
{x6 := 0;} [0.5] {x6 := 1;} |
|||
} else { |
|||
x6 := oldx5; |
|||
} |
|||
oldx5 := 0; |
|||
if(x7 = oldx6) { |
|||
{x7 := 0;} [0.5] {x7 := 1;} |
|||
} else { |
|||
x7 := oldx6; |
|||
} |
|||
oldx6 := 0; |
|||
if(x8 = oldx7) { |
|||
{x7 := 0;} [0.5] {x7 := 1;} |
|||
} else { |
|||
x8 := oldx7; |
|||
} |
|||
oldx7 := 0; |
|||
if(x9 = oldx8) { |
|||
{x9 := 0;} [0.5] {x9 := 1;} |
|||
} else { |
|||
x9 := oldx8; |
|||
} |
|||
oldx8 := 0; |
|||
if(x10 = oldx9) { |
|||
{x10 := 0;} [0.5] {x10 := 1;} |
|||
} else { |
|||
x10 := oldx9; |
|||
} |
|||
oldx9 := 0; |
|||
if(x11 = oldx10) { |
|||
{x11 := 0;} [0.5] {x11 := 1;} |
|||
} else { |
|||
x11 := oldx10; |
|||
} |
|||
oldx10 := 0; |
|||
if(x12 = oldx11) { |
|||
{x12 := 0;} [0.5] {x12 := 1;} |
|||
} else { |
|||
x12 := oldx11; |
|||
} |
|||
oldx11 := 0; |
|||
if(x13 = oldx12) { |
|||
{x13 := 0;} [0.5] {x13 := 1;} |
|||
} else { |
|||
x13 := oldx12; |
|||
} |
|||
oldx12 := 0; |
|||
if(x14 = oldx13) { |
|||
{x14 := 0;} [0.5] {x14 := 1;} |
|||
} else { |
|||
x14 := oldx13; |
|||
} |
|||
oldx13 := 0; |
|||
if(x15 = oldx14) { |
|||
{x15 := 0;} [0.5] {x15 := 1;} |
|||
} else { |
|||
x15 := oldx14; |
|||
} |
|||
oldx14 := 0; |
|||
if(x16 = oldx15) { |
|||
{x16 := 0;} [0.5] {x16 := 1;} |
|||
} else { |
|||
x16 := oldx15; |
|||
} |
|||
oldx15 := 0; |
|||
if(x17 = oldx16) { |
|||
{x17 := 0;} [0.5] {x17 := 1;} |
|||
} else { |
|||
x17 := oldx16; |
|||
} |
|||
oldx16 := 0; |
|||
if(x18 = oldx17) { |
|||
{x18 := 0;} [0.5] {x18 := 1;} |
|||
} else { |
|||
x18 := oldx17; |
|||
} |
|||
oldx17 := 0; |
|||
if(x19 = oldx18) { |
|||
{x19 := 0;} [0.5] {x19 := 1;} |
|||
} else { |
|||
x19 := oldx18; |
|||
} |
|||
oldx18 := 0; |
|||
if(x20 = oldx19) { |
|||
{x20 := 0;} [0.5] {x20 := 1;} |
|||
} else { |
|||
x20 := oldx19; |
|||
} |
|||
oldx19 := 0; |
|||
if(x21 = oldx19) { |
|||
{x21 := 0;} [0.5] {x21 := 1;} |
|||
} else { |
|||
x21 := oldx20; |
|||
} |
|||
oldx20 := 0; |
|||
} |
|||
} |
|||
@ -0,0 +1,77 @@ |
|||
function herman() { |
|||
int x1 := 0; |
|||
int x2 := 0; |
|||
int x3 := 0; |
|||
int x4 := 0; |
|||
int x5 := 0; |
|||
int x6 := 0; |
|||
int x7 := 0; |
|||
int oldx1 := 0; |
|||
int oldx2 := 0; |
|||
int oldx3 := 0; |
|||
int oldx4 := 0; |
|||
int oldx5 := 0; |
|||
int oldx6 := 0; |
|||
int oldx7 := 0; |
|||
|
|||
{x1 := 0;} [0.5] {x1 := 1;} |
|||
{x2 := 0;} [0.5] {x2 := 1;} |
|||
{x3 := 0;} [0.5] {x3 := 1;} |
|||
{x4 := 0;} [0.5] {x4 := 1;} |
|||
{x5 := 0;} [0.5] {x5 := 1;} |
|||
{x6 := 0;} [0.5] {x6 := 1;} |
|||
{x7 := 0;} [0.5] {x7 := 1;} |
|||
|
|||
// finds a ring configuration with exactly one token in the ring. |
|||
while((x1 + x2 + x3 + x4 + x5 + x6 + x7) != 1) { |
|||
oldx1 := x1; |
|||
oldx2 := x2; |
|||
oldx3 := x3; |
|||
oldx4 := x4; |
|||
oldx5 := x5; |
|||
oldx6 := x6; |
|||
oldx7 := x7; |
|||
if(x1 = oldx7) { |
|||
{x1 := 0;} [0.5] {x1 := 1;} |
|||
} else { |
|||
x1 := oldx7; |
|||
} |
|||
oldx7 := 0; |
|||
if(x2 = oldx1) { |
|||
{x2 := 0;} [0.5] {x2 := 1;} |
|||
} else { |
|||
x2 := oldx1; |
|||
} |
|||
oldx1 := 0; |
|||
if(x3 = oldx2) { |
|||
{x3 := 0;} [0.5] {x3 := 1;} |
|||
} else { |
|||
x3 := oldx2; |
|||
} |
|||
oldx2 := 0; |
|||
if(x4 = oldx3) { |
|||
{x4 := 0;} [0.5] {x4 := 1;} |
|||
} else { |
|||
x4 := oldx3; |
|||
} |
|||
oldx3 := 0; |
|||
if(x5 = oldx4) { |
|||
{x5 := 0;} [0.5] {x5 := 1;} |
|||
} else { |
|||
x5 := oldx4; |
|||
} |
|||
oldx4 := 0; |
|||
if(x6 = oldx5) { |
|||
{x6 := 0;} [0.5] {x6 := 1;} |
|||
} else { |
|||
x6 := oldx5; |
|||
} |
|||
oldx5 := 0; |
|||
if(x7 = oldx6) { |
|||
{x7 := 0;} [0.5] {x7 := 1;} |
|||
} else { |
|||
x7 := oldx6; |
|||
} |
|||
oldx6 := 0; |
|||
} |
|||
} |
|||
@ -0,0 +1,77 @@ |
|||
function herman() { |
|||
int x1 := 0; |
|||
int x2 := 0; |
|||
int x3 := 0; |
|||
int x4 := 0; |
|||
int x5 := 0; |
|||
int x6 := 0; |
|||
int x7 := 0; |
|||
int oldx1 := 0; |
|||
int oldx2 := 0; |
|||
int oldx3 := 0; |
|||
int oldx4 := 0; |
|||
int oldx5 := 0; |
|||
int oldx6 := 0; |
|||
int oldx7 := 0; |
|||
|
|||
{x1 := 0;} [] {x1 := 1;} |
|||
{x2 := 0;} [] {x2 := 1;} |
|||
{x3 := 0;} [] {x3 := 1;} |
|||
{x4 := 0;} [] {x4 := 1;} |
|||
{x5 := 0;} [] {x5 := 1;} |
|||
{x6 := 0;} [] {x6 := 1;} |
|||
{x7 := 0;} [] {x7 := 1;} |
|||
|
|||
// finds a ring configuration with exactly one token in the ring. |
|||
while((x1 + x2 + x3 + x4 + x5 + x6 + x7) != 1) { |
|||
oldx1 := x1; |
|||
oldx2 := x2; |
|||
oldx3 := x3; |
|||
oldx4 := x4; |
|||
oldx5 := x5; |
|||
oldx6 := x6; |
|||
oldx7 := x7; |
|||
if(x1 = oldx7) { |
|||
{x1 := 0;} [0.5] {x1 := 1;} |
|||
} else { |
|||
x1 := oldx7; |
|||
} |
|||
oldx7 := 0; |
|||
if(x2 = oldx1) { |
|||
{x2 := 0;} [0.5] {x2 := 1;} |
|||
} else { |
|||
x2 := oldx1; |
|||
} |
|||
oldx1 := 0; |
|||
if(x3 = oldx2) { |
|||
{x3 := 0;} [0.5] {x3 := 1;} |
|||
} else { |
|||
x3 := oldx2; |
|||
} |
|||
oldx2 := 0; |
|||
if(x4 = oldx3) { |
|||
{x4 := 0;} [0.5] {x4 := 1;} |
|||
} else { |
|||
x4 := oldx3; |
|||
} |
|||
oldx3 := 0; |
|||
if(x5 = oldx4) { |
|||
{x5 := 0;} [0.5] {x5 := 1;} |
|||
} else { |
|||
x5 := oldx4; |
|||
} |
|||
oldx4 := 0; |
|||
if(x6 = oldx5) { |
|||
{x6 := 0;} [0.5] {x6 := 1;} |
|||
} else { |
|||
x6 := oldx5; |
|||
} |
|||
oldx5 := 0; |
|||
if(x7 = oldx6) { |
|||
{x7 := 0;} [0.5] {x7 := 1;} |
|||
} else { |
|||
x7 := oldx6; |
|||
} |
|||
oldx6 := 0; |
|||
} |
|||
} |
|||
@ -0,0 +1,49 @@ |
|||
function lotkavolterra() { |
|||
|
|||
int goats := 100; |
|||
int tigers := 4; |
|||
int dwellTime := 0; |
|||
int curTime := 0; |
|||
int b := 0; |
|||
|
|||
while(tigers > 0 & goats > 0) { |
|||
|
|||
dwellTime := 0; |
|||
b := 1; |
|||
|
|||
if(goats > 0 & tigers > 0) { |
|||
|
|||
// geometric distribution with p = 0.5 |
|||
while (b >= 1) { |
|||
{b := 1;} [0.5] {b := 0;} |
|||
dwellTime := dwellTime + 1; |
|||
} |
|||
curTime := curTime + dwellTime; |
|||
{tigers := tigers + 1;} [0.2] {{goats := goats - 1;} [0.1] {tigers := tigers - 1;}} |
|||
|
|||
} else { if(goats > 0) { |
|||
|
|||
// geometric distribution with p = 0.5 |
|||
while (b >= 1) { |
|||
{b := 1;} [0.5] {b := 0;} |
|||
dwellTime := dwellTime + 1; |
|||
} |
|||
curTime := curTime + dwellTime; |
|||
goats := goats + 1; |
|||
|
|||
} else { if(tigers > 0) { |
|||
|
|||
// geometric distribution with p = 0.5 |
|||
while (b >= 1) { |
|||
{b := 1;} [0.5] {b := 0;} |
|||
dwellTime := dwellTime + 1; |
|||
} |
|||
curTime := curTime + dwellTime; |
|||
tigers := tigers - 1; |
|||
|
|||
} } } |
|||
|
|||
} |
|||
|
|||
} |
|||
|
|||
@ -0,0 +1,26 @@ |
|||
function robotOnGrid() { |
|||
|
|||
// robot starts in the lower left corner |
|||
int robotX := 1; int robotY := 20; |
|||
|
|||
// janitor starts in the grid middle |
|||
int janitorX := ceil(20 / 2); int janitorY := ceil(20 / 2); |
|||
|
|||
// iterates as long as the robot is not in the upper right corner |
|||
while(!(robotX = 20 & robotY = 1)) { |
|||
|
|||
// robot perfoms one step at max each iteration |
|||
// checks whether we can go to the right and the janitor is not there |
|||
if(robotX < 20 & !((janitorX = robotX + 1) & (janitorY = robotY))) { |
|||
robotX := robotX + 1; |
|||
} |
|||
// checks whether we can go up and the janitor is not there |
|||
if(robotX = 20 & !((janitorX = robotX) & (janitorY = robotY - 1))) { |
|||
robotY := robotY - 1; |
|||
} |
|||
|
|||
// moves the janitor randomly in one direction, not limited by any borders |
|||
{janitorX := janitorX + 1;}[0.25]{{janitorX := janitorX - 1;}[1/3]{{janitorY := janitorY + 1;}[0.375]{janitorY := janitorY - 1;}}} |
|||
|
|||
} |
|||
} |
|||
@ -1,77 +0,0 @@ |
|||
#define BENCHPRESS_CONFIG_MAIN
|
|||
|
|||
#include <fstream>
|
|||
#include <benchpress.hpp>
|
|||
#include <json.hpp>
|
|||
|
|||
BENCHMARK("parse jeopardy.json", [](benchpress::context* ctx) |
|||
{ |
|||
for (size_t i = 0; i < ctx->num_iterations(); ++i) |
|||
{ |
|||
std::ifstream input_file("benchmarks/files/jeopardy/jeopardy.json"); |
|||
nlohmann::json j; |
|||
j << input_file; |
|||
} |
|||
}) |
|||
|
|||
BENCHMARK("parse canada.json", [](benchpress::context* ctx) |
|||
{ |
|||
for (size_t i = 0; i < ctx->num_iterations(); ++i) |
|||
{ |
|||
std::ifstream input_file("benchmarks/files/nativejson-benchmark/canada.json"); |
|||
nlohmann::json j; |
|||
j << input_file; |
|||
} |
|||
}) |
|||
|
|||
BENCHMARK("parse citm_catalog.json", [](benchpress::context* ctx) |
|||
{ |
|||
for (size_t i = 0; i < ctx->num_iterations(); ++i) |
|||
{ |
|||
std::ifstream input_file("benchmarks/files/nativejson-benchmark/citm_catalog.json"); |
|||
nlohmann::json j; |
|||
j << input_file; |
|||
} |
|||
}) |
|||
|
|||
BENCHMARK("parse twitter.json", [](benchpress::context* ctx) |
|||
{ |
|||
for (size_t i = 0; i < ctx->num_iterations(); ++i) |
|||
{ |
|||
std::ifstream input_file("benchmarks/files/nativejson-benchmark/twitter.json"); |
|||
nlohmann::json j; |
|||
j << input_file; |
|||
} |
|||
}) |
|||
|
|||
BENCHMARK("dump jeopardy.json", [](benchpress::context* ctx) |
|||
{ |
|||
std::ifstream input_file("benchmarks/files/jeopardy/jeopardy.json"); |
|||
nlohmann::json j; |
|||
j << input_file; |
|||
std::ofstream output_file("jeopardy.dump.json"); |
|||
|
|||
ctx->reset_timer(); |
|||
for (size_t i = 0; i < ctx->num_iterations(); ++i) |
|||
{ |
|||
output_file << j; |
|||
} |
|||
|
|||
std::remove("jeopardy.dump.json"); |
|||
}) |
|||
|
|||
BENCHMARK("dump jeopardy.json with indent", [](benchpress::context* ctx) |
|||
{ |
|||
std::ifstream input_file("benchmarks/files/jeopardy/jeopardy.json"); |
|||
nlohmann::json j; |
|||
j << input_file; |
|||
std::ofstream output_file("jeopardy.dump.json"); |
|||
|
|||
ctx->reset_timer(); |
|||
for (size_t i = 0; i < ctx->num_iterations(); ++i) |
|||
{ |
|||
output_file << std::setw(4) << j; |
|||
} |
|||
|
|||
std::remove("jeopardy.dump.json"); |
|||
}) |
|||
@ -1,401 +0,0 @@ |
|||
/*
|
|||
* Copyright (C) 2015 Christopher Gilbert. |
|||
* |
|||
* Permission is hereby granted, free of charge, to any person obtaining a copy |
|||
* of this software and associated documentation files (the "Software"), to deal |
|||
* in the Software without restriction, including without limitation the rights |
|||
* to use, copy, modify, merge, publish, distribute, sublicense, and/or sell |
|||
* copies of the Software, and to permit persons to whom the Software is |
|||
* furnished to do so, subject to the following conditions: |
|||
* |
|||
* The above copyright notice and this permission notice shall be included in all |
|||
* copies or substantial portions of the Software. |
|||
* |
|||
* THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR |
|||
* IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY, |
|||
* FITNESS FOR A PARTICULAR PURPOSE AND NONINFRINGEMENT. IN NO EVENT SHALL THE |
|||
* AUTHORS OR COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM, DAMAGES OR OTHER |
|||
* LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM, |
|||
* OUT OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE |
|||
* SOFTWARE. |
|||
*/ |
|||
#ifndef BENCHPRESS_HPP
|
|||
#define BENCHPRESS_HPP
|
|||
|
|||
#include <algorithm> // max, min
|
|||
#include <atomic> // atomic_intmax_t
|
|||
#include <chrono> // high_resolution_timer, duration
|
|||
#include <functional> // function
|
|||
#include <iomanip> // setw
|
|||
#include <iostream> // cout
|
|||
#include <regex> // regex, regex_match
|
|||
#include <sstream> // stringstream
|
|||
#include <string> // string
|
|||
#include <thread> // thread
|
|||
#include <vector> // vector
|
|||
|
|||
namespace benchpress { |
|||
|
|||
/*
|
|||
* The options class encapsulates all options for running benchmarks. |
|||
* |
|||
* When including benchpress, a main function can be emitted which includes a command-line parser for building an |
|||
* options object. However from time-to-time it may be necessary for the developer to have to build their own main |
|||
* stub and construct the options object manually. |
|||
* |
|||
* options opts; |
|||
* opts |
|||
* .bench(".*") |
|||
* .benchtime(1) |
|||
* .cpu(4); |
|||
*/ |
|||
class options { |
|||
std::string d_bench; |
|||
size_t d_benchtime; |
|||
size_t d_cpu; |
|||
public: |
|||
options() |
|||
: d_bench(".*") |
|||
, d_benchtime(1) |
|||
, d_cpu(std::thread::hardware_concurrency()) |
|||
{} |
|||
options& bench(const std::string& bench) { |
|||
d_bench = bench; |
|||
return *this; |
|||
} |
|||
options& benchtime(size_t benchtime) { |
|||
d_benchtime = benchtime; |
|||
return *this; |
|||
} |
|||
options& cpu(size_t cpu) { |
|||
d_cpu = cpu; |
|||
return *this; |
|||
} |
|||
std::string get_bench() const { |
|||
return d_bench; |
|||
} |
|||
size_t get_benchtime() const { |
|||
return d_benchtime; |
|||
} |
|||
size_t get_cpu() const { |
|||
return d_cpu; |
|||
} |
|||
}; |
|||
|
|||
class context; |
|||
|
|||
/*
|
|||
* The benchmark_info class is used to store a function name / pointer pair. |
|||
* |
|||
* benchmark_info bi("example", [](benchpress::context* b) { |
|||
* // benchmark function
|
|||
* }); |
|||
*/ |
|||
class benchmark_info { |
|||
std::string d_name; |
|||
std::function<void(context*)> d_func; |
|||
|
|||
public: |
|||
benchmark_info(std::string name, std::function<void(context*)> func) |
|||
: d_name(name) |
|||
, d_func(func) |
|||
{} |
|||
|
|||
std::string get_name() const { return d_name; } |
|||
std::function<void(context*)> get_func() const { return d_func; } |
|||
}; |
|||
|
|||
/*
|
|||
* The registration class is responsible for providing a single global point of reference for registering |
|||
* benchmark functions. |
|||
* |
|||
* registration::get_ptr()->register_benchmark(info); |
|||
*/ |
|||
class registration { |
|||
static registration* d_this; |
|||
std::vector<benchmark_info> d_benchmarks; |
|||
|
|||
public: |
|||
static registration* get_ptr() { |
|||
if (nullptr == d_this) { |
|||
d_this = new registration(); |
|||
} |
|||
return d_this; |
|||
} |
|||
|
|||
void register_benchmark(benchmark_info& info) { |
|||
d_benchmarks.push_back(info); |
|||
} |
|||
|
|||
std::vector<benchmark_info> get_benchmarks() { return d_benchmarks; } |
|||
}; |
|||
|
|||
/*
|
|||
* The auto_register class is a helper used to register benchmarks. |
|||
*/ |
|||
class auto_register { |
|||
public: |
|||
auto_register(const std::string& name, std::function<void(context*)> func) { |
|||
benchmark_info info(name, func); |
|||
registration::get_ptr()->register_benchmark(info); |
|||
} |
|||
}; |
|||
|
|||
#define CONCAT(x, y) x ## y
|
|||
#define CONCAT2(x, y) CONCAT(x, y)
|
|||
|
|||
// The BENCHMARK macro is a helper for creating benchmark functions and automatically registering them with the
|
|||
// registration class.
|
|||
#define BENCHMARK(x, f) benchpress::auto_register CONCAT2(register_, __LINE__)((x), (f));
|
|||
|
|||
// This macro will prevent the compiler from removing a redundant code path which has no side-effects.
|
|||
#define DISABLE_REDUNDANT_CODE_OPT() { asm(""); }
|
|||
|
|||
/*
|
|||
* The result class is responsible for producing a printable string representation of a benchmark run. |
|||
*/ |
|||
class result { |
|||
size_t d_num_iterations; |
|||
std::chrono::nanoseconds d_duration; |
|||
size_t d_num_bytes; |
|||
|
|||
public: |
|||
result(size_t num_iterations, std::chrono::nanoseconds duration, size_t num_bytes) |
|||
: d_num_iterations(num_iterations) |
|||
, d_duration(duration) |
|||
, d_num_bytes(num_bytes) |
|||
{} |
|||
|
|||
size_t get_ns_per_op() const { |
|||
if (d_num_iterations <= 0) { |
|||
return 0; |
|||
} |
|||
return d_duration.count() / d_num_iterations; |
|||
} |
|||
|
|||
double get_mb_per_s() const { |
|||
if (d_num_iterations <= 0 || d_duration.count() <= 0 || d_num_bytes <= 0) { |
|||
return 0; |
|||
} |
|||
return ((double(d_num_bytes) * double(d_num_iterations) / double(1e6)) / |
|||
double(std::chrono::duration_cast<std::chrono::seconds>(d_duration).count())); |
|||
} |
|||
|
|||
std::string to_string() const { |
|||
std::stringstream tmp; |
|||
tmp << std::setw(12) << std::right << d_num_iterations; |
|||
size_t npo = get_ns_per_op(); |
|||
tmp << std::setw(12) << std::right << npo << std::setw(0) << " ns/op"; |
|||
double mbs = get_mb_per_s(); |
|||
if (mbs > 0.0) { |
|||
tmp << std::setw(12) << std::right << mbs << std::setw(0) << " MB/s"; |
|||
} |
|||
return std::string(tmp.str()); |
|||
} |
|||
}; |
|||
|
|||
/*
|
|||
* The parallel_context class is responsible for providing a thread-safe context for parallel benchmark code. |
|||
*/ |
|||
class parallel_context { |
|||
std::atomic_intmax_t d_num_iterations; |
|||
public: |
|||
parallel_context(size_t num_iterations) |
|||
: d_num_iterations(num_iterations) |
|||
{} |
|||
|
|||
bool next() { |
|||
return (d_num_iterations.fetch_sub(1) > 0); |
|||
} |
|||
}; |
|||
|
|||
/*
|
|||
* The context class is responsible for providing an interface for capturing benchmark metrics to benchmark functions. |
|||
*/ |
|||
class context { |
|||
bool d_timer_on; |
|||
std::chrono::high_resolution_clock::time_point d_start; |
|||
std::chrono::nanoseconds d_duration; |
|||
std::chrono::seconds d_benchtime; |
|||
size_t d_num_iterations; |
|||
size_t d_num_threads; |
|||
size_t d_num_bytes; |
|||
benchmark_info d_benchmark; |
|||
|
|||
public: |
|||
context(const benchmark_info& info, const options& opts) |
|||
: d_timer_on(false) |
|||
, d_start() |
|||
, d_duration() |
|||
, d_benchtime(std::chrono::seconds(opts.get_benchtime())) |
|||
, d_num_iterations(1) |
|||
, d_num_threads(opts.get_cpu()) |
|||
, d_num_bytes(0) |
|||
, d_benchmark(info) |
|||
{} |
|||
|
|||
size_t num_iterations() const { return d_num_iterations; } |
|||
|
|||
void set_num_threads(size_t n) { d_num_threads = n; } |
|||
size_t num_threads() const { return d_num_threads; } |
|||
|
|||
void start_timer() { |
|||
if (!d_timer_on) { |
|||
d_start = std::chrono::high_resolution_clock::now(); |
|||
d_timer_on = true; |
|||
} |
|||
} |
|||
void stop_timer() { |
|||
if (d_timer_on) { |
|||
d_duration += std::chrono::high_resolution_clock::now() - d_start; |
|||
d_timer_on = false; |
|||
} |
|||
} |
|||
void reset_timer() { |
|||
if (d_timer_on) { |
|||
d_start = std::chrono::high_resolution_clock::now(); |
|||
} |
|||
d_duration = std::chrono::nanoseconds::zero(); |
|||
} |
|||
|
|||
void set_bytes(int64_t bytes) { d_num_bytes = bytes; } |
|||
|
|||
size_t get_ns_per_op() { |
|||
if (d_num_iterations <= 0) { |
|||
return 0; |
|||
} |
|||
return d_duration.count() / d_num_iterations; |
|||
} |
|||
|
|||
void run_n(size_t n) { |
|||
d_num_iterations = n; |
|||
reset_timer(); |
|||
start_timer(); |
|||
d_benchmark.get_func()(this); |
|||
stop_timer(); |
|||
} |
|||
|
|||
void run_parallel(std::function<void(parallel_context*)> f) { |
|||
parallel_context pc(d_num_iterations); |
|||
std::vector<std::thread> threads; |
|||
for (size_t i = 0; i < d_num_threads; ++i) { |
|||
threads.push_back(std::thread([&pc,&f]() -> void { |
|||
f(&pc); |
|||
})); |
|||
} |
|||
for(auto& thread : threads){ |
|||
thread.join(); |
|||
} |
|||
} |
|||
|
|||
result run() { |
|||
size_t n = 1; |
|||
run_n(n); |
|||
while (d_duration < d_benchtime && n < 1e9) { |
|||
size_t last = n; |
|||
if (get_ns_per_op() == 0) { |
|||
n = 1e9; |
|||
} else { |
|||
n = d_duration.count() / get_ns_per_op(); |
|||
} |
|||
n = std::max(std::min(n+n/2, 100*last), last+1); |
|||
n = round_up(n); |
|||
run_n(n); |
|||
} |
|||
return result(n, d_duration, d_num_bytes); |
|||
} |
|||
|
|||
private: |
|||
template<typename T> |
|||
T round_down_10(T n) { |
|||
int tens = 0; |
|||
while (n > 10) { |
|||
n /= 10; |
|||
tens++; |
|||
} |
|||
int result = 1; |
|||
for (int i = 0; i < tens; ++i) { |
|||
result *= 10; |
|||
} |
|||
return result; |
|||
} |
|||
|
|||
template<typename T> |
|||
T round_up(T n) { |
|||
T base = round_down_10(n); |
|||
if (n < (2 * base)) { |
|||
return 2 * base; |
|||
} |
|||
if (n < (5 * base)) { |
|||
return 5 * base; |
|||
} |
|||
return 10 * base; |
|||
} |
|||
}; |
|||
|
|||
/*
|
|||
* The run_benchmarks function will run the registered benchmarks. |
|||
*/ |
|||
void run_benchmarks(const options& opts) { |
|||
std::regex match_r(opts.get_bench()); |
|||
auto benchmarks = registration::get_ptr()->get_benchmarks(); |
|||
for (auto& info : benchmarks) { |
|||
if (std::regex_match(info.get_name(), match_r)) { |
|||
context c(info, opts); |
|||
auto r = c.run(); |
|||
std::cout << std::setw(35) << std::left << info.get_name() << r.to_string() << std::endl; |
|||
} |
|||
} |
|||
} |
|||
|
|||
} // namespace benchpress
|
|||
|
|||
/*
|
|||
* If BENCHPRESS_CONFIG_MAIN is defined when the file is included then a main function will be emitted which provides a |
|||
* command-line parser and then executes run_benchmarks. |
|||
*/ |
|||
#ifdef BENCHPRESS_CONFIG_MAIN
|
|||
#include "cxxopts.hpp"
|
|||
benchpress::registration* benchpress::registration::d_this; |
|||
int main(int argc, char** argv) { |
|||
std::chrono::high_resolution_clock::time_point bp_start = std::chrono::high_resolution_clock::now(); |
|||
benchpress::options bench_opts; |
|||
try { |
|||
cxxopts::Options cmd_opts(argv[0], " - command line options"); |
|||
cmd_opts.add_options() |
|||
("bench", "run benchmarks matching the regular expression", cxxopts::value<std::string>() |
|||
->default_value(".*")) |
|||
("benchtime", "run enough iterations of each benchmark to take t seconds", cxxopts::value<size_t>() |
|||
->default_value("1")) |
|||
("cpu", "specify the number of threads to use for parallel benchmarks", cxxopts::value<size_t>() |
|||
->default_value(std::to_string(std::thread::hardware_concurrency()))) |
|||
("help", "print help") |
|||
; |
|||
cmd_opts.parse(argc, argv); |
|||
if (cmd_opts.count("help")) { |
|||
std::cout << cmd_opts.help({""}) << std::endl; |
|||
exit(0); |
|||
} |
|||
if (cmd_opts.count("bench")) { |
|||
bench_opts.bench(cmd_opts["bench"].as<std::string>()); |
|||
} |
|||
if (cmd_opts.count("benchtime")) { |
|||
bench_opts.benchtime(cmd_opts["benchtime"].as<size_t>()); |
|||
} |
|||
if (cmd_opts.count("cpu")) { |
|||
bench_opts.cpu(cmd_opts["cpu"].as<size_t>()); |
|||
} |
|||
} catch (const cxxopts::OptionException& e) { |
|||
std::cout << "error parsing options: " << e.what() << std::endl; |
|||
exit(1); |
|||
} |
|||
benchpress::run_benchmarks(bench_opts); |
|||
float duration = std::chrono::duration_cast<std::chrono::milliseconds>( |
|||
std::chrono::high_resolution_clock::now() - bp_start |
|||
).count() / 1000.f; |
|||
std::cout << argv[0] << " " << duration << "s" << std::endl; |
|||
return 0; |
|||
} |
|||
#endif
|
|||
|
|||
#endif // BENCHPRESS_HPP
|
|||
1312
resources/3rdparty/modernjson/benchmarks/cxxopts.hpp
File diff suppressed because it is too large
View File
File diff suppressed because it is too large
View File
@ -1 +0,0 @@ |
|||
a533fde78ce50a11f6189907f9e0392095222fe2 |
|||
9
resources/3rdparty/modernjson/benchmarks/files/nativejson-benchmark/canada.json
File diff suppressed because it is too large
View File
File diff suppressed because it is too large
View File
50469
resources/3rdparty/modernjson/benchmarks/files/nativejson-benchmark/citm_catalog.json
File diff suppressed because it is too large
View File
File diff suppressed because it is too large
View File
15482
resources/3rdparty/modernjson/benchmarks/files/nativejson-benchmark/twitter.json
File diff suppressed because it is too large
View File
File diff suppressed because it is too large
View File
@ -1,317 +0,0 @@ |
|||
# Doxyfile 1.8.9.1 |
|||
|
|||
#--------------------------------------------------------------------------- |
|||
# Project related configuration options |
|||
#--------------------------------------------------------------------------- |
|||
DOXYFILE_ENCODING = UTF-8 |
|||
PROJECT_NAME = "JSON for Modern C++" |
|||
PROJECT_NUMBER = 2.0.0 |
|||
PROJECT_BRIEF = |
|||
PROJECT_LOGO = |
|||
OUTPUT_DIRECTORY = . |
|||
CREATE_SUBDIRS = NO |
|||
ALLOW_UNICODE_NAMES = NO |
|||
OUTPUT_LANGUAGE = English |
|||
BRIEF_MEMBER_DESC = YES |
|||
REPEAT_BRIEF = NO |
|||
ABBREVIATE_BRIEF = |
|||
ALWAYS_DETAILED_SEC = YES |
|||
INLINE_INHERITED_MEMB = NO |
|||
FULL_PATH_NAMES = YES |
|||
STRIP_FROM_PATH = |
|||
STRIP_FROM_INC_PATH = |
|||
SHORT_NAMES = NO |
|||
JAVADOC_AUTOBRIEF = NO |
|||
QT_AUTOBRIEF = NO |
|||
MULTILINE_CPP_IS_BRIEF = NO |
|||
INHERIT_DOCS = YES |
|||
SEPARATE_MEMBER_PAGES = YES |
|||
TAB_SIZE = 4 |
|||
ALIASES = "complexity=@par Complexity\n" |
|||
ALIASES += liveexample{2}="@par Example\n \1 \n @includelineno \2.cpp \n Output (play with this example @htmlinclude \2.link):\n @verbinclude \2.output \n The example code above can be translated with @verbatim g++ -std=c++11 -Isrc doc/examples/\2.cpp -o \2 @endverbatim" |
|||
ALIASES += requirement="@par Requirements\n" |
|||
ALIASES += exceptionsafety="@par Exception safety\n" |
|||
TCL_SUBST = |
|||
OPTIMIZE_OUTPUT_FOR_C = NO |
|||
OPTIMIZE_OUTPUT_JAVA = NO |
|||
OPTIMIZE_FOR_FORTRAN = NO |
|||
OPTIMIZE_OUTPUT_VHDL = NO |
|||
EXTENSION_MAPPING = |
|||
MARKDOWN_SUPPORT = YES |
|||
AUTOLINK_SUPPORT = NO |
|||
BUILTIN_STL_SUPPORT = YES |
|||
CPP_CLI_SUPPORT = NO |
|||
SIP_SUPPORT = NO |
|||
IDL_PROPERTY_SUPPORT = YES |
|||
DISTRIBUTE_GROUP_DOC = NO |
|||
SUBGROUPING = YES |
|||
INLINE_GROUPED_CLASSES = NO |
|||
INLINE_SIMPLE_STRUCTS = NO |
|||
TYPEDEF_HIDES_STRUCT = NO |
|||
LOOKUP_CACHE_SIZE = 0 |
|||
#--------------------------------------------------------------------------- |
|||
# Build related configuration options |
|||
#--------------------------------------------------------------------------- |
|||
EXTRACT_ALL = YES |
|||
EXTRACT_PRIVATE = NO |
|||
EXTRACT_PACKAGE = YES |
|||
EXTRACT_STATIC = YES |
|||
EXTRACT_LOCAL_CLASSES = YES |
|||
EXTRACT_LOCAL_METHODS = YES |
|||
EXTRACT_ANON_NSPACES = YES |
|||
HIDE_UNDOC_MEMBERS = NO |
|||
HIDE_UNDOC_CLASSES = NO |
|||
HIDE_FRIEND_COMPOUNDS = NO |
|||
HIDE_IN_BODY_DOCS = NO |
|||
INTERNAL_DOCS = NO |
|||
CASE_SENSE_NAMES = NO |
|||
HIDE_SCOPE_NAMES = NO |
|||
HIDE_COMPOUND_REFERENCE= NO |
|||
SHOW_INCLUDE_FILES = YES |
|||
SHOW_GROUPED_MEMB_INC = NO |
|||
FORCE_LOCAL_INCLUDES = NO |
|||
INLINE_INFO = YES |
|||
SORT_MEMBER_DOCS = YES |
|||
SORT_BRIEF_DOCS = YES |
|||
SORT_MEMBERS_CTORS_1ST = YES |
|||
SORT_GROUP_NAMES = NO |
|||
SORT_BY_SCOPE_NAME = NO |
|||
STRICT_PROTO_MATCHING = NO |
|||
GENERATE_TODOLIST = YES |
|||
GENERATE_TESTLIST = YES |
|||
GENERATE_BUGLIST = YES |
|||
GENERATE_DEPRECATEDLIST= YES |
|||
ENABLED_SECTIONS = |
|||
MAX_INITIALIZER_LINES = 30 |
|||
SHOW_USED_FILES = NO |
|||
SHOW_FILES = NO |
|||
SHOW_NAMESPACES = NO |
|||
FILE_VERSION_FILTER = |
|||
LAYOUT_FILE = |
|||
CITE_BIB_FILES = |
|||
#--------------------------------------------------------------------------- |
|||
# Configuration options related to warning and progress messages |
|||
#--------------------------------------------------------------------------- |
|||
QUIET = YES |
|||
WARNINGS = YES |
|||
WARN_IF_UNDOCUMENTED = YES |
|||
WARN_IF_DOC_ERROR = YES |
|||
WARN_NO_PARAMDOC = YES |
|||
WARN_FORMAT = "$file:$line: $text" |
|||
WARN_LOGFILE = |
|||
#--------------------------------------------------------------------------- |
|||
# Configuration options related to the input files |
|||
#--------------------------------------------------------------------------- |
|||
INPUT = ../src/json.hpp index.md |
|||
INPUT_ENCODING = UTF-8 |
|||
FILE_PATTERNS = |
|||
RECURSIVE = NO |
|||
EXCLUDE = |
|||
EXCLUDE_SYMLINKS = NO |
|||
EXCLUDE_PATTERNS = |
|||
EXCLUDE_SYMBOLS = nlohmann::anonymous_namespace |
|||
EXAMPLE_PATH = examples |
|||
EXAMPLE_PATTERNS = |
|||
EXAMPLE_RECURSIVE = NO |
|||
IMAGE_PATH = images |
|||
INPUT_FILTER = |
|||
FILTER_PATTERNS = |
|||
FILTER_SOURCE_FILES = NO |
|||
FILTER_SOURCE_PATTERNS = |
|||
USE_MDFILE_AS_MAINPAGE = index.md |
|||
#--------------------------------------------------------------------------- |
|||
# Configuration options related to source browsing |
|||
#--------------------------------------------------------------------------- |
|||
SOURCE_BROWSER = YES |
|||
INLINE_SOURCES = NO |
|||
STRIP_CODE_COMMENTS = YES |
|||
REFERENCED_BY_RELATION = NO |
|||
REFERENCES_RELATION = NO |
|||
REFERENCES_LINK_SOURCE = NO |
|||
SOURCE_TOOLTIPS = YES |
|||
USE_HTAGS = NO |
|||
VERBATIM_HEADERS = NO |
|||
#--------------------------------------------------------------------------- |
|||
# Configuration options related to the alphabetical class index |
|||
#--------------------------------------------------------------------------- |
|||
ALPHABETICAL_INDEX = YES |
|||
COLS_IN_ALPHA_INDEX = 5 |
|||
IGNORE_PREFIX = |
|||
#--------------------------------------------------------------------------- |
|||
# Configuration options related to the HTML output |
|||
#--------------------------------------------------------------------------- |
|||
GENERATE_HTML = YES |
|||
HTML_OUTPUT = html |
|||
HTML_FILE_EXTENSION = .html |
|||
HTML_HEADER = |
|||
HTML_FOOTER = |
|||
HTML_STYLESHEET = |
|||
HTML_EXTRA_STYLESHEET = css/mylayout.css |
|||
HTML_EXTRA_FILES = |
|||
HTML_COLORSTYLE_HUE = 220 |
|||
HTML_COLORSTYLE_SAT = 100 |
|||
HTML_COLORSTYLE_GAMMA = 80 |
|||
HTML_TIMESTAMP = YES |
|||
HTML_DYNAMIC_SECTIONS = YES |
|||
HTML_INDEX_NUM_ENTRIES = 100 |
|||
GENERATE_DOCSET = YES |
|||
DOCSET_FEEDNAME = "Doxygen generated docs" |
|||
DOCSET_BUNDLE_ID = me.nlohmann.json |
|||
DOCSET_PUBLISHER_ID = me.nlohmann |
|||
DOCSET_PUBLISHER_NAME = Niels Lohmann |
|||
GENERATE_HTMLHELP = NO |
|||
CHM_FILE = |
|||
HHC_LOCATION = |
|||
GENERATE_CHI = NO |
|||
CHM_INDEX_ENCODING = |
|||
BINARY_TOC = NO |
|||
TOC_EXPAND = NO |
|||
GENERATE_QHP = NO |
|||
QCH_FILE = |
|||
QHP_NAMESPACE = org.doxygen.Project |
|||
QHP_VIRTUAL_FOLDER = doc |
|||
QHP_CUST_FILTER_NAME = |
|||
QHP_CUST_FILTER_ATTRS = |
|||
QHP_SECT_FILTER_ATTRS = |
|||
QHG_LOCATION = |
|||
GENERATE_ECLIPSEHELP = NO |
|||
ECLIPSE_DOC_ID = org.doxygen.Project |
|||
DISABLE_INDEX = NO |
|||
GENERATE_TREEVIEW = NO |
|||
ENUM_VALUES_PER_LINE = 4 |
|||
TREEVIEW_WIDTH = 250 |
|||
EXT_LINKS_IN_WINDOW = NO |
|||
FORMULA_FONTSIZE = 10 |
|||
FORMULA_TRANSPARENT = YES |
|||
USE_MATHJAX = NO |
|||
MATHJAX_FORMAT = HTML-CSS |
|||
MATHJAX_RELPATH = http://cdn.mathjax.org/mathjax/latest |
|||
MATHJAX_EXTENSIONS = |
|||
MATHJAX_CODEFILE = |
|||
SEARCHENGINE = YES |
|||
SERVER_BASED_SEARCH = NO |
|||
EXTERNAL_SEARCH = NO |
|||
SEARCHENGINE_URL = |
|||
SEARCHDATA_FILE = searchdata.xml |
|||
EXTERNAL_SEARCH_ID = |
|||
EXTRA_SEARCH_MAPPINGS = |
|||
#--------------------------------------------------------------------------- |
|||
# Configuration options related to the LaTeX output |
|||
#--------------------------------------------------------------------------- |
|||
GENERATE_LATEX = NO |
|||
LATEX_OUTPUT = latex |
|||
LATEX_CMD_NAME = latex |
|||
MAKEINDEX_CMD_NAME = makeindex |
|||
COMPACT_LATEX = NO |
|||
PAPER_TYPE = a4 |
|||
EXTRA_PACKAGES = |
|||
LATEX_HEADER = |
|||
LATEX_FOOTER = |
|||
LATEX_EXTRA_STYLESHEET = |
|||
LATEX_EXTRA_FILES = |
|||
PDF_HYPERLINKS = YES |
|||
USE_PDFLATEX = YES |
|||
LATEX_BATCHMODE = NO |
|||
LATEX_HIDE_INDICES = NO |
|||
LATEX_SOURCE_CODE = NO |
|||
LATEX_BIB_STYLE = plain |
|||
#--------------------------------------------------------------------------- |
|||
# Configuration options related to the RTF output |
|||
#--------------------------------------------------------------------------- |
|||
GENERATE_RTF = NO |
|||
RTF_OUTPUT = rtf |
|||
COMPACT_RTF = NO |
|||
RTF_HYPERLINKS = NO |
|||
RTF_STYLESHEET_FILE = |
|||
RTF_EXTENSIONS_FILE = |
|||
RTF_SOURCE_CODE = NO |
|||
#--------------------------------------------------------------------------- |
|||
# Configuration options related to the man page output |
|||
#--------------------------------------------------------------------------- |
|||
GENERATE_MAN = NO |
|||
MAN_OUTPUT = man |
|||
MAN_EXTENSION = .3 |
|||
MAN_SUBDIR = |
|||
MAN_LINKS = NO |
|||
#--------------------------------------------------------------------------- |
|||
# Configuration options related to the XML output |
|||
#--------------------------------------------------------------------------- |
|||
GENERATE_XML = NO |
|||
XML_OUTPUT = xml |
|||
XML_PROGRAMLISTING = YES |
|||
#--------------------------------------------------------------------------- |
|||
# Configuration options related to the DOCBOOK output |
|||
#--------------------------------------------------------------------------- |
|||
GENERATE_DOCBOOK = NO |
|||
DOCBOOK_OUTPUT = docbook |
|||
DOCBOOK_PROGRAMLISTING = NO |
|||
#--------------------------------------------------------------------------- |
|||
# Configuration options for the AutoGen Definitions output |
|||
#--------------------------------------------------------------------------- |
|||
GENERATE_AUTOGEN_DEF = NO |
|||
#--------------------------------------------------------------------------- |
|||
# Configuration options related to the Perl module output |
|||
#--------------------------------------------------------------------------- |
|||
GENERATE_PERLMOD = NO |
|||
PERLMOD_LATEX = NO |
|||
PERLMOD_PRETTY = YES |
|||
PERLMOD_MAKEVAR_PREFIX = |
|||
#--------------------------------------------------------------------------- |
|||
# Configuration options related to the preprocessor |
|||
#--------------------------------------------------------------------------- |
|||
ENABLE_PREPROCESSING = YES |
|||
MACRO_EXPANSION = NO |
|||
EXPAND_ONLY_PREDEF = NO |
|||
SEARCH_INCLUDES = YES |
|||
INCLUDE_PATH = |
|||
INCLUDE_FILE_PATTERNS = |
|||
PREDEFINED = |
|||
EXPAND_AS_DEFINED = |
|||
SKIP_FUNCTION_MACROS = YES |
|||
#--------------------------------------------------------------------------- |
|||
# Configuration options related to external references |
|||
#--------------------------------------------------------------------------- |
|||
TAGFILES = |
|||
GENERATE_TAGFILE = |
|||
ALLEXTERNALS = NO |
|||
EXTERNAL_GROUPS = YES |
|||
EXTERNAL_PAGES = YES |
|||
PERL_PATH = /usr/bin/perl |
|||
#--------------------------------------------------------------------------- |
|||
# Configuration options related to the dot tool |
|||
#--------------------------------------------------------------------------- |
|||
CLASS_DIAGRAMS = NO |
|||
MSCGEN_PATH = |
|||
DIA_PATH = |
|||
HIDE_UNDOC_RELATIONS = YES |
|||
HAVE_DOT = YES |
|||
DOT_NUM_THREADS = 0 |
|||
DOT_FONTNAME = Helvetica |
|||
DOT_FONTSIZE = 10 |
|||
DOT_FONTPATH = |
|||
CLASS_GRAPH = NO |
|||
COLLABORATION_GRAPH = NO |
|||
GROUP_GRAPHS = YES |
|||
UML_LOOK = YES |
|||
UML_LIMIT_NUM_FIELDS = 10 |
|||
TEMPLATE_RELATIONS = NO |
|||
INCLUDE_GRAPH = NO |
|||
INCLUDED_BY_GRAPH = NO |
|||
CALL_GRAPH = NO |
|||
CALLER_GRAPH = NO |
|||
GRAPHICAL_HIERARCHY = NO |
|||
DIRECTORY_GRAPH = NO |
|||
DOT_IMAGE_FORMAT = svg |
|||
INTERACTIVE_SVG = YES |
|||
DOT_PATH = |
|||
DOTFILE_DIRS = |
|||
MSCFILE_DIRS = |
|||
DIAFILE_DIRS = |
|||
PLANTUML_JAR_PATH = |
|||
PLANTUML_INCLUDE_PATH = |
|||
DOT_GRAPH_MAX_NODES = 50 |
|||
MAX_DOT_GRAPH_DEPTH = 0 |
|||
DOT_TRANSPARENT = NO |
|||
DOT_MULTI_TARGETS = NO |
|||
GENERATE_LEGEND = YES |
|||
DOT_CLEANUP = YES |
|||
@ -1,82 +0,0 @@ |
|||
SRCDIR = ../src |
|||
|
|||
all: doxygen |
|||
|
|||
clean: |
|||
rm -fr me.nlohmann.json.docset html |
|||
|
|||
|
|||
##########################################################################
|
|||
# example files
|
|||
##########################################################################
|
|||
|
|||
# where are the example cpp files
|
|||
EXAMPLES = $(wildcard examples/*.cpp) |
|||
|
|||
# create output from a stand-alone example file
|
|||
%.output: %.cpp |
|||
make $(<:.cpp=) CPPFLAGS="-I $(SRCDIR)" CXXFLAGS="-std=c++11" |
|||
./$(<:.cpp=) > $@ |
|||
rm $(<:.cpp=) |
|||
|
|||
# compare created output with current output of the example files
|
|||
%.test: %.cpp |
|||
make $(<:.cpp=) CPPFLAGS="-I $(SRCDIR)" CXXFLAGS="-std=c++11" |
|||
./$(<:.cpp=) > $@ |
|||
diff $@ $(<:.cpp=.output) |
|||
rm $(<:.cpp=) $@ |
|||
|
|||
# create links to try the code online
|
|||
%.link: %.cpp |
|||
rm -fr tmp |
|||
mkdir tmp |
|||
cp $(SRCDIR)/json.hpp tmp |
|||
scripts/send_to_wandbox.py tmp $< > $@.tmp |
|||
/bin/echo -n "<a target=\"_blank\" href=\"`cat $@.tmp`\"><b>online</b></a>" > $@ |
|||
rm -fr tmp $@.tmp |
|||
|
|||
# create output from all stand-alone example files
|
|||
create_output: $(EXAMPLES:.cpp=.output) |
|||
|
|||
create_links: $(EXAMPLES:.cpp=.link) |
|||
|
|||
# check output of all stand-alone example files
|
|||
check_output: $(EXAMPLES:.cpp=.test) |
|||
|
|||
|
|||
##########################################################################
|
|||
# Doxygen HTML documentation
|
|||
##########################################################################
|
|||
|
|||
# create Doxygen documentation
|
|||
doxygen: create_output create_links |
|||
doxygen |
|||
gsed -i 's@< ObjectType, ArrayType, StringType, BooleanType, NumberIntegerType, NumberFloatType, AllocatorType >@@g' html/*.html |
|||
gsed -i 's@< ObjectType, ArrayType, StringType, BooleanType, NumberIntegerType, NumberFloatType, AllocatorType >@@g' html/*.html |
|||
gsed -i 's@< ObjectType, ArrayType, StringType, BooleanType, NumberIntegerType, NumberUnsignedType, NumberFloatType, AllocatorType >@@g' html/*.html |
|||
gsed -i 's@< ObjectType, ArrayType, StringType, BooleanType, NumberIntegerType, NumberUnsignedType, NumberFloatType, AllocatorType >@@g' html/*.html |
|||
|
|||
upload: clean doxygen check_output |
|||
cd html ; ../scripts/git-update-ghpages nlohmann/json |
|||
rm -fr html |
|||
open http://nlohmann.github.io/json/ |
|||
|
|||
|
|||
##########################################################################
|
|||
# docset
|
|||
##########################################################################
|
|||
|
|||
# create docset for Dash
|
|||
docset: create_output |
|||
cp Doxyfile Doxyfile_docset |
|||
gsed -i 's/DISABLE_INDEX = NO/DISABLE_INDEX = YES/' Doxyfile_docset |
|||
gsed -i 's/SEARCHENGINE = YES/SEARCHENGINE = NO/' Doxyfile_docset |
|||
gsed -i 's@HTML_EXTRA_STYLESHEET = css/mylayout.css@HTML_EXTRA_STYLESHEET = css/mylayout_docset.css@' Doxyfile_docset |
|||
rm -fr html *.docset |
|||
doxygen Doxyfile_docset |
|||
gsed -i 's@< ObjectType, ArrayType, StringType, BooleanType, NumberIntegerType, NumberFloatType, AllocatorType >@@g' html/*.html |
|||
gsed -i 's@< ObjectType, ArrayType, StringType, BooleanType, NumberIntegerType, NumberFloatType, AllocatorType >@@g' html/*.html |
|||
make -C html |
|||
mv html/*.docset . |
|||
gsed -i 's@<string>doxygen</string>@<string>json</string>@' me.nlohmann.json.docset/Contents/Info.plist |
|||
rm -fr Doxyfile_docset html |
|||
@ -1,26 +0,0 @@ |
|||
/* hide lengthy template information */ |
|||
.memtemplate, .memTemplParams { |
|||
display: none; |
|||
} |
|||
|
|||
/* allow compiler information to wrap */ |
|||
/* https://css-tricks.com/snippets/css/make-pre-text-wrap/ */ |
|||
pre.fragment { |
|||
white-space: pre-wrap; /* css-3 */ |
|||
white-space: -moz-pre-wrap; /* Mozilla, since 1999 */ |
|||
white-space: -pre-wrap; /* Opera 4-6 */ |
|||
white-space: -o-pre-wrap; /* Opera 7 */ |
|||
word-wrap: break-word; /* Internet Explorer 5.5+ */ |
|||
} |
|||
|
|||
td.paramname { |
|||
vertical-align: top; |
|||
} |
|||
|
|||
.ok_green { |
|||
background-color: #89C35C; |
|||
} |
|||
|
|||
.nok_throws { |
|||
background-color: #ffa500; |
|||
} |
|||
@ -1,27 +0,0 @@ |
|||
.memtemplate { |
|||
display: none; |
|||
} |
|||
|
|||
.memTemplParams { |
|||
display: none; |
|||
} |
|||
|
|||
.navtab { |
|||
display: none; |
|||
} |
|||
|
|||
#top, .footer { |
|||
display: none; |
|||
} |
|||
|
|||
td.paramname { |
|||
vertical-align: top; |
|||
} |
|||
|
|||
.ok_green { |
|||
background-color: #89C35C; |
|||
} |
|||
|
|||
.nok_throws { |
|||
background-color: #ffa500; |
|||
} |
|||
@ -1,36 +0,0 @@ |
|||
#include <json.hpp>
|
|||
|
|||
using json = nlohmann::json; |
|||
|
|||
int main() |
|||
{ |
|||
// create a JSON object
|
|||
json j = |
|||
{ |
|||
{"pi", 3.141}, |
|||
{"happy", true}, |
|||
{"name", "Niels"}, |
|||
{"nothing", nullptr}, |
|||
{ |
|||
"answer", { |
|||
{"everything", 42} |
|||
} |
|||
}, |
|||
{"list", {1, 0, 2}}, |
|||
{ |
|||
"object", { |
|||
{"currency", "USD"}, |
|||
{"value", 42.99} |
|||
} |
|||
} |
|||
}; |
|||
|
|||
// add new values
|
|||
j["new"]["key"]["value"] = {"another", "list"}; |
|||
|
|||
// count elements
|
|||
j["size"] = j.size(); |
|||
|
|||
// pretty print with indent of 4 spaces
|
|||
std::cout << std::setw(4) << j << '\n'; |
|||
} |
|||
@ -1 +0,0 @@ |
|||
<a target="_blank" href="http://melpon.org/wandbox/permlink/fYyscqrsQFtgUePA"><b>online</b></a> |
|||
@ -1,27 +0,0 @@ |
|||
{ |
|||
"answer": { |
|||
"everything": 42 |
|||
}, |
|||
"happy": true, |
|||
"list": [ |
|||
1, |
|||
0, |
|||
2 |
|||
], |
|||
"name": "Niels", |
|||
"new": { |
|||
"key": { |
|||
"value": [ |
|||
"another", |
|||
"list" |
|||
] |
|||
} |
|||
}, |
|||
"nothing": null, |
|||
"object": { |
|||
"currency": "USD", |
|||
"value": 42.99 |
|||
}, |
|||
"pi": 3.141, |
|||
"size": 9 |
|||
} |
|||
Some files were not shown because too many files changed in this diff
Write
Preview
Loading…
Cancel
Save
Reference in new issue