diff --git a/Code/itf/tests/fixtures/votekeeper/voteBookkeeper_noSkipQuorumMixedVotesSameValTest.itf.json b/Code/itf/tests/fixtures/votekeeper/voteBookkeeper_noSkipQuorumMixedVotesSameValTest.itf.json deleted file mode 100644 index c2425907a..000000000 --- a/Code/itf/tests/fixtures/votekeeper/voteBookkeeper_noSkipQuorumMixedVotesSameValTest.itf.json +++ /dev/null @@ -1,235 +0,0 @@ -{ - "#meta": { - "format": "ITF", - "format-description": "https://apalache.informal.systems/docs/adr/015adr-trace.html", - "source": "voteBookkeeperTest.qnt", - "status": "passed", - "description": "Created by Quint on Fri Nov 17 2023 21:56:43 GMT+0100 (Central European Standard Time)", - "timestamp": 1700254603572 - }, - "vars": [ - "voteBookkeeperTest::voteBookkeeperSM::weightedVote", - "voteBookkeeperTest::voteBookkeeperSM::bookkeeper", - "voteBookkeeperTest::voteBookkeeperSM::lastEmitted" - ], - "states": [ - { - "#meta": { "index": 0 }, - "voteBookkeeperTest::voteBookkeeperSM::bookkeeper": { - "currentRound": { "#bigint": "1" }, - "height": { "#bigint": "1" }, - "rounds": { "#map": [] }, - "totalWeight": { "#bigint": "100" } - }, - "voteBookkeeperTest::voteBookkeeperSM::lastEmitted": { - "name": "", - "round": { "#bigint": "-1" }, - "value": "null" - }, - "voteBookkeeperTest::voteBookkeeperSM::weightedVote": { - "#tup": [ - { - "address": "", - "height": { "#bigint": "1" }, - "round": { "#bigint": "-1" }, - "typ": "", - "value": "" - }, - { "#bigint": "-1" } - ] - } - }, - { - "#meta": { "index": 1 }, - "voteBookkeeperTest::voteBookkeeperSM::bookkeeper": { - "currentRound": { "#bigint": "1" }, - "height": { "#bigint": "1" }, - "rounds": { - "#map": [ - [ - { "#bigint": "1" }, - { - "emittedEvents": { "#set": [] }, - "height": { "#bigint": "1" }, - "precommits": { - "totalWeight": { "#bigint": "100" }, - "valuesWeights": { "#map": [] }, - "votesAddresses": { "#set": [] } - }, - "prevotes": { - "totalWeight": { "#bigint": "100" }, - "valuesWeights": { "#map": [["val1", { "#bigint": "10" }]] }, - "votesAddresses": { "#set": ["alice"] } - }, - "round": { "#bigint": "1" }, - "votesAddressesWeights": { - "#map": [["alice", { "#bigint": "10" }]] - } - } - ] - ] - }, - "totalWeight": { "#bigint": "100" } - }, - "voteBookkeeperTest::voteBookkeeperSM::lastEmitted": { - "name": "None", - "round": { "#bigint": "1" }, - "value": "null" - }, - "voteBookkeeperTest::voteBookkeeperSM::weightedVote": { - "#tup": [ - { - "address": "alice", - "height": { "#bigint": "1" }, - "round": { "#bigint": "1" }, - "typ": "Prevote", - "value": "val1" - }, - { "#bigint": "10" } - ] - } - }, - { - "#meta": { "index": 2 }, - "voteBookkeeperTest::voteBookkeeperSM::bookkeeper": { - "currentRound": { "#bigint": "1" }, - "height": { "#bigint": "1" }, - "rounds": { - "#map": [ - [ - { "#bigint": "1" }, - { - "emittedEvents": { "#set": [] }, - "height": { "#bigint": "1" }, - "precommits": { - "totalWeight": { "#bigint": "100" }, - "valuesWeights": { "#map": [] }, - "votesAddresses": { "#set": [] } - }, - "prevotes": { - "totalWeight": { "#bigint": "100" }, - "valuesWeights": { "#map": [["val1", { "#bigint": "10" }]] }, - "votesAddresses": { "#set": ["alice"] } - }, - "round": { "#bigint": "1" }, - "votesAddressesWeights": { - "#map": [["alice", { "#bigint": "10" }]] - } - } - ], - [ - { "#bigint": "2" }, - { - "emittedEvents": { "#set": [] }, - "height": { "#bigint": "1" }, - "precommits": { - "totalWeight": { "#bigint": "100" }, - "valuesWeights": { "#map": [] }, - "votesAddresses": { "#set": [] } - }, - "prevotes": { - "totalWeight": { "#bigint": "100" }, - "valuesWeights": { "#map": [["val1", { "#bigint": "30" }]] }, - "votesAddresses": { "#set": ["john"] } - }, - "round": { "#bigint": "2" }, - "votesAddressesWeights": { - "#map": [["john", { "#bigint": "30" }]] - } - } - ] - ] - }, - "totalWeight": { "#bigint": "100" } - }, - "voteBookkeeperTest::voteBookkeeperSM::lastEmitted": { - "name": "None", - "round": { "#bigint": "2" }, - "value": "null" - }, - "voteBookkeeperTest::voteBookkeeperSM::weightedVote": { - "#tup": [ - { - "address": "john", - "height": { "#bigint": "1" }, - "round": { "#bigint": "2" }, - "typ": "Prevote", - "value": "val1" - }, - { "#bigint": "30" } - ] - } - }, - { - "#meta": { "index": 3 }, - "voteBookkeeperTest::voteBookkeeperSM::bookkeeper": { - "currentRound": { "#bigint": "1" }, - "height": { "#bigint": "1" }, - "rounds": { - "#map": [ - [ - { "#bigint": "1" }, - { - "emittedEvents": { "#set": [] }, - "height": { "#bigint": "1" }, - "precommits": { - "totalWeight": { "#bigint": "100" }, - "valuesWeights": { "#map": [] }, - "votesAddresses": { "#set": [] } - }, - "prevotes": { - "totalWeight": { "#bigint": "100" }, - "valuesWeights": { "#map": [["val1", { "#bigint": "10" }]] }, - "votesAddresses": { "#set": ["alice"] } - }, - "round": { "#bigint": "1" }, - "votesAddressesWeights": { - "#map": [["alice", { "#bigint": "10" }]] - } - } - ], - [ - { "#bigint": "2" }, - { - "emittedEvents": { "#set": [] }, - "height": { "#bigint": "1" }, - "precommits": { - "totalWeight": { "#bigint": "100" }, - "valuesWeights": { "#map": [["val1", { "#bigint": "30" }]] }, - "votesAddresses": { "#set": ["john"] } - }, - "prevotes": { - "totalWeight": { "#bigint": "100" }, - "valuesWeights": { "#map": [["val1", { "#bigint": "30" }]] }, - "votesAddresses": { "#set": ["john"] } - }, - "round": { "#bigint": "2" }, - "votesAddressesWeights": { - "#map": [["john", { "#bigint": "30" }]] - } - } - ] - ] - }, - "totalWeight": { "#bigint": "100" } - }, - "voteBookkeeperTest::voteBookkeeperSM::lastEmitted": { - "name": "None", - "round": { "#bigint": "2" }, - "value": "null" - }, - "voteBookkeeperTest::voteBookkeeperSM::weightedVote": { - "#tup": [ - { - "address": "john", - "height": { "#bigint": "1" }, - "round": { "#bigint": "2" }, - "typ": "Precommit", - "value": "val1" - }, - { "#bigint": "30" } - ] - } - } - ] -} diff --git a/Code/itf/tests/fixtures/votekeeper/voteBookkeeper_noSkipSmallQuorumMixedVotesSameValTest.itf.json b/Code/itf/tests/fixtures/votekeeper/voteBookkeeper_noSkipSmallQuorumMixedVotesSameValTest.itf.json deleted file mode 100644 index e5c7713b7..000000000 --- a/Code/itf/tests/fixtures/votekeeper/voteBookkeeper_noSkipSmallQuorumMixedVotesSameValTest.itf.json +++ /dev/null @@ -1 +0,0 @@ -{"#meta":{"format":"ITF","format-description":"https://apalache.informal.systems/docs/adr/015adr-trace.html","source":"voteBookkeeperTest.qnt","status":"passed","description":"Created by Quint on Fri Nov 17 2023 21:49:35 GMT+0100 (Central European Standard Time)","timestamp":1700254175174},"vars":["voteBookkeeperTest::voteBookkeeperSM::weightedVote","voteBookkeeperTest::voteBookkeeperSM::bookkeeper","voteBookkeeperTest::voteBookkeeperSM::lastEmitted"],"states":[{"#meta":{"index":0},"voteBookkeeperTest::voteBookkeeperSM::bookkeeper":{"currentRound":{"#bigint":"1"},"height":{"#bigint":"1"},"rounds":{"#map":[]},"totalWeight":{"#bigint":"90"}},"voteBookkeeperTest::voteBookkeeperSM::lastEmitted":{"name":"","round":{"#bigint":"-1"},"value":"null"},"voteBookkeeperTest::voteBookkeeperSM::weightedVote":{"#tup":[{"address":"","height":{"#bigint":"1"},"round":{"#bigint":"-1"},"typ":"","value":""},{"#bigint":"-1"}]}},{"#meta":{"index":1},"voteBookkeeperTest::voteBookkeeperSM::bookkeeper":{"currentRound":{"#bigint":"1"},"height":{"#bigint":"1"},"rounds":{"#map":[[{"#bigint":"1"},{"emittedEvents":{"#set":[]},"height":{"#bigint":"1"},"precommits":{"totalWeight":{"#bigint":"90"},"valuesWeights":{"#map":[]},"votesAddresses":{"#set":[]}},"prevotes":{"totalWeight":{"#bigint":"90"},"valuesWeights":{"#map":[["val1",{"#bigint":"10"}]]},"votesAddresses":{"#set":["alice"]}},"round":{"#bigint":"1"},"votesAddressesWeights":{"#map":[["alice",{"#bigint":"10"}]]}}]]},"totalWeight":{"#bigint":"90"}},"voteBookkeeperTest::voteBookkeeperSM::lastEmitted":{"name":"None","round":{"#bigint":"1"},"value":"null"},"voteBookkeeperTest::voteBookkeeperSM::weightedVote":{"#tup":[{"address":"alice","height":{"#bigint":"1"},"round":{"#bigint":"1"},"typ":"Prevote","value":"val1"},{"#bigint":"10"}]}},{"#meta":{"index":2},"voteBookkeeperTest::voteBookkeeperSM::bookkeeper":{"currentRound":{"#bigint":"1"},"height":{"#bigint":"1"},"rounds":{"#map":[[{"#bigint":"1"},{"emittedEvents":{"#set":[]},"height":{"#bigint":"1"},"precommits":{"totalWeight":{"#bigint":"90"},"valuesWeights":{"#map":[]},"votesAddresses":{"#set":[]}},"prevotes":{"totalWeight":{"#bigint":"90"},"valuesWeights":{"#map":[["val1",{"#bigint":"10"}]]},"votesAddresses":{"#set":["alice"]}},"round":{"#bigint":"1"},"votesAddressesWeights":{"#map":[["alice",{"#bigint":"10"}]]}}],[{"#bigint":"2"},{"emittedEvents":{"#set":[]},"height":{"#bigint":"1"},"precommits":{"totalWeight":{"#bigint":"90"},"valuesWeights":{"#map":[]},"votesAddresses":{"#set":[]}},"prevotes":{"totalWeight":{"#bigint":"90"},"valuesWeights":{"#map":[["val1",{"#bigint":"20"}]]},"votesAddresses":{"#set":["john"]}},"round":{"#bigint":"2"},"votesAddressesWeights":{"#map":[["john",{"#bigint":"20"}]]}}]]},"totalWeight":{"#bigint":"90"}},"voteBookkeeperTest::voteBookkeeperSM::lastEmitted":{"name":"None","round":{"#bigint":"2"},"value":"null"},"voteBookkeeperTest::voteBookkeeperSM::weightedVote":{"#tup":[{"address":"john","height":{"#bigint":"1"},"round":{"#bigint":"2"},"typ":"Prevote","value":"val1"},{"#bigint":"20"}]}},{"#meta":{"index":3},"voteBookkeeperTest::voteBookkeeperSM::bookkeeper":{"currentRound":{"#bigint":"1"},"height":{"#bigint":"1"},"rounds":{"#map":[[{"#bigint":"1"},{"emittedEvents":{"#set":[]},"height":{"#bigint":"1"},"precommits":{"totalWeight":{"#bigint":"90"},"valuesWeights":{"#map":[]},"votesAddresses":{"#set":[]}},"prevotes":{"totalWeight":{"#bigint":"90"},"valuesWeights":{"#map":[["val1",{"#bigint":"10"}]]},"votesAddresses":{"#set":["alice"]}},"round":{"#bigint":"1"},"votesAddressesWeights":{"#map":[["alice",{"#bigint":"10"}]]}}],[{"#bigint":"2"},{"emittedEvents":{"#set":[]},"height":{"#bigint":"1"},"precommits":{"totalWeight":{"#bigint":"90"},"valuesWeights":{"#map":[["val1",{"#bigint":"20"}]]},"votesAddresses":{"#set":["john"]}},"prevotes":{"totalWeight":{"#bigint":"90"},"valuesWeights":{"#map":[["val1",{"#bigint":"20"}]]},"votesAddresses":{"#set":["john"]}},"round":{"#bigint":"2"},"votesAddressesWeights":{"#map":[["john",{"#bigint":"20"}]]}}]]},"totalWeight":{"#bigint":"90"}},"voteBookkeeperTest::voteBookkeeperSM::lastEmitted":{"name":"None","round":{"#bigint":"2"},"value":"null"},"voteBookkeeperTest::voteBookkeeperSM::weightedVote":{"#tup":[{"address":"john","height":{"#bigint":"1"},"round":{"#bigint":"2"},"typ":"Precommit","value":"val1"},{"#bigint":"20"}]}}]} \ No newline at end of file diff --git a/Code/itf/tests/fixtures/votekeeper/voteBookkeeper_polkaAnyTest.itf.json b/Code/itf/tests/fixtures/votekeeper/voteBookkeeper_polkaAnyTest.itf.json deleted file mode 100644 index 1569cd492..000000000 --- a/Code/itf/tests/fixtures/votekeeper/voteBookkeeper_polkaAnyTest.itf.json +++ /dev/null @@ -1 +0,0 @@ -{"#meta":{"format":"ITF","format-description":"https://apalache.informal.systems/docs/adr/015adr-trace.html","source":"voteBookkeeperTest.qnt","status":"passed","description":"Created by Quint on Fri Nov 17 2023 21:49:17 GMT+0100 (Central European Standard Time)","timestamp":1700254157612},"vars":["voteBookkeeperTest::voteBookkeeperSM::weightedVote","voteBookkeeperTest::voteBookkeeperSM::bookkeeper","voteBookkeeperTest::voteBookkeeperSM::lastEmitted"],"states":[{"#meta":{"index":0},"voteBookkeeperTest::voteBookkeeperSM::bookkeeper":{"currentRound":{"#bigint":"1"},"height":{"#bigint":"1"},"rounds":{"#map":[]},"totalWeight":{"#bigint":"100"}},"voteBookkeeperTest::voteBookkeeperSM::lastEmitted":{"name":"","round":{"#bigint":"-1"},"value":"null"},"voteBookkeeperTest::voteBookkeeperSM::weightedVote":{"#tup":[{"address":"","height":{"#bigint":"1"},"round":{"#bigint":"-1"},"typ":"","value":""},{"#bigint":"-1"}]}},{"#meta":{"index":1},"voteBookkeeperTest::voteBookkeeperSM::bookkeeper":{"currentRound":{"#bigint":"1"},"height":{"#bigint":"1"},"rounds":{"#map":[[{"#bigint":"1"},{"emittedEvents":{"#set":[]},"height":{"#bigint":"1"},"precommits":{"totalWeight":{"#bigint":"100"},"valuesWeights":{"#map":[]},"votesAddresses":{"#set":[]}},"prevotes":{"totalWeight":{"#bigint":"100"},"valuesWeights":{"#map":[["val1",{"#bigint":"60"}]]},"votesAddresses":{"#set":["alice"]}},"round":{"#bigint":"1"},"votesAddressesWeights":{"#map":[["alice",{"#bigint":"60"}]]}}]]},"totalWeight":{"#bigint":"100"}},"voteBookkeeperTest::voteBookkeeperSM::lastEmitted":{"name":"None","round":{"#bigint":"1"},"value":"null"},"voteBookkeeperTest::voteBookkeeperSM::weightedVote":{"#tup":[{"address":"alice","height":{"#bigint":"1"},"round":{"#bigint":"1"},"typ":"Prevote","value":"val1"},{"#bigint":"60"}]}},{"#meta":{"index":2},"voteBookkeeperTest::voteBookkeeperSM::bookkeeper":{"currentRound":{"#bigint":"1"},"height":{"#bigint":"1"},"rounds":{"#map":[[{"#bigint":"1"},{"emittedEvents":{"#set":[{"name":"PolkaAny","round":{"#bigint":"1"},"value":"null"}]},"height":{"#bigint":"1"},"precommits":{"totalWeight":{"#bigint":"100"},"valuesWeights":{"#map":[]},"votesAddresses":{"#set":[]}},"prevotes":{"totalWeight":{"#bigint":"100"},"valuesWeights":{"#map":[["nil",{"#bigint":"10"}],["val1",{"#bigint":"60"}]]},"votesAddresses":{"#set":["alice","john"]}},"round":{"#bigint":"1"},"votesAddressesWeights":{"#map":[["alice",{"#bigint":"60"}],["john",{"#bigint":"10"}]]}}]]},"totalWeight":{"#bigint":"100"}},"voteBookkeeperTest::voteBookkeeperSM::lastEmitted":{"name":"PolkaAny","round":{"#bigint":"1"},"value":"null"},"voteBookkeeperTest::voteBookkeeperSM::weightedVote":{"#tup":[{"address":"john","height":{"#bigint":"1"},"round":{"#bigint":"1"},"typ":"Prevote","value":"nil"},{"#bigint":"10"}]}}]} \ No newline at end of file diff --git a/Code/itf/tests/fixtures/votekeeper/voteBookkeeper_polkaNilTest.itf.json b/Code/itf/tests/fixtures/votekeeper/voteBookkeeper_polkaNilTest.itf.json deleted file mode 100644 index 099b24a2c..000000000 --- a/Code/itf/tests/fixtures/votekeeper/voteBookkeeper_polkaNilTest.itf.json +++ /dev/null @@ -1 +0,0 @@ -{"#meta":{"format":"ITF","format-description":"https://apalache.informal.systems/docs/adr/015adr-trace.html","source":"voteBookkeeperTest.qnt","status":"passed","description":"Created by Quint on Fri Nov 17 2023 21:49:25 GMT+0100 (Central European Standard Time)","timestamp":1700254165713},"vars":["voteBookkeeperTest::voteBookkeeperSM::weightedVote","voteBookkeeperTest::voteBookkeeperSM::bookkeeper","voteBookkeeperTest::voteBookkeeperSM::lastEmitted"],"states":[{"#meta":{"index":0},"voteBookkeeperTest::voteBookkeeperSM::bookkeeper":{"currentRound":{"#bigint":"1"},"height":{"#bigint":"1"},"rounds":{"#map":[]},"totalWeight":{"#bigint":"100"}},"voteBookkeeperTest::voteBookkeeperSM::lastEmitted":{"name":"","round":{"#bigint":"-1"},"value":"null"},"voteBookkeeperTest::voteBookkeeperSM::weightedVote":{"#tup":[{"address":"","height":{"#bigint":"1"},"round":{"#bigint":"-1"},"typ":"","value":""},{"#bigint":"-1"}]}},{"#meta":{"index":1},"voteBookkeeperTest::voteBookkeeperSM::bookkeeper":{"currentRound":{"#bigint":"1"},"height":{"#bigint":"1"},"rounds":{"#map":[[{"#bigint":"1"},{"emittedEvents":{"#set":[]},"height":{"#bigint":"1"},"precommits":{"totalWeight":{"#bigint":"100"},"valuesWeights":{"#map":[]},"votesAddresses":{"#set":[]}},"prevotes":{"totalWeight":{"#bigint":"100"},"valuesWeights":{"#map":[["nil",{"#bigint":"60"}]]},"votesAddresses":{"#set":["alice"]}},"round":{"#bigint":"1"},"votesAddressesWeights":{"#map":[["alice",{"#bigint":"60"}]]}}]]},"totalWeight":{"#bigint":"100"}},"voteBookkeeperTest::voteBookkeeperSM::lastEmitted":{"name":"None","round":{"#bigint":"1"},"value":"null"},"voteBookkeeperTest::voteBookkeeperSM::weightedVote":{"#tup":[{"address":"alice","height":{"#bigint":"1"},"round":{"#bigint":"1"},"typ":"Prevote","value":"nil"},{"#bigint":"60"}]}},{"#meta":{"index":2},"voteBookkeeperTest::voteBookkeeperSM::bookkeeper":{"currentRound":{"#bigint":"1"},"height":{"#bigint":"1"},"rounds":{"#map":[[{"#bigint":"1"},{"emittedEvents":{"#set":[{"name":"PolkaNil","round":{"#bigint":"1"},"value":"null"}]},"height":{"#bigint":"1"},"precommits":{"totalWeight":{"#bigint":"100"},"valuesWeights":{"#map":[]},"votesAddresses":{"#set":[]}},"prevotes":{"totalWeight":{"#bigint":"100"},"valuesWeights":{"#map":[["nil",{"#bigint":"70"}]]},"votesAddresses":{"#set":["alice","john"]}},"round":{"#bigint":"1"},"votesAddressesWeights":{"#map":[["alice",{"#bigint":"60"}],["john",{"#bigint":"10"}]]}}]]},"totalWeight":{"#bigint":"100"}},"voteBookkeeperTest::voteBookkeeperSM::lastEmitted":{"name":"PolkaNil","round":{"#bigint":"1"},"value":"null"},"voteBookkeeperTest::voteBookkeeperSM::weightedVote":{"#tup":[{"address":"john","height":{"#bigint":"1"},"round":{"#bigint":"1"},"typ":"Prevote","value":"nil"},{"#bigint":"10"}]}}]} \ No newline at end of file diff --git a/Code/itf/tests/fixtures/votekeeper/voteBookkeeper_skipQuorumMixedVotesTwoValsTest.itf.json b/Code/itf/tests/fixtures/votekeeper/voteBookkeeper_skipQuorumMixedVotesTwoValsTest.itf.json deleted file mode 100644 index 197ad45c2..000000000 --- a/Code/itf/tests/fixtures/votekeeper/voteBookkeeper_skipQuorumMixedVotesTwoValsTest.itf.json +++ /dev/null @@ -1 +0,0 @@ -{"#meta":{"format":"ITF","format-description":"https://apalache.informal.systems/docs/adr/015adr-trace.html","source":"voteBookkeeperTest.qnt","status":"passed","description":"Created by Quint on Fri Nov 17 2023 21:49:30 GMT+0100 (Central European Standard Time)","timestamp":1700254170353},"vars":["voteBookkeeperTest::voteBookkeeperSM::weightedVote","voteBookkeeperTest::voteBookkeeperSM::bookkeeper","voteBookkeeperTest::voteBookkeeperSM::lastEmitted"],"states":[{"#meta":{"index":0},"voteBookkeeperTest::voteBookkeeperSM::bookkeeper":{"currentRound":{"#bigint":"1"},"height":{"#bigint":"1"},"rounds":{"#map":[]},"totalWeight":{"#bigint":"80"}},"voteBookkeeperTest::voteBookkeeperSM::lastEmitted":{"name":"","round":{"#bigint":"-1"},"value":"null"},"voteBookkeeperTest::voteBookkeeperSM::weightedVote":{"#tup":[{"address":"","height":{"#bigint":"1"},"round":{"#bigint":"-1"},"typ":"","value":""},{"#bigint":"-1"}]}},{"#meta":{"index":1},"voteBookkeeperTest::voteBookkeeperSM::bookkeeper":{"currentRound":{"#bigint":"1"},"height":{"#bigint":"1"},"rounds":{"#map":[[{"#bigint":"1"},{"emittedEvents":{"#set":[]},"height":{"#bigint":"1"},"precommits":{"totalWeight":{"#bigint":"80"},"valuesWeights":{"#map":[]},"votesAddresses":{"#set":[]}},"prevotes":{"totalWeight":{"#bigint":"80"},"valuesWeights":{"#map":[["val1",{"#bigint":"50"}]]},"votesAddresses":{"#set":["alice"]}},"round":{"#bigint":"1"},"votesAddressesWeights":{"#map":[["alice",{"#bigint":"50"}]]}}]]},"totalWeight":{"#bigint":"80"}},"voteBookkeeperTest::voteBookkeeperSM::lastEmitted":{"name":"None","round":{"#bigint":"1"},"value":"null"},"voteBookkeeperTest::voteBookkeeperSM::weightedVote":{"#tup":[{"address":"alice","height":{"#bigint":"1"},"round":{"#bigint":"1"},"typ":"Prevote","value":"val1"},{"#bigint":"50"}]}},{"#meta":{"index":2},"voteBookkeeperTest::voteBookkeeperSM::bookkeeper":{"currentRound":{"#bigint":"1"},"height":{"#bigint":"1"},"rounds":{"#map":[[{"#bigint":"1"},{"emittedEvents":{"#set":[]},"height":{"#bigint":"1"},"precommits":{"totalWeight":{"#bigint":"80"},"valuesWeights":{"#map":[]},"votesAddresses":{"#set":[]}},"prevotes":{"totalWeight":{"#bigint":"80"},"valuesWeights":{"#map":[["val1",{"#bigint":"50"}]]},"votesAddresses":{"#set":["alice"]}},"round":{"#bigint":"1"},"votesAddressesWeights":{"#map":[["alice",{"#bigint":"50"}]]}}],[{"#bigint":"2"},{"emittedEvents":{"#set":[]},"height":{"#bigint":"1"},"precommits":{"totalWeight":{"#bigint":"80"},"valuesWeights":{"#map":[]},"votesAddresses":{"#set":[]}},"prevotes":{"totalWeight":{"#bigint":"80"},"valuesWeights":{"#map":[["val1",{"#bigint":"10"}]]},"votesAddresses":{"#set":["john"]}},"round":{"#bigint":"2"},"votesAddressesWeights":{"#map":[["john",{"#bigint":"10"}]]}}]]},"totalWeight":{"#bigint":"80"}},"voteBookkeeperTest::voteBookkeeperSM::lastEmitted":{"name":"None","round":{"#bigint":"2"},"value":"null"},"voteBookkeeperTest::voteBookkeeperSM::weightedVote":{"#tup":[{"address":"john","height":{"#bigint":"1"},"round":{"#bigint":"2"},"typ":"Prevote","value":"val1"},{"#bigint":"10"}]}},{"#meta":{"index":3},"voteBookkeeperTest::voteBookkeeperSM::bookkeeper":{"currentRound":{"#bigint":"1"},"height":{"#bigint":"1"},"rounds":{"#map":[[{"#bigint":"1"},{"emittedEvents":{"#set":[]},"height":{"#bigint":"1"},"precommits":{"totalWeight":{"#bigint":"80"},"valuesWeights":{"#map":[]},"votesAddresses":{"#set":[]}},"prevotes":{"totalWeight":{"#bigint":"80"},"valuesWeights":{"#map":[["val1",{"#bigint":"50"}]]},"votesAddresses":{"#set":["alice"]}},"round":{"#bigint":"1"},"votesAddressesWeights":{"#map":[["alice",{"#bigint":"50"}]]}}],[{"#bigint":"2"},{"emittedEvents":{"#set":[{"name":"Skip","round":{"#bigint":"2"},"value":"null"}]},"height":{"#bigint":"1"},"precommits":{"totalWeight":{"#bigint":"80"},"valuesWeights":{"#map":[["val1",{"#bigint":"20"}]]},"votesAddresses":{"#set":["bob"]}},"prevotes":{"totalWeight":{"#bigint":"80"},"valuesWeights":{"#map":[["val1",{"#bigint":"10"}]]},"votesAddresses":{"#set":["john"]}},"round":{"#bigint":"2"},"votesAddressesWeights":{"#map":[["bob",{"#bigint":"20"}],["john",{"#bigint":"10"}]]}}]]},"totalWeight":{"#bigint":"80"}},"voteBookkeeperTest::voteBookkeeperSM::lastEmitted":{"name":"Skip","round":{"#bigint":"2"},"value":"null"},"voteBookkeeperTest::voteBookkeeperSM::weightedVote":{"#tup":[{"address":"bob","height":{"#bigint":"1"},"round":{"#bigint":"2"},"typ":"Precommit","value":"val1"},{"#bigint":"20"}]}}]} \ No newline at end of file diff --git a/Code/itf/tests/fixtures/votekeeper/voteBookkeeper_skipQuorumSinglePrecommitTest.itf.json b/Code/itf/tests/fixtures/votekeeper/voteBookkeeper_skipQuorumSinglePrecommitTest.itf.json deleted file mode 100644 index b6fac4cb5..000000000 --- a/Code/itf/tests/fixtures/votekeeper/voteBookkeeper_skipQuorumSinglePrecommitTest.itf.json +++ /dev/null @@ -1 +0,0 @@ -{"#meta":{"format":"ITF","format-description":"https://apalache.informal.systems/docs/adr/015adr-trace.html","source":"voteBookkeeperTest.qnt","status":"passed","description":"Created by Quint on Fri Nov 17 2023 21:49:30 GMT+0100 (Central European Standard Time)","timestamp":1700254170361},"vars":["voteBookkeeperTest::voteBookkeeperSM::weightedVote","voteBookkeeperTest::voteBookkeeperSM::bookkeeper","voteBookkeeperTest::voteBookkeeperSM::lastEmitted"],"states":[{"#meta":{"index":0},"voteBookkeeperTest::voteBookkeeperSM::bookkeeper":{"currentRound":{"#bigint":"1"},"height":{"#bigint":"1"},"rounds":{"#map":[]},"totalWeight":{"#bigint":"80"}},"voteBookkeeperTest::voteBookkeeperSM::lastEmitted":{"name":"","round":{"#bigint":"-1"},"value":"null"},"voteBookkeeperTest::voteBookkeeperSM::weightedVote":{"#tup":[{"address":"","height":{"#bigint":"1"},"round":{"#bigint":"-1"},"typ":"","value":""},{"#bigint":"-1"}]}},{"#meta":{"index":1},"voteBookkeeperTest::voteBookkeeperSM::bookkeeper":{"currentRound":{"#bigint":"1"},"height":{"#bigint":"1"},"rounds":{"#map":[[{"#bigint":"1"},{"emittedEvents":{"#set":[]},"height":{"#bigint":"1"},"precommits":{"totalWeight":{"#bigint":"80"},"valuesWeights":{"#map":[]},"votesAddresses":{"#set":[]}},"prevotes":{"totalWeight":{"#bigint":"80"},"valuesWeights":{"#map":[["val1",{"#bigint":"50"}]]},"votesAddresses":{"#set":["alice"]}},"round":{"#bigint":"1"},"votesAddressesWeights":{"#map":[["alice",{"#bigint":"50"}]]}}]]},"totalWeight":{"#bigint":"80"}},"voteBookkeeperTest::voteBookkeeperSM::lastEmitted":{"name":"None","round":{"#bigint":"1"},"value":"null"},"voteBookkeeperTest::voteBookkeeperSM::weightedVote":{"#tup":[{"address":"alice","height":{"#bigint":"1"},"round":{"#bigint":"1"},"typ":"Prevote","value":"val1"},{"#bigint":"50"}]}},{"#meta":{"index":2},"voteBookkeeperTest::voteBookkeeperSM::bookkeeper":{"currentRound":{"#bigint":"1"},"height":{"#bigint":"1"},"rounds":{"#map":[[{"#bigint":"1"},{"emittedEvents":{"#set":[]},"height":{"#bigint":"1"},"precommits":{"totalWeight":{"#bigint":"80"},"valuesWeights":{"#map":[]},"votesAddresses":{"#set":[]}},"prevotes":{"totalWeight":{"#bigint":"80"},"valuesWeights":{"#map":[["val1",{"#bigint":"50"}]]},"votesAddresses":{"#set":["alice"]}},"round":{"#bigint":"1"},"votesAddressesWeights":{"#map":[["alice",{"#bigint":"50"}]]}}],[{"#bigint":"2"},{"emittedEvents":{"#set":[]},"height":{"#bigint":"1"},"precommits":{"totalWeight":{"#bigint":"80"},"valuesWeights":{"#map":[]},"votesAddresses":{"#set":[]}},"prevotes":{"totalWeight":{"#bigint":"80"},"valuesWeights":{"#map":[["val1",{"#bigint":"10"}]]},"votesAddresses":{"#set":["john"]}},"round":{"#bigint":"2"},"votesAddressesWeights":{"#map":[["john",{"#bigint":"10"}]]}}]]},"totalWeight":{"#bigint":"80"}},"voteBookkeeperTest::voteBookkeeperSM::lastEmitted":{"name":"None","round":{"#bigint":"2"},"value":"null"},"voteBookkeeperTest::voteBookkeeperSM::weightedVote":{"#tup":[{"address":"john","height":{"#bigint":"1"},"round":{"#bigint":"2"},"typ":"Prevote","value":"val1"},{"#bigint":"10"}]}},{"#meta":{"index":3},"voteBookkeeperTest::voteBookkeeperSM::bookkeeper":{"currentRound":{"#bigint":"1"},"height":{"#bigint":"1"},"rounds":{"#map":[[{"#bigint":"1"},{"emittedEvents":{"#set":[]},"height":{"#bigint":"1"},"precommits":{"totalWeight":{"#bigint":"80"},"valuesWeights":{"#map":[]},"votesAddresses":{"#set":[]}},"prevotes":{"totalWeight":{"#bigint":"80"},"valuesWeights":{"#map":[["val1",{"#bigint":"50"}]]},"votesAddresses":{"#set":["alice"]}},"round":{"#bigint":"1"},"votesAddressesWeights":{"#map":[["alice",{"#bigint":"50"}]]}}],[{"#bigint":"2"},{"emittedEvents":{"#set":[{"name":"Skip","round":{"#bigint":"2"},"value":"null"}]},"height":{"#bigint":"1"},"precommits":{"totalWeight":{"#bigint":"80"},"valuesWeights":{"#map":[["val1",{"#bigint":"20"}]]},"votesAddresses":{"#set":["bob"]}},"prevotes":{"totalWeight":{"#bigint":"80"},"valuesWeights":{"#map":[["val1",{"#bigint":"10"}]]},"votesAddresses":{"#set":["john"]}},"round":{"#bigint":"2"},"votesAddressesWeights":{"#map":[["bob",{"#bigint":"20"}],["john",{"#bigint":"10"}]]}}]]},"totalWeight":{"#bigint":"80"}},"voteBookkeeperTest::voteBookkeeperSM::lastEmitted":{"name":"Skip","round":{"#bigint":"2"},"value":"null"},"voteBookkeeperTest::voteBookkeeperSM::weightedVote":{"#tup":[{"address":"bob","height":{"#bigint":"1"},"round":{"#bigint":"2"},"typ":"Precommit","value":"val1"},{"#bigint":"20"}]}}]} \ No newline at end of file diff --git a/Code/itf/tests/fixtures/votekeeper/voteBookkeeper_skipQuorumSinglePrevoteTest.itf.json b/Code/itf/tests/fixtures/votekeeper/voteBookkeeper_skipQuorumSinglePrevoteTest.itf.json deleted file mode 100644 index b682ef1d1..000000000 --- a/Code/itf/tests/fixtures/votekeeper/voteBookkeeper_skipQuorumSinglePrevoteTest.itf.json +++ /dev/null @@ -1 +0,0 @@ -{"#meta":{"format":"ITF","format-description":"https://apalache.informal.systems/docs/adr/015adr-trace.html","source":"voteBookkeeperTest.qnt","status":"passed","description":"Created by Quint on Fri Nov 17 2023 21:49:30 GMT+0100 (Central European Standard Time)","timestamp":1700254170360},"vars":["voteBookkeeperTest::voteBookkeeperSM::weightedVote","voteBookkeeperTest::voteBookkeeperSM::bookkeeper","voteBookkeeperTest::voteBookkeeperSM::lastEmitted"],"states":[{"#meta":{"index":0},"voteBookkeeperTest::voteBookkeeperSM::bookkeeper":{"currentRound":{"#bigint":"1"},"height":{"#bigint":"1"},"rounds":{"#map":[]},"totalWeight":{"#bigint":"80"}},"voteBookkeeperTest::voteBookkeeperSM::lastEmitted":{"name":"","round":{"#bigint":"-1"},"value":"null"},"voteBookkeeperTest::voteBookkeeperSM::weightedVote":{"#tup":[{"address":"","height":{"#bigint":"1"},"round":{"#bigint":"-1"},"typ":"","value":""},{"#bigint":"-1"}]}},{"#meta":{"index":1},"voteBookkeeperTest::voteBookkeeperSM::bookkeeper":{"currentRound":{"#bigint":"1"},"height":{"#bigint":"1"},"rounds":{"#map":[[{"#bigint":"1"},{"emittedEvents":{"#set":[]},"height":{"#bigint":"1"},"precommits":{"totalWeight":{"#bigint":"80"},"valuesWeights":{"#map":[]},"votesAddresses":{"#set":[]}},"prevotes":{"totalWeight":{"#bigint":"80"},"valuesWeights":{"#map":[["val1",{"#bigint":"50"}]]},"votesAddresses":{"#set":["alice"]}},"round":{"#bigint":"1"},"votesAddressesWeights":{"#map":[["alice",{"#bigint":"50"}]]}}]]},"totalWeight":{"#bigint":"80"}},"voteBookkeeperTest::voteBookkeeperSM::lastEmitted":{"name":"None","round":{"#bigint":"1"},"value":"null"},"voteBookkeeperTest::voteBookkeeperSM::weightedVote":{"#tup":[{"address":"alice","height":{"#bigint":"1"},"round":{"#bigint":"1"},"typ":"Prevote","value":"val1"},{"#bigint":"50"}]}},{"#meta":{"index":2},"voteBookkeeperTest::voteBookkeeperSM::bookkeeper":{"currentRound":{"#bigint":"1"},"height":{"#bigint":"1"},"rounds":{"#map":[[{"#bigint":"1"},{"emittedEvents":{"#set":[]},"height":{"#bigint":"1"},"precommits":{"totalWeight":{"#bigint":"80"},"valuesWeights":{"#map":[]},"votesAddresses":{"#set":[]}},"prevotes":{"totalWeight":{"#bigint":"80"},"valuesWeights":{"#map":[["val1",{"#bigint":"50"}]]},"votesAddresses":{"#set":["alice"]}},"round":{"#bigint":"1"},"votesAddressesWeights":{"#map":[["alice",{"#bigint":"50"}]]}}],[{"#bigint":"2"},{"emittedEvents":{"#set":[]},"height":{"#bigint":"1"},"precommits":{"totalWeight":{"#bigint":"80"},"valuesWeights":{"#map":[]},"votesAddresses":{"#set":[]}},"prevotes":{"totalWeight":{"#bigint":"80"},"valuesWeights":{"#map":[["val1",{"#bigint":"10"}]]},"votesAddresses":{"#set":["john"]}},"round":{"#bigint":"2"},"votesAddressesWeights":{"#map":[["john",{"#bigint":"10"}]]}}]]},"totalWeight":{"#bigint":"80"}},"voteBookkeeperTest::voteBookkeeperSM::lastEmitted":{"name":"None","round":{"#bigint":"2"},"value":"null"},"voteBookkeeperTest::voteBookkeeperSM::weightedVote":{"#tup":[{"address":"john","height":{"#bigint":"1"},"round":{"#bigint":"2"},"typ":"Prevote","value":"val1"},{"#bigint":"10"}]}},{"#meta":{"index":3},"voteBookkeeperTest::voteBookkeeperSM::bookkeeper":{"currentRound":{"#bigint":"1"},"height":{"#bigint":"1"},"rounds":{"#map":[[{"#bigint":"1"},{"emittedEvents":{"#set":[]},"height":{"#bigint":"1"},"precommits":{"totalWeight":{"#bigint":"80"},"valuesWeights":{"#map":[]},"votesAddresses":{"#set":[]}},"prevotes":{"totalWeight":{"#bigint":"80"},"valuesWeights":{"#map":[["val1",{"#bigint":"50"}]]},"votesAddresses":{"#set":["alice"]}},"round":{"#bigint":"1"},"votesAddressesWeights":{"#map":[["alice",{"#bigint":"50"}]]}}],[{"#bigint":"2"},{"emittedEvents":{"#set":[{"name":"Skip","round":{"#bigint":"2"},"value":"null"}]},"height":{"#bigint":"1"},"precommits":{"totalWeight":{"#bigint":"80"},"valuesWeights":{"#map":[["val1",{"#bigint":"20"}]]},"votesAddresses":{"#set":["bob"]}},"prevotes":{"totalWeight":{"#bigint":"80"},"valuesWeights":{"#map":[["val1",{"#bigint":"10"}]]},"votesAddresses":{"#set":["john"]}},"round":{"#bigint":"2"},"votesAddressesWeights":{"#map":[["bob",{"#bigint":"20"}],["john",{"#bigint":"10"}]]}}]]},"totalWeight":{"#bigint":"80"}},"voteBookkeeperTest::voteBookkeeperSM::lastEmitted":{"name":"Skip","round":{"#bigint":"2"},"value":"null"},"voteBookkeeperTest::voteBookkeeperSM::weightedVote":{"#tup":[{"address":"bob","height":{"#bigint":"1"},"round":{"#bigint":"2"},"typ":"Precommit","value":"val1"},{"#bigint":"20"}]}}]} \ No newline at end of file diff --git a/Code/itf/tests/fixtures/votekeeper/voteBookkeeper_skipSmallQuorumAllPrevotesTest.itf.json b/Code/itf/tests/fixtures/votekeeper/voteBookkeeper_skipSmallQuorumAllPrevotesTest.itf.json deleted file mode 100644 index 999287cc9..000000000 --- a/Code/itf/tests/fixtures/votekeeper/voteBookkeeper_skipSmallQuorumAllPrevotesTest.itf.json +++ /dev/null @@ -1 +0,0 @@ -{"#meta":{"format":"ITF","format-description":"https://apalache.informal.systems/docs/adr/015adr-trace.html","source":"voteBookkeeperTest.qnt","status":"passed","description":"Created by Quint on Fri Nov 17 2023 21:49:30 GMT+0100 (Central European Standard Time)","timestamp":1700254170358},"vars":["voteBookkeeperTest::voteBookkeeperSM::weightedVote","voteBookkeeperTest::voteBookkeeperSM::bookkeeper","voteBookkeeperTest::voteBookkeeperSM::lastEmitted"],"states":[{"#meta":{"index":0},"voteBookkeeperTest::voteBookkeeperSM::bookkeeper":{"currentRound":{"#bigint":"1"},"height":{"#bigint":"1"},"rounds":{"#map":[]},"totalWeight":{"#bigint":"80"}},"voteBookkeeperTest::voteBookkeeperSM::lastEmitted":{"name":"","round":{"#bigint":"-1"},"value":"null"},"voteBookkeeperTest::voteBookkeeperSM::weightedVote":{"#tup":[{"address":"","height":{"#bigint":"1"},"round":{"#bigint":"-1"},"typ":"","value":""},{"#bigint":"-1"}]}},{"#meta":{"index":1},"voteBookkeeperTest::voteBookkeeperSM::bookkeeper":{"currentRound":{"#bigint":"1"},"height":{"#bigint":"1"},"rounds":{"#map":[[{"#bigint":"1"},{"emittedEvents":{"#set":[]},"height":{"#bigint":"1"},"precommits":{"totalWeight":{"#bigint":"80"},"valuesWeights":{"#map":[]},"votesAddresses":{"#set":[]}},"prevotes":{"totalWeight":{"#bigint":"80"},"valuesWeights":{"#map":[["val1",{"#bigint":"50"}]]},"votesAddresses":{"#set":["alice"]}},"round":{"#bigint":"1"},"votesAddressesWeights":{"#map":[["alice",{"#bigint":"50"}]]}}]]},"totalWeight":{"#bigint":"80"}},"voteBookkeeperTest::voteBookkeeperSM::lastEmitted":{"name":"None","round":{"#bigint":"1"},"value":"null"},"voteBookkeeperTest::voteBookkeeperSM::weightedVote":{"#tup":[{"address":"alice","height":{"#bigint":"1"},"round":{"#bigint":"1"},"typ":"Prevote","value":"val1"},{"#bigint":"50"}]}},{"#meta":{"index":2},"voteBookkeeperTest::voteBookkeeperSM::bookkeeper":{"currentRound":{"#bigint":"1"},"height":{"#bigint":"1"},"rounds":{"#map":[[{"#bigint":"1"},{"emittedEvents":{"#set":[]},"height":{"#bigint":"1"},"precommits":{"totalWeight":{"#bigint":"80"},"valuesWeights":{"#map":[]},"votesAddresses":{"#set":[]}},"prevotes":{"totalWeight":{"#bigint":"80"},"valuesWeights":{"#map":[["val1",{"#bigint":"50"}]]},"votesAddresses":{"#set":["alice"]}},"round":{"#bigint":"1"},"votesAddressesWeights":{"#map":[["alice",{"#bigint":"50"}]]}}],[{"#bigint":"2"},{"emittedEvents":{"#set":[]},"height":{"#bigint":"1"},"precommits":{"totalWeight":{"#bigint":"80"},"valuesWeights":{"#map":[]},"votesAddresses":{"#set":[]}},"prevotes":{"totalWeight":{"#bigint":"80"},"valuesWeights":{"#map":[["val1",{"#bigint":"10"}]]},"votesAddresses":{"#set":["john"]}},"round":{"#bigint":"2"},"votesAddressesWeights":{"#map":[["john",{"#bigint":"10"}]]}}]]},"totalWeight":{"#bigint":"80"}},"voteBookkeeperTest::voteBookkeeperSM::lastEmitted":{"name":"None","round":{"#bigint":"2"},"value":"null"},"voteBookkeeperTest::voteBookkeeperSM::weightedVote":{"#tup":[{"address":"john","height":{"#bigint":"1"},"round":{"#bigint":"2"},"typ":"Prevote","value":"val1"},{"#bigint":"10"}]}},{"#meta":{"index":3},"voteBookkeeperTest::voteBookkeeperSM::bookkeeper":{"currentRound":{"#bigint":"1"},"height":{"#bigint":"1"},"rounds":{"#map":[[{"#bigint":"1"},{"emittedEvents":{"#set":[]},"height":{"#bigint":"1"},"precommits":{"totalWeight":{"#bigint":"80"},"valuesWeights":{"#map":[]},"votesAddresses":{"#set":[]}},"prevotes":{"totalWeight":{"#bigint":"80"},"valuesWeights":{"#map":[["val1",{"#bigint":"50"}]]},"votesAddresses":{"#set":["alice"]}},"round":{"#bigint":"1"},"votesAddressesWeights":{"#map":[["alice",{"#bigint":"50"}]]}}],[{"#bigint":"2"},{"emittedEvents":{"#set":[{"name":"Skip","round":{"#bigint":"2"},"value":"null"}]},"height":{"#bigint":"1"},"precommits":{"totalWeight":{"#bigint":"80"},"valuesWeights":{"#map":[["val1",{"#bigint":"20"}]]},"votesAddresses":{"#set":["bob"]}},"prevotes":{"totalWeight":{"#bigint":"80"},"valuesWeights":{"#map":[["val1",{"#bigint":"10"}]]},"votesAddresses":{"#set":["john"]}},"round":{"#bigint":"2"},"votesAddressesWeights":{"#map":[["bob",{"#bigint":"20"}],["john",{"#bigint":"10"}]]}}]]},"totalWeight":{"#bigint":"80"}},"voteBookkeeperTest::voteBookkeeperSM::lastEmitted":{"name":"Skip","round":{"#bigint":"2"},"value":"null"},"voteBookkeeperTest::voteBookkeeperSM::weightedVote":{"#tup":[{"address":"bob","height":{"#bigint":"1"},"round":{"#bigint":"2"},"typ":"Precommit","value":"val1"},{"#bigint":"20"}]}}]} \ No newline at end of file diff --git a/Code/itf/tests/fixtures/votekeeper/voteBookkeeper_skipSmallQuorumMixedVotesTwoValsTest.itf.json b/Code/itf/tests/fixtures/votekeeper/voteBookkeeper_skipSmallQuorumMixedVotesTwoValsTest.itf.json deleted file mode 100644 index b76ad5e91..000000000 --- a/Code/itf/tests/fixtures/votekeeper/voteBookkeeper_skipSmallQuorumMixedVotesTwoValsTest.itf.json +++ /dev/null @@ -1 +0,0 @@ -{"#meta":{"format":"ITF","format-description":"https://apalache.informal.systems/docs/adr/015adr-trace.html","source":"voteBookkeeperTest.qnt","status":"passed","description":"Created by Quint on Fri Nov 17 2023 21:51:30 GMT+0100 (Central European Standard Time)","timestamp":1700254290114},"vars":["voteBookkeeperTest::voteBookkeeperSM::weightedVote","voteBookkeeperTest::voteBookkeeperSM::bookkeeper","voteBookkeeperTest::voteBookkeeperSM::lastEmitted"],"states":[{"#meta":{"index":0},"voteBookkeeperTest::voteBookkeeperSM::bookkeeper":{"currentRound":{"#bigint":"1"},"height":{"#bigint":"1"},"rounds":{"#map":[]},"totalWeight":{"#bigint":"80"}},"voteBookkeeperTest::voteBookkeeperSM::lastEmitted":{"name":"","round":{"#bigint":"-1"},"value":"null"},"voteBookkeeperTest::voteBookkeeperSM::weightedVote":{"#tup":[{"address":"","height":{"#bigint":"1"},"round":{"#bigint":"-1"},"typ":"","value":""},{"#bigint":"-1"}]}},{"#meta":{"index":1},"voteBookkeeperTest::voteBookkeeperSM::bookkeeper":{"currentRound":{"#bigint":"1"},"height":{"#bigint":"1"},"rounds":{"#map":[[{"#bigint":"1"},{"emittedEvents":{"#set":[]},"height":{"#bigint":"1"},"precommits":{"totalWeight":{"#bigint":"80"},"valuesWeights":{"#map":[]},"votesAddresses":{"#set":[]}},"prevotes":{"totalWeight":{"#bigint":"80"},"valuesWeights":{"#map":[["val1",{"#bigint":"50"}]]},"votesAddresses":{"#set":["alice"]}},"round":{"#bigint":"1"},"votesAddressesWeights":{"#map":[["alice",{"#bigint":"50"}]]}}]]},"totalWeight":{"#bigint":"80"}},"voteBookkeeperTest::voteBookkeeperSM::lastEmitted":{"name":"None","round":{"#bigint":"1"},"value":"null"},"voteBookkeeperTest::voteBookkeeperSM::weightedVote":{"#tup":[{"address":"alice","height":{"#bigint":"1"},"round":{"#bigint":"1"},"typ":"Prevote","value":"val1"},{"#bigint":"50"}]}},{"#meta":{"index":2},"voteBookkeeperTest::voteBookkeeperSM::bookkeeper":{"currentRound":{"#bigint":"1"},"height":{"#bigint":"1"},"rounds":{"#map":[[{"#bigint":"1"},{"emittedEvents":{"#set":[]},"height":{"#bigint":"1"},"precommits":{"totalWeight":{"#bigint":"80"},"valuesWeights":{"#map":[]},"votesAddresses":{"#set":[]}},"prevotes":{"totalWeight":{"#bigint":"80"},"valuesWeights":{"#map":[["val1",{"#bigint":"50"}]]},"votesAddresses":{"#set":["alice"]}},"round":{"#bigint":"1"},"votesAddressesWeights":{"#map":[["alice",{"#bigint":"50"}]]}}],[{"#bigint":"2"},{"emittedEvents":{"#set":[]},"height":{"#bigint":"1"},"precommits":{"totalWeight":{"#bigint":"80"},"valuesWeights":{"#map":[]},"votesAddresses":{"#set":[]}},"prevotes":{"totalWeight":{"#bigint":"80"},"valuesWeights":{"#map":[["val1",{"#bigint":"10"}]]},"votesAddresses":{"#set":["john"]}},"round":{"#bigint":"2"},"votesAddressesWeights":{"#map":[["john",{"#bigint":"10"}]]}}]]},"totalWeight":{"#bigint":"80"}},"voteBookkeeperTest::voteBookkeeperSM::lastEmitted":{"name":"None","round":{"#bigint":"2"},"value":"null"},"voteBookkeeperTest::voteBookkeeperSM::weightedVote":{"#tup":[{"address":"john","height":{"#bigint":"1"},"round":{"#bigint":"2"},"typ":"Prevote","value":"val1"},{"#bigint":"10"}]}},{"#meta":{"index":3},"voteBookkeeperTest::voteBookkeeperSM::bookkeeper":{"currentRound":{"#bigint":"1"},"height":{"#bigint":"1"},"rounds":{"#map":[[{"#bigint":"1"},{"emittedEvents":{"#set":[]},"height":{"#bigint":"1"},"precommits":{"totalWeight":{"#bigint":"80"},"valuesWeights":{"#map":[]},"votesAddresses":{"#set":[]}},"prevotes":{"totalWeight":{"#bigint":"80"},"valuesWeights":{"#map":[["val1",{"#bigint":"50"}]]},"votesAddresses":{"#set":["alice"]}},"round":{"#bigint":"1"},"votesAddressesWeights":{"#map":[["alice",{"#bigint":"50"}]]}}],[{"#bigint":"2"},{"emittedEvents":{"#set":[{"name":"Skip","round":{"#bigint":"2"},"value":"null"}]},"height":{"#bigint":"1"},"precommits":{"totalWeight":{"#bigint":"80"},"valuesWeights":{"#map":[["val1",{"#bigint":"20"}]]},"votesAddresses":{"#set":["bob"]}},"prevotes":{"totalWeight":{"#bigint":"80"},"valuesWeights":{"#map":[["val1",{"#bigint":"10"}]]},"votesAddresses":{"#set":["john"]}},"round":{"#bigint":"2"},"votesAddressesWeights":{"#map":[["bob",{"#bigint":"20"}],["john",{"#bigint":"10"}]]}}]]},"totalWeight":{"#bigint":"80"}},"voteBookkeeperTest::voteBookkeeperSM::lastEmitted":{"name":"Skip","round":{"#bigint":"2"},"value":"null"},"voteBookkeeperTest::voteBookkeeperSM::weightedVote":{"#tup":[{"address":"bob","height":{"#bigint":"1"},"round":{"#bigint":"2"},"typ":"Precommit","value":"val1"},{"#bigint":"20"}]}}]} \ No newline at end of file diff --git a/Code/itf/tests/fixtures/votekeeper/voteBookkeeper_synchronousConsensusTest.itf.json b/Code/itf/tests/fixtures/votekeeper/voteBookkeeper_synchronousConsensusTest.itf.json deleted file mode 100644 index c66108d98..000000000 --- a/Code/itf/tests/fixtures/votekeeper/voteBookkeeper_synchronousConsensusTest.itf.json +++ /dev/null @@ -1 +0,0 @@ -{"#meta":{"format":"ITF","format-description":"https://apalache.informal.systems/docs/adr/015adr-trace.html","source":"voteBookkeeperTest.qnt","status":"passed","description":"Created by Quint on Fri Nov 17 2023 21:53:17 GMT+0100 (Central European Standard Time)","timestamp":1700254397757},"vars":["voteBookkeeperTest::voteBookkeeperSM::weightedVote","voteBookkeeperTest::voteBookkeeperSM::bookkeeper","voteBookkeeperTest::voteBookkeeperSM::lastEmitted"],"states":[{"#meta":{"index":0},"voteBookkeeperTest::voteBookkeeperSM::bookkeeper":{"currentRound":{"#bigint":"1"},"height":{"#bigint":"1"},"rounds":{"#map":[]},"totalWeight":{"#bigint":"100"}},"voteBookkeeperTest::voteBookkeeperSM::lastEmitted":{"name":"","round":{"#bigint":"-1"},"value":"null"},"voteBookkeeperTest::voteBookkeeperSM::weightedVote":{"#tup":[{"address":"","height":{"#bigint":"1"},"round":{"#bigint":"-1"},"typ":"","value":""},{"#bigint":"-1"}]}},{"#meta":{"index":1},"voteBookkeeperTest::voteBookkeeperSM::bookkeeper":{"currentRound":{"#bigint":"1"},"height":{"#bigint":"1"},"rounds":{"#map":[[{"#bigint":"1"},{"emittedEvents":{"#set":[]},"height":{"#bigint":"1"},"precommits":{"totalWeight":{"#bigint":"100"},"valuesWeights":{"#map":[]},"votesAddresses":{"#set":[]}},"prevotes":{"totalWeight":{"#bigint":"100"},"valuesWeights":{"#map":[["val1",{"#bigint":"60"}]]},"votesAddresses":{"#set":["alice"]}},"round":{"#bigint":"1"},"votesAddressesWeights":{"#map":[["alice",{"#bigint":"60"}]]}}]]},"totalWeight":{"#bigint":"100"}},"voteBookkeeperTest::voteBookkeeperSM::lastEmitted":{"name":"None","round":{"#bigint":"1"},"value":"null"},"voteBookkeeperTest::voteBookkeeperSM::weightedVote":{"#tup":[{"address":"alice","height":{"#bigint":"1"},"round":{"#bigint":"1"},"typ":"Prevote","value":"val1"},{"#bigint":"60"}]}},{"#meta":{"index":2},"voteBookkeeperTest::voteBookkeeperSM::bookkeeper":{"currentRound":{"#bigint":"1"},"height":{"#bigint":"1"},"rounds":{"#map":[[{"#bigint":"1"},{"emittedEvents":{"#set":[{"name":"PolkaValue","round":{"#bigint":"1"},"value":"val1"}]},"height":{"#bigint":"1"},"precommits":{"totalWeight":{"#bigint":"100"},"valuesWeights":{"#map":[]},"votesAddresses":{"#set":[]}},"prevotes":{"totalWeight":{"#bigint":"100"},"valuesWeights":{"#map":[["val1",{"#bigint":"70"}]]},"votesAddresses":{"#set":["alice","john"]}},"round":{"#bigint":"1"},"votesAddressesWeights":{"#map":[["alice",{"#bigint":"60"}],["john",{"#bigint":"10"}]]}}]]},"totalWeight":{"#bigint":"100"}},"voteBookkeeperTest::voteBookkeeperSM::lastEmitted":{"name":"PolkaValue","round":{"#bigint":"1"},"value":"val1"},"voteBookkeeperTest::voteBookkeeperSM::weightedVote":{"#tup":[{"address":"john","height":{"#bigint":"1"},"round":{"#bigint":"1"},"typ":"Prevote","value":"val1"},{"#bigint":"10"}]}},{"#meta":{"index":3},"voteBookkeeperTest::voteBookkeeperSM::bookkeeper":{"currentRound":{"#bigint":"1"},"height":{"#bigint":"1"},"rounds":{"#map":[[{"#bigint":"1"},{"emittedEvents":{"#set":[{"name":"PolkaValue","round":{"#bigint":"1"},"value":"val1"}]},"height":{"#bigint":"1"},"precommits":{"totalWeight":{"#bigint":"100"},"valuesWeights":{"#map":[]},"votesAddresses":{"#set":[]}},"prevotes":{"totalWeight":{"#bigint":"100"},"valuesWeights":{"#map":[["val1",{"#bigint":"100"}]]},"votesAddresses":{"#set":["alice","bob","john"]}},"round":{"#bigint":"1"},"votesAddressesWeights":{"#map":[["alice",{"#bigint":"60"}],["bob",{"#bigint":"30"}],["john",{"#bigint":"10"}]]}}]]},"totalWeight":{"#bigint":"100"}},"voteBookkeeperTest::voteBookkeeperSM::lastEmitted":{"name":"None","round":{"#bigint":"1"},"value":"null"},"voteBookkeeperTest::voteBookkeeperSM::weightedVote":{"#tup":[{"address":"bob","height":{"#bigint":"1"},"round":{"#bigint":"1"},"typ":"Prevote","value":"val1"},{"#bigint":"30"}]}},{"#meta":{"index":4},"voteBookkeeperTest::voteBookkeeperSM::bookkeeper":{"currentRound":{"#bigint":"1"},"height":{"#bigint":"1"},"rounds":{"#map":[[{"#bigint":"1"},{"emittedEvents":{"#set":[{"name":"PolkaValue","round":{"#bigint":"1"},"value":"val1"}]},"height":{"#bigint":"1"},"precommits":{"totalWeight":{"#bigint":"100"},"valuesWeights":{"#map":[["val1",{"#bigint":"30"}]]},"votesAddresses":{"#set":["bob"]}},"prevotes":{"totalWeight":{"#bigint":"100"},"valuesWeights":{"#map":[["val1",{"#bigint":"100"}]]},"votesAddresses":{"#set":["alice","bob","john"]}},"round":{"#bigint":"1"},"votesAddressesWeights":{"#map":[["alice",{"#bigint":"60"}],["bob",{"#bigint":"30"}],["john",{"#bigint":"10"}]]}}]]},"totalWeight":{"#bigint":"100"}},"voteBookkeeperTest::voteBookkeeperSM::lastEmitted":{"name":"None","round":{"#bigint":"1"},"value":"null"},"voteBookkeeperTest::voteBookkeeperSM::weightedVote":{"#tup":[{"address":"bob","height":{"#bigint":"1"},"round":{"#bigint":"1"},"typ":"Precommit","value":"val1"},{"#bigint":"30"}]}},{"#meta":{"index":5},"voteBookkeeperTest::voteBookkeeperSM::bookkeeper":{"currentRound":{"#bigint":"1"},"height":{"#bigint":"1"},"rounds":{"#map":[[{"#bigint":"1"},{"emittedEvents":{"#set":[{"name":"PolkaValue","round":{"#bigint":"1"},"value":"val1"}]},"height":{"#bigint":"1"},"precommits":{"totalWeight":{"#bigint":"100"},"valuesWeights":{"#map":[["val1",{"#bigint":"40"}]]},"votesAddresses":{"#set":["bob","john"]}},"prevotes":{"totalWeight":{"#bigint":"100"},"valuesWeights":{"#map":[["val1",{"#bigint":"100"}]]},"votesAddresses":{"#set":["alice","bob","john"]}},"round":{"#bigint":"1"},"votesAddressesWeights":{"#map":[["alice",{"#bigint":"60"}],["bob",{"#bigint":"30"}],["john",{"#bigint":"10"}]]}}]]},"totalWeight":{"#bigint":"100"}},"voteBookkeeperTest::voteBookkeeperSM::lastEmitted":{"name":"None","round":{"#bigint":"1"},"value":"null"},"voteBookkeeperTest::voteBookkeeperSM::weightedVote":{"#tup":[{"address":"john","height":{"#bigint":"1"},"round":{"#bigint":"1"},"typ":"Precommit","value":"val1"},{"#bigint":"10"}]}},{"#meta":{"index":6},"voteBookkeeperTest::voteBookkeeperSM::bookkeeper":{"currentRound":{"#bigint":"1"},"height":{"#bigint":"1"},"rounds":{"#map":[[{"#bigint":"1"},{"emittedEvents":{"#set":[{"name":"PolkaValue","round":{"#bigint":"1"},"value":"val1"},{"name":"PrecommitValue","round":{"#bigint":"1"},"value":"val1"}]},"height":{"#bigint":"1"},"precommits":{"totalWeight":{"#bigint":"100"},"valuesWeights":{"#map":[["val1",{"#bigint":"100"}]]},"votesAddresses":{"#set":["alice","bob","john"]}},"prevotes":{"totalWeight":{"#bigint":"100"},"valuesWeights":{"#map":[["val1",{"#bigint":"100"}]]},"votesAddresses":{"#set":["alice","bob","john"]}},"round":{"#bigint":"1"},"votesAddressesWeights":{"#map":[["alice",{"#bigint":"60"}],["bob",{"#bigint":"30"}],["john",{"#bigint":"10"}]]}}]]},"totalWeight":{"#bigint":"100"}},"voteBookkeeperTest::voteBookkeeperSM::lastEmitted":{"name":"PrecommitValue","round":{"#bigint":"1"},"value":"val1"},"voteBookkeeperTest::voteBookkeeperSM::weightedVote":{"#tup":[{"address":"alice","height":{"#bigint":"1"},"round":{"#bigint":"1"},"typ":"Precommit","value":"val1"},{"#bigint":"60"}]}}]} \ No newline at end of file