Update Alloy for Alloy 6 (PR #1963) manual cherry-pick

2 files changed, 48 insertions, 48 deletions

diff --git a/tests/examplefiles/alloy/example.als b/tests/examplefiles/alloy/example.als
index 3a5ab82b..c1a6d27e 100644
--- a/tests/examplefiles/alloy/example.als
+++ b/tests/examplefiles/alloy/example.als
@@ -32,8 +32,8 @@ module examples/systems/views
  *
  * As a terminological convention, when there are two
  * complementary view relationships, we will give them types
- * t and t'. For example, KeySetView propagates from map to
- * set, and KeySetView' propagates from set to map.
+ * t and t". For example, KeySetView propagates from map to
+ * set, and KeySetView" propagates from set to map.
  *
  * author: Daniel Jackson
  */
@@ -76,12 +76,12 @@ sig SetRef extends Ref {}
 fact {State.obj[SetRef] in Set}
 
 abstract sig ViewType {}
-one sig KeySetView, KeySetView', IteratorView extends ViewType {}
+one sig KeySetView, KeySetView", IteratorView extends ViewType {}
 fact ViewTypes {
   State.views[KeySetView] in MapRef -> SetRef
-  State.views[KeySetView'] in SetRef -> MapRef
+  State.views[KeySetView"] in SetRef -> MapRef
   State.views[IteratorView] in IteratorRef -> SetRef
-  all s: State | s.views[KeySetView] = ~(s.views[KeySetView'])
+  all s: State | s.views[KeySetView] = ~(s.views[KeySetView"])
   }
 
 /**
@@ -107,20 +107,20 @@ pred allocates [pre, post: State, rs: set Ref] {
   }
 
 /** 
- * models frame condition that limits change to view object from v to v' when backing object changes to b'
+ * models frame condition that limits change to view object from v to v" when backing object changes to b"
  */
-pred viewFrame [t: ViewType, v, v', b': Object] {
-  t in KeySetView => v'.elts = dom [b'.map]
-  t in KeySetView' => b'.elts = dom [v'.map]
-  t in KeySetView' => (b'.elts) <: (v.map) = (b'.elts) <: (v'.map)
-  t in IteratorView => v'.elts = b'.left + b'.done
+pred viewFrame [t: ViewType, v, v", b": Object] {
+  t in KeySetView => v".elts = dom [b".map]
+  t in KeySetView" => b".elts = dom [v".map]
+  t in KeySetView" => (b".elts) <: (v.map) = (b".elts) <: (v".map)
+  t in IteratorView => v".elts = b".left + b".done
   }
 
 pred MapRef.keySet [pre, post: State, setRefs: SetRef] {
   post.obj[setRefs].elts = dom [pre.obj[this].map]
   modifies [pre, post, none]
   allocates [pre, post, setRefs]
-  post.views = pre.views + KeySetView->this->setRefs + KeySetView'->setRefs->this
+  post.views = pre.views + KeySetView->this->setRefs + KeySetView"->setRefs->this
   }
 
 pred MapRef.put [pre, post: State, k, v: Ref] {
@@ -141,10 +141,10 @@ pred SetRef.iterator [pre, post: State, iterRef: IteratorRef] {
   }
 
 pred IteratorRef.remove [pre, post: State] {
-  let i = pre.obj[this], i' = post.obj[this] {
-    i'.left = i.left
-    i'.done = i.done - i.lastRef
-    no i'.lastRef
+  let i = pre.obj[this], i" = post.obj[this] {
+    i".left = i.left
+    i".done = i.done - i.lastRef
+    no i".lastRef
     }
   modifies [pre,post,this]
   allocates [pre, post, none]
@@ -152,11 +152,11 @@ pred IteratorRef.remove [pre, post: State] {
   }
 
 pred IteratorRef.next [pre, post: State, ref: Ref] {
-  let i = pre.obj[this], i' = post.obj[this] {
+  let i = pre.obj[this], i" = post.obj[this] {
     ref in i.left
-    i'.left = i.left - ref
-    i'.done = i.done + ref
-    i'.lastRef = ref
+    i".left = i.left - ref
+    i".done = i.done + ref
+    i".lastRef = ref
     }
   modifies [pre, post, this]
   allocates [pre, post, none]
diff --git a/tests/examplefiles/alloy/example.als.output b/tests/examplefiles/alloy/example.als.output
index fc7d42b3..bda535e2 100644
--- a/tests/examplefiles/alloy/example.als.output
+++ b/tests/examplefiles/alloy/example.als.output
@@ -9,7 +9,7 @@
 
 '\n'          Text.Whitespace
 
-"/*\n * Model of views in object-oriented programming.\n *\n * Two object references, called the view and the backing,\n * are related by a view mechanism when changes to the\n * backing are automatically propagated to the view. Note\n * that the state of a view need not be a projection of the\n * state of the backing; the keySet method of Map, for\n * example, produces two view relationships, and for the\n * one in which the map is modified by changes to the key\n * set, the value of the new map cannot be determined from\n * the key set. Note that in the iterator view mechanism,\n * the iterator is by this definition the backing object,\n * since changes are propagated from iterator to collection\n * and not vice versa. Oddly, a reference may be a view of\n * more than one backing: there can be two iterators on the\n * same collection, eg. A reference cannot be a view under\n * more than one view type.\n *\n * A reference is made dirty when it is a backing for a view\n * with which it is no longer related by the view invariant.\n * This usually happens when a view is modified, either\n * directly or via another backing. For example, changing a\n * collection directly when it has an iterator invalidates\n * it, as does changing the collection through one iterator\n * when there are others.\n *\n * More work is needed if we want to model more closely the\n * failure of an iterator when its collection is invalidated.\n *\n * As a terminological convention, when there are two\n * complementary view relationships, we will give them types\n * t and t'. For example, KeySetView propagates from map to\n * set, and KeySetView' propagates from set to map.\n *\n * author: Daniel Jackson\n */" Comment.Multiline
+'/*\n * Model of views in object-oriented programming.\n *\n * Two object references, called the view and the backing,\n * are related by a view mechanism when changes to the\n * backing are automatically propagated to the view. Note\n * that the state of a view need not be a projection of the\n * state of the backing; the keySet method of Map, for\n * example, produces two view relationships, and for the\n * one in which the map is modified by changes to the key\n * set, the value of the new map cannot be determined from\n * the key set. Note that in the iterator view mechanism,\n * the iterator is by this definition the backing object,\n * since changes are propagated from iterator to collection\n * and not vice versa. Oddly, a reference may be a view of\n * more than one backing: there can be two iterators on the\n * same collection, eg. A reference cannot be a view under\n * more than one view type.\n *\n * A reference is made dirty when it is a backing for a view\n * with which it is no longer related by the view invariant.\n * This usually happens when a view is modified, either\n * directly or via another backing. For example, changing a\n * collection directly when it has an iterator invalidates\n * it, as does changing the collection through one iterator\n * when there are others.\n *\n * More work is needed if we want to model more closely the\n * failure of an iterator when its collection is invalidated.\n *\n * As a terminological convention, when there are two\n * complementary view relationships, we will give them types\n * t and t". For example, KeySetView propagates from map to\n * set, and KeySetView" propagates from set to map.\n *\n * author: Daniel Jackson\n */' Comment.Multiline
 '\n'          Text.Whitespace
 
 '\n'          Text.Whitespace
@@ -407,7 +407,7 @@
 'KeySetView'  Name
 ','           Punctuation
 ' '           Text.Whitespace
-"KeySetView'" Name
+'KeySetView"' Name
 ','           Punctuation
 ' '           Text.Whitespace
 'IteratorView' Name
@@ -449,7 +449,7 @@
 '.'           Operator
 'views'       Name
 '['           Operator
-"KeySetView'" Name
+'KeySetView"' Name
 ']'           Operator
 ' '           Text.Whitespace
 'in'          Operator.Word
@@ -503,7 +503,7 @@
 '.'           Operator
 'views'       Name
 '['           Operator
-"KeySetView'" Name
+'KeySetView"' Name
 ']'           Operator
 ')'           Operator
 '\n'          Text.Whitespace
@@ -837,7 +837,7 @@
 
 '\n'          Text.Whitespace
 
-"/** \n * models frame condition that limits change to view object from v to v' when backing object changes to b'\n */" Comment.Multiline
+'/** \n * models frame condition that limits change to view object from v to v" when backing object changes to b"\n */' Comment.Multiline
 '\n'          Text.Whitespace
 
 'pred'        Keyword
@@ -854,10 +854,10 @@
 'v'           Name
 ','           Punctuation
 ' '           Text.Whitespace
-"v'"          Name
+'v"'          Name
 ','           Punctuation
 ' '           Text.Whitespace
-"b'"          Name
+'b"'          Name
 ':'           Punctuation
 ' '           Text.Whitespace
 'Object'      Name
@@ -876,7 +876,7 @@
 '='           Operator
 '>'           Operator
 ' '           Text.Whitespace
-"v'"          Name
+'v"'          Name
 '.'           Operator
 'elts'        Name
 ' '           Text.Whitespace
@@ -885,7 +885,7 @@
 'dom'         Name
 ' '           Text.Whitespace
 '['           Operator
-"b'"          Name
+'b"'          Name
 '.'           Operator
 'map'         Name
 ']'           Operator
@@ -896,12 +896,12 @@
 ' '           Text.Whitespace
 'in'          Operator.Word
 ' '           Text.Whitespace
-"KeySetView'" Name
+'KeySetView"' Name
 ' '           Text.Whitespace
 '='           Operator
 '>'           Operator
 ' '           Text.Whitespace
-"b'"          Name
+'b"'          Name
 '.'           Operator
 'elts'        Name
 ' '           Text.Whitespace
@@ -910,7 +910,7 @@
 'dom'         Name
 ' '           Text.Whitespace
 '['           Operator
-"v'"          Name
+'v"'          Name
 '.'           Operator
 'map'         Name
 ']'           Operator
@@ -921,13 +921,13 @@
 ' '           Text.Whitespace
 'in'          Operator.Word
 ' '           Text.Whitespace
-"KeySetView'" Name
+'KeySetView"' Name
 ' '           Text.Whitespace
 '='           Operator
 '>'           Operator
 ' '           Text.Whitespace
 '('           Operator
-"b'"          Name
+'b"'          Name
 '.'           Operator
 'elts'        Name
 ')'           Operator
@@ -944,7 +944,7 @@
 '='           Operator
 ' '           Text.Whitespace
 '('           Operator
-"b'"          Name
+'b"'          Name
 '.'           Operator
 'elts'        Name
 ')'           Operator
@@ -953,7 +953,7 @@
 ':'           Punctuation
 ' '           Text.Whitespace
 '('           Operator
-"v'"          Name
+'v"'          Name
 '.'           Operator
 'map'         Name
 ')'           Operator
@@ -969,19 +969,19 @@
 '='           Operator
 '>'           Operator
 ' '           Text.Whitespace
-"v'"          Name
+'v"'          Name
 '.'           Operator
 'elts'        Name
 ' '           Text.Whitespace
 '='           Operator
 ' '           Text.Whitespace
-"b'"          Name
+'b"'          Name
 '.'           Operator
 'left'        Name
 ' '           Text.Whitespace
 '+'           Operator
 ' '           Text.Whitespace
-"b'"          Name
+'b"'          Name
 '.'           Operator
 'done'        Name
 '\n'          Text.Whitespace
@@ -1092,7 +1092,7 @@
 ' '           Text.Whitespace
 '+'           Operator
 ' '           Text.Whitespace
-"KeySetView'" Name
+'KeySetView"' Name
 '->'          Operator
 'setRefs'     Name
 '->'          Operator
@@ -1370,7 +1370,7 @@
 ']'           Operator
 ','           Punctuation
 ' '           Text.Whitespace
-"i'"          Name
+'i"'          Name
 ' '           Text.Whitespace
 '='           Operator
 ' '           Text.Whitespace
@@ -1385,7 +1385,7 @@
 '\n'          Text.Whitespace
 
 '    '        Text.Whitespace
-"i'"          Name
+'i"'          Name
 '.'           Operator
 'left'        Name
 ' '           Text.Whitespace
@@ -1397,7 +1397,7 @@
 '\n'          Text.Whitespace
 
 '    '        Text.Whitespace
-"i'"          Name
+'i"'          Name
 '.'           Operator
 'done'        Name
 ' '           Text.Whitespace
@@ -1417,7 +1417,7 @@
 '    '        Text.Whitespace
 'no'          Keyword
 ' '           Text.Whitespace
-"i'"          Name
+'i"'          Name
 '.'           Operator
 'lastRef'     Name
 '\n'          Text.Whitespace
@@ -1510,7 +1510,7 @@
 ']'           Operator
 ','           Punctuation
 ' '           Text.Whitespace
-"i'"          Name
+'i"'          Name
 ' '           Text.Whitespace
 '='           Operator
 ' '           Text.Whitespace
@@ -1535,7 +1535,7 @@
 '\n'          Text.Whitespace
 
 '    '        Text.Whitespace
-"i'"          Name
+'i"'          Name
 '.'           Operator
 'left'        Name
 ' '           Text.Whitespace
@@ -1551,7 +1551,7 @@
 '\n'          Text.Whitespace
 
 '    '        Text.Whitespace
-"i'"          Name
+'i"'          Name
 '.'           Operator
 'done'        Name
 ' '           Text.Whitespace
@@ -1567,7 +1567,7 @@
 '\n'          Text.Whitespace
 
 '    '        Text.Whitespace
-"i'"          Name
+'i"'          Name
 '.'           Operator
 'lastRef'     Name
 ' '           Text.Whitespace