prog

example/pseudocycle.prism

@@ -25,4 +25,4 @@ endinvariant
 
 endmodule
 
-label "accepting" = (s!=6)&(s!=4);
+label "accepting" = (s!=6)&(s!=4)&(s!=0);

src/OutFormat.ml

@@ -196,11 +196,15 @@ let plot_of_style style store_traj ntraj data =
            "set xrange [-0.5 :*]\n\
             binwidth = 0.1\n\
             binstart= -0.5\n\
+            set ytics nomirror\n\
+            set y2tics\n\
             set boxwidth 0.9*binwidth\n\
             set style fill solid 0.5\n\
             plot '%s' i 0 u \
             (binwidth*(floor(($2-binstart)/binwidth)+0.5)+binstart):(1.0) \
-            smooth freq w boxes\n"
+            smooth freq w boxes title 'size', '' i 0 u \
+            (binwidth*(floor(($3-binstart)/binwidth)+0.5)+binstart):(1.0) \
+            smooth freq w boxes axes x1y1 title 'duration'\n"
            data)
   (* fprintf gnuplot "set xrange [-0.5 :*]\nbinwidth = 1.0\nbinstart= -0.5\nset boxwidth 0.9*binwidth\nset style fill solid 0.5\n";
       fprintf gnuplot "plot '%s' i 0 u (binwidth*(floor(($1-binstart)/binwidth)+0.5)+binstart):(1.0) smooth freq w boxes\n" data*)

src/Semantic.ml

@@ -269,11 +269,14 @@ struct
             |>>| true
           then (0, -.t_length -. 1.0, 0.0, smp_full)
           else
-            let n, size, duration =
-              Samp.sample ~out_style:t_length ~max_iter:100 ~boltz ?seed
-                ~sampler:Low_disc_sampler.random rgp2 template n
-            in
-            (n, size, duration, smp_full)
+            try
+              let n, size, duration =
+                Samp.sample ~out_style:t_length ~max_iter:100 ~boltz ?seed
+                  ~sampler:Low_disc_sampler.random rgp2 template n
+              in
+              (n, size, duration, smp_full)
+            with Sampling.SMC_Not_terminating ->
+              (1, infinity, infinity, smp_full)
         in
 
         let b, v, smp_full =

src/sampling.ml

@@ -382,6 +382,8 @@ struct
     r
 end
 
+exception SMC_Not_terminating
+
 module MakeSMCMonitor
     (Bt : ZoneGraphInput.BoundType)
     (W : Polynomial.WeightStructure)
@@ -409,6 +411,7 @@ struct
 
   let up_trans (_, mon_state) time _ _ =
     let (size, duration), glob = !mon_state in
+    if size > 10000 then raise SMC_Not_terminating;
     mon_state := ((size + 1, duration +. time), glob)
 
   let up_state _ ?smp:_ _ _ = None