Skip to content

Commit

Permalink
Update the alloy golden test
Browse files Browse the repository at this point in the history
Alloy 6 recommends changing `'` in legacy specs to `"`. Since this is a
breaking change, the golden test is updated to reflect that.
  • Loading branch information
hwayne committed Nov 29, 2021
1 parent 109de2b commit 67ea008
Show file tree
Hide file tree
Showing 2 changed files with 48 additions and 48 deletions.
40 changes: 20 additions & 20 deletions tests/examplefiles/alloy/example.als
Expand Up @@ -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
*/
Expand Down Expand Up @@ -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"])
}

/**
Expand All @@ -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] {
Expand All @@ -141,22 +141,22 @@ 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]
pre.views = post.views
}

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]
Expand Down
56 changes: 28 additions & 28 deletions tests/examplefiles/alloy/example.als.output

Some generated files are not rendered by default. Learn more about how customized files appear on GitHub.

0 comments on commit 67ea008

Please sign in to comment.