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