====
C2
====
Uppaal:
(14900 runs) Pr(<> ...) in [0.326093,0.346093] with confidence 0.99.
(14740 runs) Pr(<> ...) in [0.661112,0.681111] with confidence 0.99.

** Note: Technically not fully supported by UPPAAL, as it has to be deterministic

Modes:
Analysis results for C2.modest
Runs: 26492
Time: 0.4 s

+ Property p12_min
  Mean: 0.669866666666667

+ Property p3_min
  Mean: 0.330133333333333
  
====
C3
====
(12486 runs) Pr(<> ...) in [0.741466,0.761465] with confidence 0.99.

Modes:
Analysis results for C3_point.modest
Runs: 26492
Time: 0.4 s

+ Property p1_min
  Mean: 1

====
C4
====
Uppaal:
(7893 runs) Pr(<> ...) in [0.853836,0.873835] with confidence 0.99.
** Note: exponential distribution (PDF) offset by lower bound of guard

Modes:
** Note: different semantics: invalid sample is deadlock
** Note: run this experiment on Windows, Mono seems to have a bug with the RNG
Analysis results for C4.modest
Runs: 26492
Time: 0.3 s

+ Property p1_min
  Mean: 0.528310433338366

====
C5_Zeno
====
Uppaal:
Pr[<= 7](<> q.q2) Run exceeds 100000 steps: probably Zeno behavior.
** Note: special behavior for point intervals at invariant and property boundaries

Modes:
C5_Zeno.modest: error: Run length exceeded.

====
C5_Actionlock
====
Uppaal:
(263 runs) Pr(<> ...) in [0.980056,1] with confidence 0.99.

Modes:
Analysis results for C5_Actionlock.modest
Runs: 26492
Time: 0.3 s

+ Property q1_min
  Mean: 1

====
C5_deadlock
====
Uppaal:
(263 runs) Pr(<> ...) in [0.980056,1] with confidence 0.99.

Modes:
Analysis results for C5_deadlock.modest
Runs: 26492
Time: 0.3 s

+ Property r1_min
  Mean: 1



====
C1C3
====
Uppaal:
Pr[<= 5] (<> p.p1) Location p.p0 [ x=0 #time=0 ] is time-locked.
Pr[<= 5] (<> q.q1) Location p.p0 [ x=0 #time=0 ] is time-locked.

Modes:
Analysis results for C1C3.modest
Runs: 26492
Time: 0.4 s

+ Property and_min
  Mean: 1

+ Property or_min
  Mean: 0

** Note: the invariant on the target state cannot be fully represented in Modest
  
====
C2C3
====
Uppaal:
** Note: Can technically not be represented by NPTA semantics (upper bound in guard)

(10733 runs) Pr(<> ...) in [0.789363,0.809363] with confidence 0.99.
(10598 runs) Pr(<> ...) in [0.18725,0.207249] with confidence 0.99.

Modes:
Analysis results for C2C3.modest
Runs: 26492
Time: 0.3 s

+ Property p1_min
  Mean: 1

+ Property p2_min
  Mean: 0

====
C2C3_disjoint
====
Uppaal:
(10891 runs) Pr(<> ...) in [0.194611,0.21461] with confidence 0.99.
(10498 runs) Pr(<> ...) in [0.795253,0.815251] with confidence 0.99.

Modest:
Analysis results for C2C3_disjoint.modest
Runs: 26492
Time: 0.3 s

+ Property q1_min
  Mean: 1

+ Property q2_min
  Mean: 0


====
C2C3_overlap
====
Uppaal:
(6015 runs) Pr(<> ...) in [0.890761,0.910758] with confidence 0.99.
(6316 runs) Pr(<> ...) in [0.0949558,0.114956] with confidence 0.99.

Modest:
Analysis results for C2C3_overlap.modest
Runs: 26492
Time: 0.3 s

+ Property r1_min
  Mean: 1

+ Property r2_min
  Mean: 0