Merge branch 'master' of https://github.com/nmacedo/Electrum

Author: nmacedo

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)
 }
 

electrum/src/main/resources/models/util/sequence.als

@@ -50,15 +50,15 @@ 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 */
 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])
   }
 }
 

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)
 }

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
 }