CS4211 AY20/21 Semester 1
All error trails can be performed with the iSpin Simulate tab. The necessary pml.trail files are already included, so verification does not need to be run again.
If you would like to perform verification, all files label LTL claims as "q", for ease of use.
|-assignment/
| |- Question1/
| | |- Question1_template.pml: Original template + my LTL property
| | |- Question1_template.pml.trail: Error trail for LTL on Question1_template.pml
| | |- Question1.pml: Augmented protocol + LTL
| |- Question2/
| | |- Question2.pml: Model + LTL
| | |- Question2.pml.trail: Error trail for LTL on Question2.pml
| |- Question3/
| | |- Question3.pml: Model + LTL
| | |- Question3.pml.trail: Error trail for LTL on Question3.pml
| | |- Question3_modified.pml: Augmented model + LTL
|- README.md
|- instructions.pdf
|- report.pdf
Note: My attempts at Question 1 and 2 are fine (albeit not the cleanest); Question 3 is an absolute dumpster fire. Peruse at your own risk.