How to use user defined data structure correctly?
2 posters
PAT Forum :: Support :: Using PAT :: CSP and PCSP Module
Page 1 of 1
How to use user defined data structure correctly?
The manual says the following
How bad could this situation be? Does the following model contain any bug?
Thanks a lot.
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
Re: How to use user defined data structure correctly?
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 followingWarning: 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 Forum :: Support :: Using PAT :: CSP and PCSP Module
Page 1 of 1
Permissions in this forum:
You cannot reply to topics in this forum
|
|