PAT Forum
Would you like to react to this message? Create an account in a few clicks or log in to continue.

How to use user defined data structure correctly?

2 posters

Go down

How to use user defined data structure correctly? Empty How to use user defined data structure correctly?

Post  alex2ren Fri Dec 21, 2012 5:58 am

The manual says the following
Warning: when user defined data structure is used as parameter, if the parameter in the process updates the data structure, the verification/simulation maybe wrong and un-expected. For instance the following example, i is an object used in both branch of the choice operator, so the effect of executing add1 will stay even the actual branch selected is add2. In the simulator, you will find that after executing event add2, the value of set1 can become [1,2]. The root of this cause is the pointer problem.

#import "PAT.Lib.Set";
var<Set> set1;
Q() = P(set1);
P(i) = add1{i.Add(1);} -> Skip [] add2{i.Add(2);} -> Skip;

How bad could this situation be? Does the following model contain any bug?

Code:
#import "PAT.Lib.Set"
var<Set> set1;
Q() = P(set1);
P(i) = evt1 -> {i.Add(1);} -> Skip [] evt2 -> {i.Add(2);} -> Skip;

Thanks a lot.

alex2ren

Posts : 6
Join date : 2012-12-03

Back to top Go down

How to use user defined data structure correctly? Empty Re: How to use user defined data structure correctly?

Post  pat team Mon Dec 24, 2012 11:35 pm

The main problem of this way of modeling is that you don't know what are the values in the object because of the pointer problem. so the result is not expected and it is very hard to debug the model. If you are using an object as global variable, then no need to pass it as parameter.

alex2ren wrote:The manual says the following
Warning: when user defined data structure is used as parameter, if the parameter in the process updates the data structure, the verification/simulation maybe wrong and un-expected. For instance the following example, i is an object used in both branch of the choice operator, so the effect of executing add1 will stay even the actual branch selected is add2. In the simulator, you will find that after executing event add2, the value of set1 can become [1,2]. The root of this cause is the pointer problem.

#import "PAT.Lib.Set";
var<Set> set1;
Q() = P(set1);
P(i) = add1{i.Add(1);} -> Skip [] add2{i.Add(2);} -> Skip;

How bad could this situation be? Does the following model contain any bug?

Code:
#import "PAT.Lib.Set"
var<Set> set1;
Q() = P(set1);
P(i) = evt1 -> {i.Add(1);} -> Skip [] evt2 -> {i.Add(2);} -> Skip;

Thanks a lot.

pat team
Admin

Posts : 17
Join date : 2010-02-15

http://www.comp.nus.edu.sg/~pat/

Back to top Go down

Back to top

- Similar topics

 
Permissions in this forum:
You cannot reply to topics in this forum