From 71ba4369e3fef96b62bef40a8cb0d7bc5e6a377e Mon Sep 17 00:00:00 2001 From: David Chemouil Date: Sat, 25 Nov 2017 18:37:37 +0100 Subject: [PATCH] remove primes from util/ models to be able to use them in Electrum --- .../src/main/resources/models/util/seqrel.als | 4 +- .../main/resources/models/util/sequence.als | 4 +- .../main/resources/models/util/sequniv.als | 4 +- .../src/main/resources/models/util/time.als | 44 +++++++++---------- 4 files changed, 28 insertions(+), 28 deletions(-) diff --git a/electrum/src/main/resources/models/util/seqrel.als b/electrum/src/main/resources/models/util/seqrel.als index 1fe3802d..57afece8 100755 --- a/electrum/src/main/resources/models/util/seqrel.als +++ b/electrum/src/main/resources/models/util/seqrel.als @@ -93,13 +93,13 @@ fun delete[s: SeqIdx -> elem, i: SeqIdx] : SeqIdx -> elem { /** appended is the result of appending s2 to s1 */ fun append [s1, s2: SeqIdx -> elem] : SeqIdx -> elem { - let shift = {i', i: SeqIdx | #ord/prevs[i'] = add[#ord/prevs[i], add[#ord/prevs[lastIdx[s1]], 1]] } | + let shift = {i2, i: SeqIdx | #ord/prevs[i2] = add[#ord/prevs[i], add[#ord/prevs[lastIdx[s1]], 1]] } | s1 + shift.s2 } /** returns the subsequence of s between from and to, inclusive */ fun subseq [s: SeqIdx -> elem, from, to: SeqIdx] : SeqIdx -> elem { - let shift = {i', i: SeqIdx | #ord/prevs[i'] = sub[#ord/prevs[i], #ord/prevs[from]] } | + let shift = {i2, i: SeqIdx | #ord/prevs[i2] = sub[#ord/prevs[i], #ord/prevs[from]] } | shift.((SeqIdx - ord/nexts[to]) <: s) } diff --git a/electrum/src/main/resources/models/util/sequence.als b/electrum/src/main/resources/models/util/sequence.als index 524e3cf7..b092e872 100755 --- a/electrum/src/main/resources/models/util/sequence.als +++ b/electrum/src/main/resources/models/util/sequence.als @@ -50,7 +50,7 @@ pred noDuplicates { /** invoke if you want all sequences within scope to exist */ pred allExist { (some s: Seq | s.isEmpty) && - (all s: Seq | SeqIdx !in s.inds => (all e: elem | some s': Seq | s.add[e, s'])) + (all s: Seq | SeqIdx !in s.inds => (all e: elem | some s2: Seq | s.add[e, s2])) } /** invoke if you want all sequences within scope with no duplicates */ @@ -58,7 +58,7 @@ pred allExistNoDuplicates { some s: Seq | s.isEmpty all s: Seq { !s.hasDups - SeqIdx !in s.inds => (all e: elem - s.elems | some s': Seq | s.add[e, s']) + SeqIdx !in s.inds => (all e: elem - s.elems | some s2: Seq | s.add[e, s2]) } } diff --git a/electrum/src/main/resources/models/util/sequniv.als b/electrum/src/main/resources/models/util/sequniv.als index efa8bf42..8ec23975 100755 --- a/electrum/src/main/resources/models/util/sequniv.als +++ b/electrum/src/main/resources/models/util/sequniv.als @@ -123,7 +123,7 @@ fun delete[s: Int -> univ, i: Int] : s { * (If the resulting sequence is too long, it will be truncated) */ fun append [s1, s2: Int -> univ] : s1+s2 { - let shift = {i', i: seq/Int | int[i'] = ui/add[int[i], ui/add[int[lastIdx[s1]], 1]] } | + let shift = {i2, i: seq/Int | int[i2] = ui/add[int[i], ui/add[int[lastIdx[s1]], 1]] } | no s1 => s2 else (s1 + shift.s2) } @@ -132,6 +132,6 @@ fun append [s1, s2: Int -> univ] : s1+s2 { * Precondition: 0 <= from <= to < #s */ fun subseq [s: Int -> univ, from, to: Int] : s { - let shift = {i', i: seq/Int | int[i'] = ui/sub[int[i], int[from]] } | + let shift = {i2, i: seq/Int | int[i2] = ui/sub[int[i], int[from]] } | shift.((seq/Int - ui/nexts[to]) <: s) } diff --git a/electrum/src/main/resources/models/util/time.als b/electrum/src/main/resources/models/util/time.als index b6f9d8ca..eace299e 100755 --- a/electrum/src/main/resources/models/util/time.als +++ b/electrum/src/main/resources/models/util/time.als @@ -6,48 +6,48 @@ let dynamic[x] = x one-> Time let dynamicSet[x] = x -> Time -let then [a, b, t, t'] { - some x:Time | a[t,x] && b[x,t'] +let then [a, b, t, t2] { + some x:Time | a[t,x] && b[x,t2] } let while = while3 -let while9 [cond, body, t, t'] { - some x:Time | (cond[t] => body[t,x] else t=x) && while8[cond,body,x,t'] +let while9 [cond, body, t, t2] { + some x:Time | (cond[t] => body[t,x] else t=x) && while8[cond,body,x,t2] } -let while8 [cond, body, t, t'] { - some x:Time | (cond[t] => body[t,x] else t=x) && while7[cond,body,x,t'] +let while8 [cond, body, t, t2] { + some x:Time | (cond[t] => body[t,x] else t=x) && while7[cond,body,x,t2] } -let while7 [cond, body, t, t'] { - some x:Time | (cond[t] => body[t,x] else t=x) && while6[cond,body,x,t'] +let while7 [cond, body, t, t2] { + some x:Time | (cond[t] => body[t,x] else t=x) && while6[cond,body,x,t2] } -let while6 [cond, body, t, t'] { - some x:Time | (cond[t] => body[t,x] else t=x) && while5[cond,body,x,t'] +let while6 [cond, body, t, t2] { + some x:Time | (cond[t] => body[t,x] else t=x) && while5[cond,body,x,t2] } -let while5 [cond, body, t, t'] { - some x:Time | (cond[t] => body[t,x] else t=x) && while4[cond,body,x,t'] +let while5 [cond, body, t, t2] { + some x:Time | (cond[t] => body[t,x] else t=x) && while4[cond,body,x,t2] } -let while4 [cond, body, t, t'] { - some x:Time | (cond[t] => body[t,x] else t=x) && while3[cond,body,x,t'] +let while4 [cond, body, t, t2] { + some x:Time | (cond[t] => body[t,x] else t=x) && while3[cond,body,x,t2] } -let while3 [cond, body, t, t'] { - some x:Time | (cond[t] => body[t,x] else t=x) && while2[cond,body,x,t'] +let while3 [cond, body, t, t2] { + some x:Time | (cond[t] => body[t,x] else t=x) && while2[cond,body,x,t2] } -let while2 [cond, body, t, t'] { - some x:Time | (cond[t] => body[t,x] else t=x) && while1[cond,body,x,t'] +let while2 [cond, body, t, t2] { + some x:Time | (cond[t] => body[t,x] else t=x) && while1[cond,body,x,t2] } -let while1 [cond, body, t, t'] { - some x:Time | (cond[t] => body[t,x] else t=x) && while0[cond,body,x,t'] +let while1 [cond, body, t, t2] { + some x:Time | (cond[t] => body[t,x] else t=x) && while0[cond,body,x,t2] } -let while0 [cond, body, t, t'] { - !cond[t] && t=t' +let while0 [cond, body, t, t2] { + !cond[t] && t=t2 }