//Insert declarations of global clocks, variables, constants and channels.
int[0,2000] logSize1, logSize2, logSize3, logSizeFiltered, userNum, detected, y1, y2, y3, totalSize;
urgent chan filter, add, stored;
const F_RATE_HIGH 5, AVE_ACC_NUM 70, PRIOD_LOG_CHECK 7;
LogSize
int[0,2000] logSize, detected, y, totalSize, logSizeFiltered; urgent chan filter, add
//Insert local declarations of clocks, variables and constants.
LogonEventFilteredCollectedRecorded
StaticPolicy2int[0,2000] logSizeFiltered, detectedNo; urgent chan filteridleobjectFilterSecMngint[0,2000] totalSize; urgent chan addTotaledCompleteTiredGiveUp//Insert process assignments.
LogSizeU1 := LogSize(logSize1, detected, y1, totalSize, logSizeFiltered, filter, add);
LogSizeU2 := LogSize(logSize2, detected, y2, totalSize, logSizeFiltered, filter, add);
LogSizeU3 := LogSize(logSize3, detected, y3, totalSize, logSizeFiltered, filter, add);
StaticPolicy2 := StaticPolicy2(logSizeFiltered, detected, filter);
SecMng:= SecMng(totalSize, add);
//Edit system definition.
system LogSizeU1, LogSizeU2, LogSizeU3, StaticPolicy2, SecMng;