// nand multiplex system (N number of lines each input is split into) // gxn/dxp 20/03/03 // modelling error: U performs a random choice with replacement (of the outputs of the previous stage) dtmc const int N; // number of inputs in each bundle const int K; // number of restorative stages const int M = 2*K+1; // total number of multiplexing units const double perr; // probability nand works correctly const double prob1; // probability initial inputs are stimulated // model whole system as a single module by resuing variables // to decrease the state space module multiplex u : [1..M]; // number of stages c : [0..N]; // counter (number of copies of the nand done) s : [0..4]; // local state // 0 - initial state // 1 - set x inputs // 2 - set y inputs // 3 - set outputs // 4 - done z : [0..N]; // number of new outputs equal to 1 zold : [0..N] init floor(N*prob1); // number of old outputs equal to 1 // initially probability that an output is stimulated is prob1 x : [0..1]; // value of first input y : [0..1]; // value of second input [] s=0 & (c<N) -> (s'=1); // do next nand if have not done N yet [] s=0 & (c=N) & (u<M) -> (s'=1) & (zold'=z) & (z'=0) & (u'=u+1) & (c'=0); // move on to next u if not finished [] s=0 & (c=N) & (u=M) -> (s'=4) & (zold'=0) & (x'=0) & (y'=0); // finished (so reset unused variables) // choose x and y randomly from selection (have zold stimulated inputs) [] s=1 & zold<N & zold>0 -> zold/N : (x'=1) & (s'=2) + (N-zold)/N : (x'=0) & (s'=2); [] s=1 & zold=N -> 1 : (x'=1) & (s'=2); [] s=1 & zold=0 -> 1 : (x'=0) & (s'=2); [] s=2 & zold<N & zold>0 -> zold/N : (y'=1) & (s'=3) + (N-zold)/N : (y'=0) & (s'=3); [] s=2 & zold=N -> 1 : (y'=1) & (s'=3); [] s=2 & zold=0 -> 1 : (y'=0) & (s'=3); // use nad gate [] s=3 & c<N & z<N -> (1-perr) : (z'=z+(1-x*y)) & (s'=0) & (c'=c+1) & (x'=0) & (y'=0) // not faulty + perr : (z'=z+(x*y) ) & (s'=0) & (c'=c+1) & (x'=0) & (y'=0); // von neumann fault // finished [] s=4 -> true; endmodule // reward structure - final value of gate rewards [] s=0 & (c=N) & (u=M) : z/N; endrewards