// 971204, Arne, Fredrik, Kim & Paul.
// Fairmont Hotel, San Francisco.
// Test Data from Feb. 18, 2003 by Aglais Co. http://aglaia.cc/profile.html
const LEAKY_NUM 108, WORK1_ACC_NUM 60, WORK2_ACC_NUM 84, WORK3_ACC_NUM 65, W1_ACC_NUM 88, W2_ACC_NUM 95, W3_ACC_NUM 101, W4_ACC_NUM 108;
int[0,150] accNo1, accNo2, accNo3, detected, checked, detectedNo;
urgent chan check, w0, w1, w2, w3, w4;
UserAcc
int[0,150] accNo, checked, detected, detectedNo; const workAccNum; urgent chan check, w0, w1, w2, w3, w4
idle
Logon
AccessDetectionMngReviewStopWorkLeakFinishWorkwarnMessageLogoffMngInspect
DynamicPolicy1 int[0,150] checked, detected, detectedNo; urgent chan w0, w1, w2, w3, w4idleUser1 := UserAcc(accNo1, checked, detected, detectedNo, WORK1_ACC_NUM, check, w0, w1, w2, w3, w4);
User2 := UserAcc(accNo2, checked, detected, detectedNo, WORK2_ACC_NUM, check, w0, w1, w2, w3, w4);
User3 := UserAcc(accNo3, checked, detected, detectedNo, WORK3_ACC_NUM, check, w0, w1, w2, w3, w4);
DynamicPolicy1 := DynamicPolicy1(checked, detected, detectedNo, w0, w1, w2, w3, w4);
system User1, User2, User3, DynamicPolicy1;