Modules and delays

[Bennaceur Walid]

Greetings PRISM community!

I am new to PRISM and I have a question please.

Let's consider the following two models:

1. The first model: 3 sensors in the same module

ctmc
const double lambda_s = 1/(30*24*60*60); 
module sensors
        s : [0..3] init 3; // number of sensors working
        [failure] s>1 -> s*lambda_s : (s'=s-1); // failure of a single sensor        
endmodule

 

2. The second model: 3 sensors defined separately 

ctmc

const double lambda_s = 1/(30*24*60*60); // 1 month
module sensor1
        s1 : [0..1] init 1;
        [failure_s1] s1=1 -> lambda_s : (s1'=0);
endmodule

module sensor2
        s2 : [0..1] init 1;
        [failure_s2] s2=1 -> lambda_s : (s2'=0);
endmodule

module sensor3
        s3 : [0..1] init 1;
        [failure_s3] s3=1 -> lambda_s : (s3'=0);
endmodule

From my point of view the two models are equivalent, but my question concerns  the delays. I have the impression that in the first model the delays are dependent, i.e. when the first sensor fails after a certain delay (randomly fired from an exponential distribution with rate 3*lambda), the second sensor follows with rate 2*lambda and then the third one. But in the second model each delay is independent of the other.

Does anyone have an explanation for this, please?

Thank you in advance.

Walid.

[Gethin Norman]

Hi Walid,

you can consider the first model as an abstraction of the second where the first just counts the number of sensors that have failed rather than which specific sensor has failed (s=1 means one sensor has failed rather than sensor 1 has failed).

When all sensors are operational in the first model one of the three sensors will fail at the rate 3*lambda_s
When all sensors are operationalin the second model one of the sensors will fail with rate 3*lambda_s where the probability it is sensor 1, 2 or 3 is each 1/3.

Then after a sensor has failed in the first model a second sensor will fail with rate 2*lambda_s
Then after a sensor has failed in the second:

- if sensor 1 failed, then either sensor 2 or 3 will fail with rate 2*lambda_s where the probability it is either is 1/2
- if sensor 2 failed, then either sensor 1 or 3 will fail with rate 2*lambda_s where the probability it is either is 1/2
- if sensor 3 failed, then either sensor 1 or 2 will fail with rate 2*lambda_s where the probability it is either is 1/2

The probabilities in the second mode come from the race condition, see for example http://www.prismmodelchecker.org/bibitem.php?key=KNP07a for more details.

I hope this helps to clarify things.

thanks

Gethin

> --
> You received this message because you are subscribed to the Google Groups "PRISM model checker" group.
> To unsubscribe from this group and stop receiving emails from it, send an email to prismmodelchec...@googlegroups.com.
> To view this discussion on the web, visit https://groups.google.com/d/msgid/prismmodelchecker/3bd7226a-b9b7-4805-b143-b0397867583dn%40googlegroups.com.

[Bennaceur Walid]

Hi Gethin,

Thank you very much for this clarification.

Sincerely,

Walid 

To view this discussion on the web, visit https://groups.google.com/d/msgid/prismmodelchecker/32AE299D-3A5F-4576-9DEA-26861275FCB0%40gmail.com.