Query regarding synchronization between multiple users of the same system

[Shahid Ali Khan]

Respected Sir/Madam, I am working on PRISM model in which there are multiple users and different scenarios (places to visit). Where for each scenario there is a trace of the user recorded whenever he/she visit the specific place, basically my model has to keep track of all people for 3 to 4 different places. Whenever any user is problematic my model will have to warn other users, who have visited the same place in that specific time period.

I want to synchronize their movement, so my model can effectively bound the relevant traced people.

Thank you for your time.

[Shahid Ali Khan]

Getting in more details I want to synchronize some states of different modules, but it is giving me statements overlapping error. I am attaching my snippets from my code for the reference. Thank you in advance.

Description of the Code:

Here in the below code I want to synchronize the states of module user 1 e.g;  [Sync1] z2=1 &(Y21=1)&(Y11=1)  -> (q1'=1); with user 2 e.g [Sync1] z1=1 &(Y21=1)&(Y11=1)  -> (q2'=1);  and so on for user 3, 4, 5, 6, 7,......9. 

Is it the right way to do it this way, or I have to look for other way?

Code Snippet:

// Defining module for User 1
module User1

  q1 : [0..1] init 0;
  //There are total 18 states in for the user 1
  s1 : [0..22] init P1; // States for User 1
 
  // Transitions within User 1's states

  // startig from the intial state and goingin P2 with probability 1
  [] s1=P1 -> 1: (s1' = P2);
  [] s1=P2 -> 1: (s1' = P3);
  // transition from Process P3 to critical state with 0.2 probab and Plt with prob 0.8
  [] s1=P3 -> 0.2: (s1' = Crt) + 0.8: (s1' = Ptr);

  // checking the scenarios where user 1 is coming in contact with other users
 
  // For syncing contact tracing with user 2
 
  //for local transport
  [Sync1] z2=1 &(Y21=1)&(Y11=1)  -> (q1'=1);
  //for shoping center
  [Sync2] z2=1 &(Y22=1)&(Y12=1)  -> (q1'=1);
  //for restaurant
  [Sync3] z2=1 &(Y23=1)&(Y13=1)  -> (q1'=1);

 .

 .

 .

 .

 .

endmodule

module User2

  q2 : [0..1] init 0;
  //There are total 18 states in for the user 1
  s2 : [0..22] init P1; // States for User 1
 
  // Transitions within User 1's states

  // startig from the intial state and goingin P2 with probability 1
  [] s2=P1 -> 1: (s2' = P2);
  [] s2=P2 -> 1: (s2' = P3);
  // transition from Process P3 to critical state with 0.2 probab and Plt with prob 0.8
  [] s2=P3 -> 0.2: (s2' = Crt) + 0.8: (s2' = Ptr)&(q2'=0);



// checking the scenarios where user 1 is coming in contact with other users
 
  // For syncing contact tracing with user 1
 
  //for local transport
  [Sync1] z1=1 &(Y21=1)&(Y11=1)  -> (q2'=1);
  //for shoping center
  [Sync2] z1=1 &(Y22=1)&(Y12=1)  -> (q2'=1);
  //for restaurant
  [Sync3] z1=1 &(Y23=1)&(Y13=1)  -> (q2'=1);

  .

  .

  .

  .

endmodule

[Dave Parker]

Hi Shahid,

Yes, that looks like the right way to do it. Usually, your commands
labelled with e.g. Sync1 would also feature local variables from their
module (e.g. q1 or s1), but perhaps that that is not needed here.

Feel free to send the full model and the error message here, or to me
directly, and I can take a look.

Best wishes,

Dave

On 04/01/2024 07:08, Shahid Ali Khan wrote:
> Getting in more details I want to synchronize some states of different
> modules, but it is giving me statements overlapping error. I am
> attaching my snippets from my code for the reference. Thank you in advance.
>

> *Description of the Code:*
> Here in the below code I want to synchronize the states of module *user
> 1* e.g; * [Sync1] z2=1 &(Y21=1)&(Y11=1)  -> (q1'=1); *with *user 2* e.g
> *[Sync1] z1=1 &(Y21=1)&(Y11=1)  -> (q2'=1); * and so on for user 3, 4,

> 5, 6, 7,......9.
>
> Is it the right way to do it this way, or I have to look for other way?

> *
> *
>
> *Code Snippet:*

>
> // Defining module for User 1
> module User1
>
>   q1 : [0..1] init 0;
>   //There are total 18 states in for the user 1
>   s1 : [0..22] init P1; // States for User 1
>
>   // Transitions within User 1's states
>
>   // startig from the intial state and goingin P2 with probability 1
>   [] s1=P1 -> 1: (s1' = P2);
>   [] s1=P2 -> 1: (s1' = P3);
>   // transition from Process P3 to critical state with 0.2 probab and
> Plt with prob 0.8
>   [] s1=P3 -> 0.2: (s1' = Crt) + 0.8: (s1' = Ptr);
>
>   // checking the scenarios where user 1 is coming in contact with
> other users
>
>   // For syncing contact tracing with user 2
>

> *//for local transport

>   [Sync1] z2=1 &(Y21=1)&(Y11=1)  -> (q1'=1);
>   //for shoping center
>   [Sync2] z2=1 &(Y22=1)&(Y12=1)  -> (q1'=1);
>   //for restaurant

>   [Sync3] z2=1 &(Y23=1)&(Y13=1)  -> (q1'=1);*

>  .
>  .
>  .
>  .
>  .
> endmodule
>
>
> module User2
>
>   q2 : [0..1] init 0;
>   //There are total 18 states in for the user 1
>   s2 : [0..22] init P1; // States for User 1
>
>   // Transitions within User 1's states
>
>   // startig from the intial state and goingin P2 with probability 1
>   [] s2=P1 -> 1: (s2' = P2);
>   [] s2=P2 -> 1: (s2' = P3);
>   // transition from Process P3 to critical state with 0.2 probab and
> Plt with prob 0.8
>   [] s2=P3 -> 0.2: (s2' = Crt) + 0.8: (s2' = Ptr)&(q2'=0);
>
>
>
> // checking the scenarios where user 1 is coming in contact with other users
>
>   // For syncing contact tracing with user 1

> *

>   //for local transport
>   [Sync1] z1=1 &(Y21=1)&(Y11=1)  -> (q2'=1);
>   //for shoping center
>   [Sync2] z1=1 &(Y22=1)&(Y12=1)  -> (q2'=1);
>   //for restaurant

>   [Sync3] z1=1 &(Y23=1)&(Y13=1)  -> (q2'=1);*
> *  .*
> *  .*
> *  .*
> *  .*

> endmodule
>
>
> On Monday, January 1, 2024 at 1:01:13 PM UTC+5 Shahid Ali Khan wrote:
>
> Respected Sir/Madam, I am working on PRISM model in which there are
> multiple users and different scenarios (places to visit). Where for
> each scenario there is a trace of the user recorded whenever he/she
> visit the specific place, basically my model has to keep track of
> all people for 3 to 4 different places. Whenever any user is
> problematic my model will have to warn other users, who have visited
> the same place in that specific time period.
> I want to synchronize their movement, so my model can effectively
> bound the relevant traced people.
>
> Thank you for your time.
>

> --
> 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
> <mailto:prismmodelchec...@googlegroups.com>.
> To view this discussion on the web, visit
> https://groups.google.com/d/msgid/prismmodelchecker/6f64b900-70b0-4351-b394-398bdc01dbb8n%40googlegroups.com <https://groups.google.com/d/msgid/prismmodelchecker/6f64b900-70b0-4351-b394-398bdc01dbb8n%40googlegroups.com?utm_medium=email&utm_source=footer>.

[Shahid Ali Khan]

Respected Dave Parker, Thank you for your kind reply.

I have tried another way to solve my problem and luckily, I am successful so far. I will keep in touch with you to learn more about PRISM in future.

Regards, 

Shahid Ali