Advance model

tests/difference/core/quint_model/basicSpells.qnt

@@ -0,0 +1,126 @@
+// -*- mode: Bluespec; -*-
+/**
+ * This module collects definitions that are ubiquitous.
+ * One day they will become the standard library of Quint.
+ */
+module basicSpells {
+  /// An annotation for writing preconditions.
+  /// - @param __cond condition to check
+  /// - @returns true if and only if __cond evaluates to true
+  pure def require(__cond: bool): bool = __cond
+
+  run requireTest = all {
+    assert(require(4 > 3)),
+    assert(not(require(false))),
+  }
+
+  /// A convenience operator that returns a string error code,
+  ///  if the condition does not hold true.
+  ///
+  /// - @param __cond condition to check
+  /// - @param __error a non-empty error message
+  /// - @returns "", when __cond holds true; otherwise __error
+  pure def requires(__cond: bool, __error: str): str = {
+    if (__cond) "" else __error
+  }
+
+  run requiresTest = all {
+    assert(requires(4 > 3, "4 > 3") == ""),
+    assert(requires(4 < 3, "false: 4 < 3") == "false: 4 < 3"),
+  }
+
+
+  /// Compute the maximum of two integers.
+  ///
+  /// - @param __i first integer
+  /// - @param __j second integer
+  /// - @returns the maximum of __i and __j
+  pure def max(__i: int, __j: int): int = {
+    if (__i > __j) __i else __j
+  }
+
+  run maxTest = all {
+    assert(max(3, 4) == 4),
+    assert(max(6, 3) == 6),
+    assert(max(10, 10) == 10),
+    assert(max(-3, -5) == -3),
+    assert(max(-5, -3) == -3),
+  }
+
+  /// Compute the absolute value of an integer
+  ///
+  /// - @param __i : an integer whose absolute value we are interested in
+  /// - @returns |__i|, the absolute value of __i
+  pure def abs(__i: int): int = {
+    if (__i < 0) -__i else __i
+  }
+
+  run absTest = all {
+    assert(abs(3) == 3),
+    assert(abs(-3) == 3),
+    assert(abs(0) == 0),
+  }
+
+  /// Remove a set element.
+  ///
+  /// - @param __set a set to remove an element from
+  /// - @param __elem an element to remove
+  /// - @returns a new set that contains all elements of __set but __elem
+  pure def setRemove(__set: Set[a], __elem: a): Set[a] = {
+    __set.exclude(Set(__elem))
+  }
+
+  run setRemoveTest = all {
+    assert(Set(2, 4) == Set(2, 3, 4).setRemove(3)),
+    assert(Set() == Set().setRemove(3)),
+  }
+
+  /// Test whether a key is present in a map
+  ///
+  /// - @param __map a map to query
+  /// - @param __key the key to look for
+  /// - @returns true if and only __map has an entry associated with __key
+  pure def has(__map: a -> b, __key: a): bool = {
+    __map.keys().contains(__key)
+  }
+
+  run hasTest = all {
+    assert(Map(2 -> 3, 4 -> 5).has(2)),
+    assert(not(Map(2 -> 3, 4 -> 5).has(6))),
+  }
+
+  /// Get the map value associated with a key, or the default,
+  /// if the key is not present.
+  ///
+  /// - @param __map the map to query
+  /// - @param __key the key to search for
+  /// - @returns the value associated with the key, if __key is
+  ///   present in the map, and __default otherwise
+  pure def getOrElse(__map: a -> b, __key: a, __default: b): b = {
+    if (__map.has(__key)) {
+      __map.get(__key)
+    } else {
+      __default
+    }
+  }
+
+  run getOrElseTest = all {
+    assert(Map(2 -> 3, 4 -> 5).getOrElse(2, 0) == 3),
+    assert(Map(2 -> 3, 4 -> 5).getOrElse(7, 11) == 11),
+  }
+
+  /// Remove a map entry.
+  ///
+  /// - @param __map a map to remove an entry from
+  /// - @param __key the key of an entry to remove
+  /// - @returns a new map that contains all entries of __map
+  ///          that do not have the key __key
+  pure def mapRemove(__map: a -> b, __key: a): a -> b = {
+    __map.keys().setRemove(__key).mapBy(__k => __map.get(__k))
+  }
+
+  run mapRemoveTest = all {
+    assert(Map(3 -> 4, 7 -> 8) == Map(3 -> 4, 5 -> 6, 7 -> 8).mapRemove(5)),
+    assert(Map() == Map().mapRemove(3)),
+  }
+}

