!!
FLUENT Verification ProjectI made a properly synchronized version of the AND gate PRISM model (source at bottom of this message). The model includes a pair of counters:
c0 accumulates the AND gate outputs, and
t0 tracks the total elapsed clock cycles. The stochastic output is the ratio c0/t0.
What's interesting to me is that if I want to run the analysis for N steps, then I need to define the range for both c0 and t0 as 0..N. These variables are initialized to 0, so it's trivial to deduce that states with c0 > t or t0 > t are unreachable up to step t. But it looks like PRISM builds a gigantic state space anyway. So the model below is really slow, even if my property is just looking at the window from steps 100 to 127. If I set the maximum range of c0 and t0 at 127, it completes rapidly.
This presents a potential challenge for stochastic circuits with
regeneration, where a stream's statistics are sampled and a new stream is emitted with the same statistic. I wonder if there's a way to make this work efficiently in PRISM?
//----------------------------------
// Stochastic AND gate model
//----------------------------------
// Unipolar representation
// stochatic multiplier
//
// Expected behavior:
// Pr(c0=1) = epsilon0*epsilon1
//-----------------------------------
dtmc
const double epsilon0=0.25;
const double epsilon1=0.75;
//------------------
// Signal Sources
//------------------
module Source0
x0 : [0..1] init 0;
[event] (x0=0 | x0=1) -> epsilon0:(x0'=1) + (1-epsilon0):(x0'=0);
endmodule
// Duplicate signal source:
module Source1 = Source0 [ x0=x1, epsilon0=epsilon1 ] endmodule
//------------------
// AND gate
//------------------
module AND0
a0 : [0..1] init 0;
[event] (x0=1 & x1=1) -> (a0'=1);
[event] (x0=0 | x1=0) -> (a0'=0);
endmodule
module Counter0
c0: [0..1023] init 0;
[event] (c0 < 1023) -> (c0' = c0 + a0);
[event] (c0 = 1023) -> (c0' = c0);
endmodule
module elapsedTime
t0: [0..1023] init 0;
[event] (t0 < 1023) -> (t0' = t0 + 1);
endmodule
Property:
P=? [ F[100,127] c0/t0>0.9[i]epsilon0[/i]epsilon1 & c0/t0<1.1[i]epsilon0[/i]epsilon1 ]
