I have a couple of questions and remarks regarding the solution of exercise 7.
- Task 2a: In the policy: Why the * around the empty set? Shouldn't the regex specify the same traces if we leave out the star?
- Task 2b: The filesystem is updated as follows: mu' = mu[f1 --> 1]. Shouldnt that be mu' = mu[f1 / 1]?
- Task 2b: In the second to last sentence different symbols are used for the filesystem and the network.
- Task 3c: In the CSP expression for the policy: At the end of each line POL1 or POL2 is used. I think it should be POL1(CRIT, DEC) and POL2(CRIT, DEC)
- Task 4a i: I dont understand how the enforcer works here. From my understanding the enforcer described in the exercise text should work like the TERM enforcer only that we need to replace the STOP with logViolation(ev) --> sync --> REPLACE(CRIT). Instead the enforcer in the sample solution does not even use the logViolation event.
- Task 5b: On the exercise sheet the task is to provide the sets of traces for INT(a,b)\b and for SA(Prog, b, POL, y, ENF). The traces for SA are missing in the solution.