MCS peer review

Daan Vanoverloop 1 month ago
parent dce7c0122e
commit 87a66e84de
  1. 17

@ -0,0 +1,17 @@
- It works.
- Reasonably easy to read.
- Well documented.
- Why introduce `floor` and `door` predicates when `ElPosition` and `ElDoorState` functions are already given?
Using inertia rules and causes on functions is easier than using them on predicates (see page 113 in course notes).
- Using material implication to define `ElPosition` and `ElDoorState` might be risky as it could produce unwanted results if `floor` and `door` are not defined for certain values of `t`, `f` and `d`.
- Good use of helper predicates
- I am unable to prove the invariants, possibly caused by the use of `t - 1`?
- It works.
- Easy to read and well documented.
- `URPartial` looks like a weird solution to a weird problem.
- It is considered a "common mistake" to not use preconditions/putting them inside the definitions, but I didn't do it either and disagree that this is a mistake. The code still looks very readable without them and they are mainly applicable in situations where there are multiple solutions to the problem, which is not the case here.