tests/difference/core/quint_model/extraSpells.qnt

@@ -0,0 +1,19 @@
+module extraSpells {
+
+    /// Removes a set of map entry.
+    ///
+    /// - @param __map a map to remove an entry from
+    /// - @param __keys a set of keys to remove from the map
+    /// - @returns a new map that contains all entries of __map
+    ///          that do not have a key in __keys
+    pure def mapRemoveAll(__map: a -> b, __keys: Set[a]): a -> b = {
+        __map.keys().exclude(__keys).mapBy(__k => __map.get(__k))
+    }
+
+    run mapRemoveAllTest =
+        val m = Map(3 -> 4, 5 -> 6, 7 -> 8)
+        all {
+            assert(m.mapRemoveAll(Set(5, 7)) == Map(3 -> 4)),
+            assert(m.mapRemoveAll(Set(5, 99999)) == Map(3 -> 4, 7 -> 8)),
+        }
+}

tests/difference/core/quint_model/modularity.qnt

@@ -0,0 +1,60 @@
+module bank {
+    var balances: str -> int
+
+    action Send(sender: str, receiver: str, amt: int): bool = all {
+        balances.get(sender) > amt,
+        balances' = balances.set(sender, balances.get(sender) - amt),
+    }
+
+    action __bank_noop(): bool = all {
+        balances' = balances,
+    }
+}
+
+module governance {
+    var votes: str -> bool
+
+    action Vote(voter: str, vote: bool): bool = all {
+        votes' = votes.set(voter, vote),
+    }
+
+    action __gov_noop(): bool = all {
+        votes' = votes,
+    }
+}
+
+module main {
+    import bank.*
+    import governance.*
+
+
+   // working
+   action MainAction(boolean: bool): bool = all {
+        if(boolean) {
+            all {
+                Send("Alice", "Bob", 10),
+                votes' = votes,
+            }
+        } else {
+            all { 
+                balances' = balances,
+                Vote("Alice", true)
+            }
+        }
+   }
+
+   // not working
+   action MainAction2(boolean: bool): bool = all {
+        if(boolean) {
+            all {
+                Send("Alice", "Bob", 10),
+                votes' = votes,
+            }
+        } else {
+            all { 
+                balances' = balances,
+                Vote("Alice", true)
+            }
+        }
+   }
+}

tests/difference/core/quint_model/test.qnt

@@ -6,11 +6,13 @@ module weird_parsing {
     any {
         all {
             boolean == MyTrue,
-            channel' = channel
+            channel' = channel.append(1)
         },
         all {
             not(boolean),
             channel' = channel
         }
     }
+
+    action init = channel' = []
 }

tests/difference/core/quint_model/weird_parsing2.qnt

@@ -0,0 +1,43 @@
+module main {
+    var myMap: int -> int
+
+    action op1(a: int): bool =
+        myMap' =  myMap.set(3,a)
+
+    action op2(b: int): bool =
+        myMap' = myMap.set(1,b)
+
+    action noop(): bool =
+        myMap' = myMap
+
+    // not working
+    action main(boolean: bool): bool =
+        if(boolean){
+            noop
+        } else {
+            op1(2)
+        }
+
+    // not working
+    // action main2(boolean: bool): bool =
+    //     if(boolean){
+    //         op1()
+    //     } else {
+    //         op2()
+    //     }
+
+    // not working
+    // action main2(boolean: bool): bool =
+    //     any {
+    //         op1(),
+    //         op2()
+    //     }
+
+    // fine
+    // action main3(boolean: bool): bool =
+    //     if(boolean){
+    //         myMap' = myMap
+    //     } else {
+    //         myMap' = myMap.set(3,4)
+    //     }
+}