fix: alloy6 language migration (#1803)

The alloy tool in which the formal memory model is specified has been updated to version 6. The single quote has been introduced as a new operator thus the old notation no longer compiles. This ensures the formal memory spec still works under the new alloy 6. Signed-off-by: Tianrui Wei <[email protected]>
riscv · Jan 15, 2025 · 97273ec · 97273ec
1 parent 866cfb8
commit 97273ec
Showing 1 changed file with 1 addition and 1 deletion.
diff --git a/src/mm-formal.adoc b/src/mm-formal.adoc
@@ -243,7 +243,7 @@ pred restrict_to_current_encodings {
 // =Alloy shortcuts=
 pred acyclic[rel: Event->Event] { no iden & ^rel }
 pred total[rel: Event->Event, bag: Event] {
-  all disj e, e': bag | e->e' in rel + ~rel
+  all disj e, f: bag | e->f in rel + ~rel
   acyclic[rel]
 }
 ....