From a92b8a5a90ea275ea0695750c916fe676f9b7b42 Mon Sep 17 00:00:00 2001 From: Philip Offtermatt Date: Wed, 9 Aug 2023 11:25:39 +0200 Subject: [PATCH] Advance model --- .../core/quint_model/basicSpells.qnt | 126 ++++++++++++++++++ .../core/quint_model/extraSpells.qnt | 19 +++ .../core/quint_model/modularity.qnt | 60 +++++++++ tests/difference/core/quint_model/test.qnt | 4 +- .../core/quint_model/weird_parsing2.qnt | 43 ++++++ 5 files changed, 251 insertions(+), 1 deletion(-) create mode 100644 tests/difference/core/quint_model/basicSpells.qnt create mode 100644 tests/difference/core/quint_model/extraSpells.qnt create mode 100644 tests/difference/core/quint_model/modularity.qnt create mode 100644 tests/difference/core/quint_model/weird_parsing2.qnt diff --git a/tests/difference/core/quint_model/basicSpells.qnt b/tests/difference/core/quint_model/basicSpells.qnt new file mode 100644 index 0000000000..32747e0f67 --- /dev/null +++ b/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)), + } +} \ No newline at end of file diff --git a/tests/difference/core/quint_model/extraSpells.qnt b/tests/difference/core/quint_model/extraSpells.qnt new file mode 100644 index 0000000000..5539c0140b --- /dev/null +++ b/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)), + } +} \ No newline at end of file diff --git a/tests/difference/core/quint_model/modularity.qnt b/tests/difference/core/quint_model/modularity.qnt new file mode 100644 index 0000000000..9d102e2679 --- /dev/null +++ b/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) + } + } + } +} \ No newline at end of file diff --git a/tests/difference/core/quint_model/test.qnt b/tests/difference/core/quint_model/test.qnt index ca04b357f0..9a62b6b32f 100644 --- a/tests/difference/core/quint_model/test.qnt +++ b/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' = [] } \ No newline at end of file diff --git a/tests/difference/core/quint_model/weird_parsing2.qnt b/tests/difference/core/quint_model/weird_parsing2.qnt new file mode 100644 index 0000000000..936e6f96b5 --- /dev/null +++ b/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) + // } +} \ No newline at end of file