From 67ea00875ad10bb356b7b3170f77dcb179f66f0f Mon Sep 17 00:00:00 2001 From: Hillel Date: Mon, 29 Nov 2021 11:45:44 -0600 Subject: [PATCH] Update the alloy golden test Alloy 6 recommends changing `'` in legacy specs to `"`. Since this is a breaking change, the golden test is updated to reflect that. --- tests/examplefiles/alloy/example.als | 40 +++++++-------- tests/examplefiles/alloy/example.als.output | 56 ++++++++++----------- 2 files changed, 48 insertions(+), 48 deletions(-) diff --git a/tests/examplefiles/alloy/example.als b/tests/examplefiles/alloy/example.als index 3a5ab82bf8..c1a6d27e26 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 3de5573717..88859f8d73 100644 --- a/tests/examplefiles/alloy/example.als.output +++ b/tests/examplefiles/alloy/example.als.output @@ -9,7 +9,7 @@ '\n' Text -"/*\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 '\n' Text @@ -407,7 +407,7 @@ 'KeySetView' Name ',' Punctuation ' ' Text -"KeySetView'" Name +'KeySetView"' Name ',' Punctuation ' ' Text 'IteratorView' Name @@ -449,7 +449,7 @@ '.' Operator 'views' Name '[' Operator -"KeySetView'" Name +'KeySetView"' Name ']' Operator ' ' Text 'in' Operator.Word @@ -503,7 +503,7 @@ '.' Operator 'views' Name '[' Operator -"KeySetView'" Name +'KeySetView"' Name ']' Operator ')' Operator '\n' Text @@ -837,7 +837,7 @@ '\n' Text -"/** \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 'pred' Keyword @@ -854,10 +854,10 @@ 'v' Name ',' Punctuation ' ' Text -"v'" Name +'v"' Name ',' Punctuation ' ' Text -"b'" Name +'b"' Name ':' Punctuation ' ' Text 'Object' Name @@ -876,7 +876,7 @@ '=' Operator '>' Operator ' ' Text -"v'" Name +'v"' Name '.' Operator 'elts' Name ' ' Text @@ -885,7 +885,7 @@ 'dom' Name ' ' Text '[' Operator -"b'" Name +'b"' Name '.' Operator 'map' Name ']' Operator @@ -896,12 +896,12 @@ ' ' Text 'in' Operator.Word ' ' Text -"KeySetView'" Name +'KeySetView"' Name ' ' Text '=' Operator '>' Operator ' ' Text -"b'" Name +'b"' Name '.' Operator 'elts' Name ' ' Text @@ -910,7 +910,7 @@ 'dom' Name ' ' Text '[' Operator -"v'" Name +'v"' Name '.' Operator 'map' Name ']' Operator @@ -921,13 +921,13 @@ ' ' Text 'in' Operator.Word ' ' Text -"KeySetView'" Name +'KeySetView"' Name ' ' Text '=' Operator '>' Operator ' ' Text '(' Operator -"b'" Name +'b"' Name '.' Operator 'elts' Name ')' Operator @@ -944,7 +944,7 @@ '=' Operator ' ' Text '(' Operator -"b'" Name +'b"' Name '.' Operator 'elts' Name ')' Operator @@ -953,7 +953,7 @@ ':' Punctuation ' ' Text '(' Operator -"v'" Name +'v"' Name '.' Operator 'map' Name ')' Operator @@ -969,19 +969,19 @@ '=' Operator '>' Operator ' ' Text -"v'" Name +'v"' Name '.' Operator 'elts' Name ' ' Text '=' Operator ' ' Text -"b'" Name +'b"' Name '.' Operator 'left' Name ' ' Text '+' Operator ' ' Text -"b'" Name +'b"' Name '.' Operator 'done' Name '\n' Text @@ -1092,7 +1092,7 @@ ' ' Text '+' Operator ' ' Text -"KeySetView'" Name +'KeySetView"' Name '->' Operator 'setRefs' Name '->' Operator @@ -1370,7 +1370,7 @@ ']' Operator ',' Punctuation ' ' Text -"i'" Name +'i"' Name ' ' Text '=' Operator ' ' Text @@ -1385,7 +1385,7 @@ '\n' Text ' ' Text -"i'" Name +'i"' Name '.' Operator 'left' Name ' ' Text @@ -1397,7 +1397,7 @@ '\n' Text ' ' Text -"i'" Name +'i"' Name '.' Operator 'done' Name ' ' Text @@ -1417,7 +1417,7 @@ ' ' Text 'no' Keyword ' ' Text -"i'" Name +'i"' Name '.' Operator 'lastRef' Name '\n' Text @@ -1510,7 +1510,7 @@ ']' Operator ',' Punctuation ' ' Text -"i'" Name +'i"' Name ' ' Text '=' Operator ' ' Text @@ -1535,7 +1535,7 @@ '\n' Text ' ' Text -"i'" Name +'i"' Name '.' Operator 'left' Name ' ' Text @@ -1551,7 +1551,7 @@ '\n' Text ' ' Text -"i'" Name +'i"' Name '.' Operator 'done' Name ' ' Text @@ -1567,7 +1567,7 @@ '\n' Text ' ' Text -"i'" Name +'i"' Name '.' Operator 'lastRef' Name ' ' Text