diff --git a/Code/itf/tests/fixtures/votekeeper.itf.json b/Code/itf/tests/fixtures/votekeeper.itf.json deleted file mode 100644 index 226b288d6..000000000 --- a/Code/itf/tests/fixtures/votekeeper.itf.json +++ /dev/null @@ -1,2702 +0,0 @@ -{ - "#meta": { - "format": "ITF", - "format-description": "https://apalache.informal.systems/docs/adr/015adr-trace.html", - "source": "voteBookkeeper.qnt", - "status": "ok", - "description": "Created by Quint on Fri Nov 10 2023 13:41:10 GMT+0100 (GMT+01:00)", - "timestamp": 1699620070943 - }, - "vars": [ - "lastEmitted", - "bookkeeper" - ], - "states": [ - { - "#meta": { - "index": 0 - }, - "bookkeeper": { - "height": { - "#bigint": "10" - }, - "rounds": { - "#map": [] - }, - "totalWeight": { - "#bigint": "100" - } - }, - "lastEmitted": { - "name": "", - "round": { - "#bigint": "-1" - }, - "value": "null" - } - }, - { - "#meta": { - "index": 1 - }, - "bookkeeper": { - "height": { - "#bigint": "10" - }, - "rounds": { - "#map": [ - [ - { - "#bigint": "1" - }, - { - "emittedEvents": { - "#set": [] - }, - "height": { - "#bigint": "10" - }, - "precommits": { - "totalWeight": { - "#bigint": "100" - }, - "valuesWeights": { - "#map": [ - [ - "null", - { - "#bigint": "60" - } - ] - ] - }, - "votesAddresses": { - "#set": [ - "alice" - ] - } - }, - "prevotes": { - "totalWeight": { - "#bigint": "100" - }, - "valuesWeights": { - "#map": [] - }, - "votesAddresses": { - "#set": [] - } - }, - "round": { - "#bigint": "1" - }, - "votesAddressesWeights": { - "#map": [ - [ - "alice", - { - "#bigint": "60" - } - ] - ] - } - } - ] - ] - }, - "totalWeight": { - "#bigint": "100" - } - }, - "lastEmitted": { - "name": "None", - "round": { - "#bigint": "1" - }, - "value": "null" - } - }, - { - "#meta": { - "index": 2 - }, - "bookkeeper": { - "height": { - "#bigint": "10" - }, - "rounds": { - "#map": [ - [ - { - "#bigint": "1" - }, - { - "emittedEvents": { - "#set": [] - }, - "height": { - "#bigint": "10" - }, - "precommits": { - "totalWeight": { - "#bigint": "100" - }, - "valuesWeights": { - "#map": [ - [ - "null", - { - "#bigint": "60" - } - ] - ] - }, - "votesAddresses": { - "#set": [ - "alice" - ] - } - }, - "prevotes": { - "totalWeight": { - "#bigint": "100" - }, - "valuesWeights": { - "#map": [ - [ - "proposal", - { - "#bigint": "30" - } - ] - ] - }, - "votesAddresses": { - "#set": [ - "bob" - ] - } - }, - "round": { - "#bigint": "1" - }, - "votesAddressesWeights": { - "#map": [ - [ - "alice", - { - "#bigint": "60" - } - ], - [ - "bob", - { - "#bigint": "30" - } - ] - ] - } - } - ] - ] - }, - "totalWeight": { - "#bigint": "100" - } - }, - "lastEmitted": { - "name": "None", - "round": { - "#bigint": "1" - }, - "value": "null" - } - }, - { - "#meta": { - "index": 3 - }, - "bookkeeper": { - "height": { - "#bigint": "10" - }, - "rounds": { - "#map": [ - [ - { - "#bigint": "1" - }, - { - "emittedEvents": { - "#set": [ - { - "name": "PolkaAny", - "round": { - "#bigint": "1" - }, - "value": "null" - } - ] - }, - "height": { - "#bigint": "10" - }, - "precommits": { - "totalWeight": { - "#bigint": "100" - }, - "valuesWeights": { - "#map": [ - [ - "null", - { - "#bigint": "60" - } - ] - ] - }, - "votesAddresses": { - "#set": [ - "alice" - ] - } - }, - "prevotes": { - "totalWeight": { - "#bigint": "100" - }, - "valuesWeights": { - "#map": [ - [ - "null", - { - "#bigint": "60" - } - ], - [ - "proposal", - { - "#bigint": "30" - } - ] - ] - }, - "votesAddresses": { - "#set": [ - "alice", - "bob" - ] - } - }, - "round": { - "#bigint": "1" - }, - "votesAddressesWeights": { - "#map": [ - [ - "alice", - { - "#bigint": "60" - } - ], - [ - "bob", - { - "#bigint": "30" - } - ] - ] - } - } - ] - ] - }, - "totalWeight": { - "#bigint": "100" - } - }, - "lastEmitted": { - "name": "PolkaAny", - "round": { - "#bigint": "1" - }, - "value": "null" - } - }, - { - "#meta": { - "index": 4 - }, - "bookkeeper": { - "height": { - "#bigint": "10" - }, - "rounds": { - "#map": [ - [ - { - "#bigint": "1" - }, - { - "emittedEvents": { - "#set": [ - { - "name": "PolkaAny", - "round": { - "#bigint": "1" - }, - "value": "null" - } - ] - }, - "height": { - "#bigint": "10" - }, - "precommits": { - "totalWeight": { - "#bigint": "100" - }, - "valuesWeights": { - "#map": [ - [ - "null", - { - "#bigint": "60" - } - ] - ] - }, - "votesAddresses": { - "#set": [ - "alice" - ] - } - }, - "prevotes": { - "totalWeight": { - "#bigint": "100" - }, - "valuesWeights": { - "#map": [ - [ - "null", - { - "#bigint": "60" - } - ], - [ - "proposal", - { - "#bigint": "30" - } - ] - ] - }, - "votesAddresses": { - "#set": [ - "alice", - "bob" - ] - } - }, - "round": { - "#bigint": "1" - }, - "votesAddressesWeights": { - "#map": [ - [ - "alice", - { - "#bigint": "60" - } - ], - [ - "bob", - { - "#bigint": "30" - } - ] - ] - } - } - ] - ] - }, - "totalWeight": { - "#bigint": "100" - } - }, - "lastEmitted": { - "name": "None", - "round": { - "#bigint": "1" - }, - "value": "null" - } - }, - { - "#meta": { - "index": 5 - }, - "bookkeeper": { - "height": { - "#bigint": "10" - }, - "rounds": { - "#map": [ - [ - { - "#bigint": "1" - }, - { - "emittedEvents": { - "#set": [ - { - "name": "PolkaAny", - "round": { - "#bigint": "1" - }, - "value": "null" - }, - { - "name": "PrecommitAny", - "round": { - "#bigint": "1" - }, - "value": "null" - } - ] - }, - "height": { - "#bigint": "10" - }, - "precommits": { - "totalWeight": { - "#bigint": "100" - }, - "valuesWeights": { - "#map": [ - [ - "null", - { - "#bigint": "60" - } - ], - [ - "proposal", - { - "#bigint": "10" - } - ] - ] - }, - "votesAddresses": { - "#set": [ - "alice", - "john" - ] - } - }, - "prevotes": { - "totalWeight": { - "#bigint": "100" - }, - "valuesWeights": { - "#map": [ - [ - "null", - { - "#bigint": "60" - } - ], - [ - "proposal", - { - "#bigint": "30" - } - ] - ] - }, - "votesAddresses": { - "#set": [ - "alice", - "bob" - ] - } - }, - "round": { - "#bigint": "1" - }, - "votesAddressesWeights": { - "#map": [ - [ - "alice", - { - "#bigint": "60" - } - ], - [ - "bob", - { - "#bigint": "30" - } - ], - [ - "john", - { - "#bigint": "10" - } - ] - ] - } - } - ] - ] - }, - "totalWeight": { - "#bigint": "100" - } - }, - "lastEmitted": { - "name": "PrecommitAny", - "round": { - "#bigint": "1" - }, - "value": "null" - } - }, - { - "#meta": { - "index": 6 - }, - "bookkeeper": { - "height": { - "#bigint": "10" - }, - "rounds": { - "#map": [ - [ - { - "#bigint": "1" - }, - { - "emittedEvents": { - "#set": [ - { - "name": "PolkaAny", - "round": { - "#bigint": "1" - }, - "value": "null" - }, - { - "name": "PrecommitAny", - "round": { - "#bigint": "1" - }, - "value": "null" - }, - { - "name": "PrecommitValue", - "round": { - "#bigint": "1" - }, - "value": "null" - } - ] - }, - "height": { - "#bigint": "10" - }, - "precommits": { - "totalWeight": { - "#bigint": "100" - }, - "valuesWeights": { - "#map": [ - [ - "null", - { - "#bigint": "90" - } - ], - [ - "proposal", - { - "#bigint": "10" - } - ] - ] - }, - "votesAddresses": { - "#set": [ - "alice", - "bob", - "john" - ] - } - }, - "prevotes": { - "totalWeight": { - "#bigint": "100" - }, - "valuesWeights": { - "#map": [ - [ - "null", - { - "#bigint": "60" - } - ], - [ - "proposal", - { - "#bigint": "30" - } - ] - ] - }, - "votesAddresses": { - "#set": [ - "alice", - "bob" - ] - } - }, - "round": { - "#bigint": "1" - }, - "votesAddressesWeights": { - "#map": [ - [ - "alice", - { - "#bigint": "60" - } - ], - [ - "bob", - { - "#bigint": "30" - } - ], - [ - "john", - { - "#bigint": "10" - } - ] - ] - } - } - ] - ] - }, - "totalWeight": { - "#bigint": "100" - } - }, - "lastEmitted": { - "name": "PrecommitValue", - "round": { - "#bigint": "1" - }, - "value": "null" - } - }, - { - "#meta": { - "index": 7 - }, - "bookkeeper": { - "height": { - "#bigint": "10" - }, - "rounds": { - "#map": [ - [ - { - "#bigint": "1" - }, - { - "emittedEvents": { - "#set": [ - { - "name": "PolkaAny", - "round": { - "#bigint": "1" - }, - "value": "null" - }, - { - "name": "PrecommitAny", - "round": { - "#bigint": "1" - }, - "value": "null" - }, - { - "name": "PrecommitValue", - "round": { - "#bigint": "1" - }, - "value": "null" - } - ] - }, - "height": { - "#bigint": "10" - }, - "precommits": { - "totalWeight": { - "#bigint": "100" - }, - "valuesWeights": { - "#map": [ - [ - "null", - { - "#bigint": "90" - } - ], - [ - "proposal", - { - "#bigint": "10" - } - ] - ] - }, - "votesAddresses": { - "#set": [ - "alice", - "bob", - "john" - ] - } - }, - "prevotes": { - "totalWeight": { - "#bigint": "100" - }, - "valuesWeights": { - "#map": [ - [ - "null", - { - "#bigint": "60" - } - ], - [ - "proposal", - { - "#bigint": "30" - } - ] - ] - }, - "votesAddresses": { - "#set": [ - "alice", - "bob" - ] - } - }, - "round": { - "#bigint": "1" - }, - "votesAddressesWeights": { - "#map": [ - [ - "alice", - { - "#bigint": "60" - } - ], - [ - "bob", - { - "#bigint": "30" - } - ], - [ - "john", - { - "#bigint": "10" - } - ] - ] - } - } - ] - ] - }, - "totalWeight": { - "#bigint": "100" - } - }, - "lastEmitted": { - "name": "None", - "round": { - "#bigint": "1" - }, - "value": "null" - } - }, - { - "#meta": { - "index": 8 - }, - "bookkeeper": { - "height": { - "#bigint": "10" - }, - "rounds": { - "#map": [ - [ - { - "#bigint": "1" - }, - { - "emittedEvents": { - "#set": [ - { - "name": "PolkaAny", - "round": { - "#bigint": "1" - }, - "value": "null" - }, - { - "name": "PrecommitAny", - "round": { - "#bigint": "1" - }, - "value": "null" - }, - { - "name": "PrecommitValue", - "round": { - "#bigint": "1" - }, - "value": "null" - } - ] - }, - "height": { - "#bigint": "10" - }, - "precommits": { - "totalWeight": { - "#bigint": "100" - }, - "valuesWeights": { - "#map": [ - [ - "null", - { - "#bigint": "90" - } - ], - [ - "proposal", - { - "#bigint": "10" - } - ] - ] - }, - "votesAddresses": { - "#set": [ - "alice", - "bob", - "john" - ] - } - }, - "prevotes": { - "totalWeight": { - "#bigint": "100" - }, - "valuesWeights": { - "#map": [ - [ - "null", - { - "#bigint": "60" - } - ], - [ - "proposal", - { - "#bigint": "30" - } - ] - ] - }, - "votesAddresses": { - "#set": [ - "alice", - "bob" - ] - } - }, - "round": { - "#bigint": "1" - }, - "votesAddressesWeights": { - "#map": [ - [ - "alice", - { - "#bigint": "60" - } - ], - [ - "bob", - { - "#bigint": "30" - } - ], - [ - "john", - { - "#bigint": "10" - } - ] - ] - } - } - ] - ] - }, - "totalWeight": { - "#bigint": "100" - } - }, - "lastEmitted": { - "name": "None", - "round": { - "#bigint": "1" - }, - "value": "null" - } - }, - { - "#meta": { - "index": 9 - }, - "bookkeeper": { - "height": { - "#bigint": "10" - }, - "rounds": { - "#map": [ - [ - { - "#bigint": "1" - }, - { - "emittedEvents": { - "#set": [ - { - "name": "PolkaAny", - "round": { - "#bigint": "1" - }, - "value": "null" - }, - { - "name": "PrecommitAny", - "round": { - "#bigint": "1" - }, - "value": "null" - }, - { - "name": "PrecommitValue", - "round": { - "#bigint": "1" - }, - "value": "null" - } - ] - }, - "height": { - "#bigint": "10" - }, - "precommits": { - "totalWeight": { - "#bigint": "100" - }, - "valuesWeights": { - "#map": [ - [ - "null", - { - "#bigint": "90" - } - ], - [ - "proposal", - { - "#bigint": "10" - } - ] - ] - }, - "votesAddresses": { - "#set": [ - "alice", - "bob", - "john" - ] - } - }, - "prevotes": { - "totalWeight": { - "#bigint": "100" - }, - "valuesWeights": { - "#map": [ - [ - "null", - { - "#bigint": "60" - } - ], - [ - "proposal", - { - "#bigint": "30" - } - ] - ] - }, - "votesAddresses": { - "#set": [ - "alice", - "bob" - ] - } - }, - "round": { - "#bigint": "1" - }, - "votesAddressesWeights": { - "#map": [ - [ - "alice", - { - "#bigint": "60" - } - ], - [ - "bob", - { - "#bigint": "30" - } - ], - [ - "john", - { - "#bigint": "10" - } - ] - ] - } - } - ] - ] - }, - "totalWeight": { - "#bigint": "100" - } - }, - "lastEmitted": { - "name": "None", - "round": { - "#bigint": "1" - }, - "value": "null" - } - }, - { - "#meta": { - "index": 10 - }, - "bookkeeper": { - "height": { - "#bigint": "10" - }, - "rounds": { - "#map": [ - [ - { - "#bigint": "1" - }, - { - "emittedEvents": { - "#set": [ - { - "name": "PolkaAny", - "round": { - "#bigint": "1" - }, - "value": "null" - }, - { - "name": "PrecommitAny", - "round": { - "#bigint": "1" - }, - "value": "null" - }, - { - "name": "PrecommitValue", - "round": { - "#bigint": "1" - }, - "value": "null" - } - ] - }, - "height": { - "#bigint": "10" - }, - "precommits": { - "totalWeight": { - "#bigint": "100" - }, - "valuesWeights": { - "#map": [ - [ - "null", - { - "#bigint": "90" - } - ], - [ - "proposal", - { - "#bigint": "10" - } - ] - ] - }, - "votesAddresses": { - "#set": [ - "alice", - "bob", - "john" - ] - } - }, - "prevotes": { - "totalWeight": { - "#bigint": "100" - }, - "valuesWeights": { - "#map": [ - [ - "null", - { - "#bigint": "60" - } - ], - [ - "proposal", - { - "#bigint": "30" - } - ] - ] - }, - "votesAddresses": { - "#set": [ - "alice", - "bob" - ] - } - }, - "round": { - "#bigint": "1" - }, - "votesAddressesWeights": { - "#map": [ - [ - "alice", - { - "#bigint": "60" - } - ], - [ - "bob", - { - "#bigint": "30" - } - ], - [ - "john", - { - "#bigint": "10" - } - ] - ] - } - } - ] - ] - }, - "totalWeight": { - "#bigint": "100" - } - }, - "lastEmitted": { - "name": "None", - "round": { - "#bigint": "1" - }, - "value": "null" - } - }, - { - "#meta": { - "index": 11 - }, - "bookkeeper": { - "height": { - "#bigint": "10" - }, - "rounds": { - "#map": [ - [ - { - "#bigint": "1" - }, - { - "emittedEvents": { - "#set": [ - { - "name": "PolkaAny", - "round": { - "#bigint": "1" - }, - "value": "null" - }, - { - "name": "PrecommitAny", - "round": { - "#bigint": "1" - }, - "value": "null" - }, - { - "name": "PrecommitValue", - "round": { - "#bigint": "1" - }, - "value": "null" - } - ] - }, - "height": { - "#bigint": "10" - }, - "precommits": { - "totalWeight": { - "#bigint": "100" - }, - "valuesWeights": { - "#map": [ - [ - "null", - { - "#bigint": "90" - } - ], - [ - "proposal", - { - "#bigint": "10" - } - ] - ] - }, - "votesAddresses": { - "#set": [ - "alice", - "bob", - "john" - ] - } - }, - "prevotes": { - "totalWeight": { - "#bigint": "100" - }, - "valuesWeights": { - "#map": [ - [ - "null", - { - "#bigint": "60" - } - ], - [ - "proposal", - { - "#bigint": "30" - } - ] - ] - }, - "votesAddresses": { - "#set": [ - "alice", - "bob" - ] - } - }, - "round": { - "#bigint": "1" - }, - "votesAddressesWeights": { - "#map": [ - [ - "alice", - { - "#bigint": "60" - } - ], - [ - "bob", - { - "#bigint": "30" - } - ], - [ - "john", - { - "#bigint": "10" - } - ] - ] - } - } - ] - ] - }, - "totalWeight": { - "#bigint": "100" - } - }, - "lastEmitted": { - "name": "None", - "round": { - "#bigint": "1" - }, - "value": "null" - } - }, - { - "#meta": { - "index": 12 - }, - "bookkeeper": { - "height": { - "#bigint": "10" - }, - "rounds": { - "#map": [ - [ - { - "#bigint": "1" - }, - { - "emittedEvents": { - "#set": [ - { - "name": "PolkaAny", - "round": { - "#bigint": "1" - }, - "value": "null" - }, - { - "name": "PrecommitAny", - "round": { - "#bigint": "1" - }, - "value": "null" - }, - { - "name": "PrecommitValue", - "round": { - "#bigint": "1" - }, - "value": "null" - } - ] - }, - "height": { - "#bigint": "10" - }, - "precommits": { - "totalWeight": { - "#bigint": "100" - }, - "valuesWeights": { - "#map": [ - [ - "null", - { - "#bigint": "90" - } - ], - [ - "proposal", - { - "#bigint": "10" - } - ] - ] - }, - "votesAddresses": { - "#set": [ - "alice", - "bob", - "john" - ] - } - }, - "prevotes": { - "totalWeight": { - "#bigint": "100" - }, - "valuesWeights": { - "#map": [ - [ - "null", - { - "#bigint": "60" - } - ], - [ - "proposal", - { - "#bigint": "30" - } - ] - ] - }, - "votesAddresses": { - "#set": [ - "alice", - "bob" - ] - } - }, - "round": { - "#bigint": "1" - }, - "votesAddressesWeights": { - "#map": [ - [ - "alice", - { - "#bigint": "60" - } - ], - [ - "bob", - { - "#bigint": "30" - } - ], - [ - "john", - { - "#bigint": "10" - } - ] - ] - } - } - ] - ] - }, - "totalWeight": { - "#bigint": "100" - } - }, - "lastEmitted": { - "name": "None", - "round": { - "#bigint": "1" - }, - "value": "null" - } - }, - { - "#meta": { - "index": 13 - }, - "bookkeeper": { - "height": { - "#bigint": "10" - }, - "rounds": { - "#map": [ - [ - { - "#bigint": "1" - }, - { - "emittedEvents": { - "#set": [ - { - "name": "PolkaAny", - "round": { - "#bigint": "1" - }, - "value": "null" - }, - { - "name": "PrecommitAny", - "round": { - "#bigint": "1" - }, - "value": "null" - }, - { - "name": "PrecommitValue", - "round": { - "#bigint": "1" - }, - "value": "null" - } - ] - }, - "height": { - "#bigint": "10" - }, - "precommits": { - "totalWeight": { - "#bigint": "100" - }, - "valuesWeights": { - "#map": [ - [ - "null", - { - "#bigint": "90" - } - ], - [ - "proposal", - { - "#bigint": "10" - } - ] - ] - }, - "votesAddresses": { - "#set": [ - "alice", - "bob", - "john" - ] - } - }, - "prevotes": { - "totalWeight": { - "#bigint": "100" - }, - "valuesWeights": { - "#map": [ - [ - "null", - { - "#bigint": "60" - } - ], - [ - "proposal", - { - "#bigint": "30" - } - ] - ] - }, - "votesAddresses": { - "#set": [ - "alice", - "bob" - ] - } - }, - "round": { - "#bigint": "1" - }, - "votesAddressesWeights": { - "#map": [ - [ - "alice", - { - "#bigint": "60" - } - ], - [ - "bob", - { - "#bigint": "30" - } - ], - [ - "john", - { - "#bigint": "10" - } - ] - ] - } - } - ] - ] - }, - "totalWeight": { - "#bigint": "100" - } - }, - "lastEmitted": { - "name": "None", - "round": { - "#bigint": "1" - }, - "value": "null" - } - }, - { - "#meta": { - "index": 14 - }, - "bookkeeper": { - "height": { - "#bigint": "10" - }, - "rounds": { - "#map": [ - [ - { - "#bigint": "1" - }, - { - "emittedEvents": { - "#set": [ - { - "name": "PolkaAny", - "round": { - "#bigint": "1" - }, - "value": "null" - }, - { - "name": "PrecommitAny", - "round": { - "#bigint": "1" - }, - "value": "null" - }, - { - "name": "PrecommitValue", - "round": { - "#bigint": "1" - }, - "value": "null" - } - ] - }, - "height": { - "#bigint": "10" - }, - "precommits": { - "totalWeight": { - "#bigint": "100" - }, - "valuesWeights": { - "#map": [ - [ - "null", - { - "#bigint": "90" - } - ], - [ - "proposal", - { - "#bigint": "10" - } - ] - ] - }, - "votesAddresses": { - "#set": [ - "alice", - "bob", - "john" - ] - } - }, - "prevotes": { - "totalWeight": { - "#bigint": "100" - }, - "valuesWeights": { - "#map": [ - [ - "null", - { - "#bigint": "60" - } - ], - [ - "proposal", - { - "#bigint": "30" - } - ] - ] - }, - "votesAddresses": { - "#set": [ - "alice", - "bob" - ] - } - }, - "round": { - "#bigint": "1" - }, - "votesAddressesWeights": { - "#map": [ - [ - "alice", - { - "#bigint": "60" - } - ], - [ - "bob", - { - "#bigint": "30" - } - ], - [ - "john", - { - "#bigint": "10" - } - ] - ] - } - } - ] - ] - }, - "totalWeight": { - "#bigint": "100" - } - }, - "lastEmitted": { - "name": "None", - "round": { - "#bigint": "1" - }, - "value": "null" - } - }, - { - "#meta": { - "index": 15 - }, - "bookkeeper": { - "height": { - "#bigint": "10" - }, - "rounds": { - "#map": [ - [ - { - "#bigint": "1" - }, - { - "emittedEvents": { - "#set": [ - { - "name": "PolkaAny", - "round": { - "#bigint": "1" - }, - "value": "null" - }, - { - "name": "PolkaValue", - "round": { - "#bigint": "1" - }, - "value": "null" - }, - { - "name": "PrecommitAny", - "round": { - "#bigint": "1" - }, - "value": "null" - }, - { - "name": "PrecommitValue", - "round": { - "#bigint": "1" - }, - "value": "null" - } - ] - }, - "height": { - "#bigint": "10" - }, - "precommits": { - "totalWeight": { - "#bigint": "100" - }, - "valuesWeights": { - "#map": [ - [ - "null", - { - "#bigint": "90" - } - ], - [ - "proposal", - { - "#bigint": "10" - } - ] - ] - }, - "votesAddresses": { - "#set": [ - "alice", - "bob", - "john" - ] - } - }, - "prevotes": { - "totalWeight": { - "#bigint": "100" - }, - "valuesWeights": { - "#map": [ - [ - "null", - { - "#bigint": "70" - } - ], - [ - "proposal", - { - "#bigint": "30" - } - ] - ] - }, - "votesAddresses": { - "#set": [ - "alice", - "bob", - "john" - ] - } - }, - "round": { - "#bigint": "1" - }, - "votesAddressesWeights": { - "#map": [ - [ - "alice", - { - "#bigint": "60" - } - ], - [ - "bob", - { - "#bigint": "30" - } - ], - [ - "john", - { - "#bigint": "10" - } - ] - ] - } - } - ] - ] - }, - "totalWeight": { - "#bigint": "100" - } - }, - "lastEmitted": { - "name": "PolkaValue", - "round": { - "#bigint": "1" - }, - "value": "null" - } - }, - { - "#meta": { - "index": 16 - }, - "bookkeeper": { - "height": { - "#bigint": "10" - }, - "rounds": { - "#map": [ - [ - { - "#bigint": "1" - }, - { - "emittedEvents": { - "#set": [ - { - "name": "PolkaAny", - "round": { - "#bigint": "1" - }, - "value": "null" - }, - { - "name": "PolkaValue", - "round": { - "#bigint": "1" - }, - "value": "null" - }, - { - "name": "PrecommitAny", - "round": { - "#bigint": "1" - }, - "value": "null" - }, - { - "name": "PrecommitValue", - "round": { - "#bigint": "1" - }, - "value": "null" - } - ] - }, - "height": { - "#bigint": "10" - }, - "precommits": { - "totalWeight": { - "#bigint": "100" - }, - "valuesWeights": { - "#map": [ - [ - "null", - { - "#bigint": "90" - } - ], - [ - "proposal", - { - "#bigint": "10" - } - ] - ] - }, - "votesAddresses": { - "#set": [ - "alice", - "bob", - "john" - ] - } - }, - "prevotes": { - "totalWeight": { - "#bigint": "100" - }, - "valuesWeights": { - "#map": [ - [ - "null", - { - "#bigint": "70" - } - ], - [ - "proposal", - { - "#bigint": "30" - } - ] - ] - }, - "votesAddresses": { - "#set": [ - "alice", - "bob", - "john" - ] - } - }, - "round": { - "#bigint": "1" - }, - "votesAddressesWeights": { - "#map": [ - [ - "alice", - { - "#bigint": "60" - } - ], - [ - "bob", - { - "#bigint": "30" - } - ], - [ - "john", - { - "#bigint": "10" - } - ] - ] - } - } - ] - ] - }, - "totalWeight": { - "#bigint": "100" - } - }, - "lastEmitted": { - "name": "None", - "round": { - "#bigint": "1" - }, - "value": "null" - } - }, - { - "#meta": { - "index": 17 - }, - "bookkeeper": { - "height": { - "#bigint": "10" - }, - "rounds": { - "#map": [ - [ - { - "#bigint": "1" - }, - { - "emittedEvents": { - "#set": [ - { - "name": "PolkaAny", - "round": { - "#bigint": "1" - }, - "value": "null" - }, - { - "name": "PolkaValue", - "round": { - "#bigint": "1" - }, - "value": "null" - }, - { - "name": "PrecommitAny", - "round": { - "#bigint": "1" - }, - "value": "null" - }, - { - "name": "PrecommitValue", - "round": { - "#bigint": "1" - }, - "value": "null" - } - ] - }, - "height": { - "#bigint": "10" - }, - "precommits": { - "totalWeight": { - "#bigint": "100" - }, - "valuesWeights": { - "#map": [ - [ - "null", - { - "#bigint": "90" - } - ], - [ - "proposal", - { - "#bigint": "10" - } - ] - ] - }, - "votesAddresses": { - "#set": [ - "alice", - "bob", - "john" - ] - } - }, - "prevotes": { - "totalWeight": { - "#bigint": "100" - }, - "valuesWeights": { - "#map": [ - [ - "null", - { - "#bigint": "70" - } - ], - [ - "proposal", - { - "#bigint": "30" - } - ] - ] - }, - "votesAddresses": { - "#set": [ - "alice", - "bob", - "john" - ] - } - }, - "round": { - "#bigint": "1" - }, - "votesAddressesWeights": { - "#map": [ - [ - "alice", - { - "#bigint": "60" - } - ], - [ - "bob", - { - "#bigint": "30" - } - ], - [ - "john", - { - "#bigint": "10" - } - ] - ] - } - } - ] - ] - }, - "totalWeight": { - "#bigint": "100" - } - }, - "lastEmitted": { - "name": "None", - "round": { - "#bigint": "1" - }, - "value": "null" - } - }, - { - "#meta": { - "index": 18 - }, - "bookkeeper": { - "height": { - "#bigint": "10" - }, - "rounds": { - "#map": [ - [ - { - "#bigint": "1" - }, - { - "emittedEvents": { - "#set": [ - { - "name": "PolkaAny", - "round": { - "#bigint": "1" - }, - "value": "null" - }, - { - "name": "PolkaValue", - "round": { - "#bigint": "1" - }, - "value": "null" - }, - { - "name": "PrecommitAny", - "round": { - "#bigint": "1" - }, - "value": "null" - }, - { - "name": "PrecommitValue", - "round": { - "#bigint": "1" - }, - "value": "null" - } - ] - }, - "height": { - "#bigint": "10" - }, - "precommits": { - "totalWeight": { - "#bigint": "100" - }, - "valuesWeights": { - "#map": [ - [ - "null", - { - "#bigint": "90" - } - ], - [ - "proposal", - { - "#bigint": "10" - } - ] - ] - }, - "votesAddresses": { - "#set": [ - "alice", - "bob", - "john" - ] - } - }, - "prevotes": { - "totalWeight": { - "#bigint": "100" - }, - "valuesWeights": { - "#map": [ - [ - "null", - { - "#bigint": "70" - } - ], - [ - "proposal", - { - "#bigint": "30" - } - ] - ] - }, - "votesAddresses": { - "#set": [ - "alice", - "bob", - "john" - ] - } - }, - "round": { - "#bigint": "1" - }, - "votesAddressesWeights": { - "#map": [ - [ - "alice", - { - "#bigint": "60" - } - ], - [ - "bob", - { - "#bigint": "30" - } - ], - [ - "john", - { - "#bigint": "10" - } - ] - ] - } - } - ] - ] - }, - "totalWeight": { - "#bigint": "100" - } - }, - "lastEmitted": { - "name": "None", - "round": { - "#bigint": "1" - }, - "value": "null" - } - }, - { - "#meta": { - "index": 19 - }, - "bookkeeper": { - "height": { - "#bigint": "10" - }, - "rounds": { - "#map": [ - [ - { - "#bigint": "1" - }, - { - "emittedEvents": { - "#set": [ - { - "name": "PolkaAny", - "round": { - "#bigint": "1" - }, - "value": "null" - }, - { - "name": "PolkaValue", - "round": { - "#bigint": "1" - }, - "value": "null" - }, - { - "name": "PrecommitAny", - "round": { - "#bigint": "1" - }, - "value": "null" - }, - { - "name": "PrecommitValue", - "round": { - "#bigint": "1" - }, - "value": "null" - } - ] - }, - "height": { - "#bigint": "10" - }, - "precommits": { - "totalWeight": { - "#bigint": "100" - }, - "valuesWeights": { - "#map": [ - [ - "null", - { - "#bigint": "90" - } - ], - [ - "proposal", - { - "#bigint": "10" - } - ] - ] - }, - "votesAddresses": { - "#set": [ - "alice", - "bob", - "john" - ] - } - }, - "prevotes": { - "totalWeight": { - "#bigint": "100" - }, - "valuesWeights": { - "#map": [ - [ - "null", - { - "#bigint": "70" - } - ], - [ - "proposal", - { - "#bigint": "30" - } - ] - ] - }, - "votesAddresses": { - "#set": [ - "alice", - "bob", - "john" - ] - } - }, - "round": { - "#bigint": "1" - }, - "votesAddressesWeights": { - "#map": [ - [ - "alice", - { - "#bigint": "60" - } - ], - [ - "bob", - { - "#bigint": "30" - } - ], - [ - "john", - { - "#bigint": "10" - } - ] - ] - } - } - ] - ] - }, - "totalWeight": { - "#bigint": "100" - } - }, - "lastEmitted": { - "name": "None", - "round": { - "#bigint": "1" - }, - "value": "null" - } - }, - { - "#meta": { - "index": 20 - }, - "bookkeeper": { - "height": { - "#bigint": "10" - }, - "rounds": { - "#map": [ - [ - { - "#bigint": "1" - }, - { - "emittedEvents": { - "#set": [ - { - "name": "PolkaAny", - "round": { - "#bigint": "1" - }, - "value": "null" - }, - { - "name": "PolkaValue", - "round": { - "#bigint": "1" - }, - "value": "null" - }, - { - "name": "PrecommitAny", - "round": { - "#bigint": "1" - }, - "value": "null" - }, - { - "name": "PrecommitValue", - "round": { - "#bigint": "1" - }, - "value": "null" - } - ] - }, - "height": { - "#bigint": "10" - }, - "precommits": { - "totalWeight": { - "#bigint": "100" - }, - "valuesWeights": { - "#map": [ - [ - "null", - { - "#bigint": "90" - } - ], - [ - "proposal", - { - "#bigint": "10" - } - ] - ] - }, - "votesAddresses": { - "#set": [ - "alice", - "bob", - "john" - ] - } - }, - "prevotes": { - "totalWeight": { - "#bigint": "100" - }, - "valuesWeights": { - "#map": [ - [ - "null", - { - "#bigint": "70" - } - ], - [ - "proposal", - { - "#bigint": "30" - } - ] - ] - }, - "votesAddresses": { - "#set": [ - "alice", - "bob", - "john" - ] - } - }, - "round": { - "#bigint": "1" - }, - "votesAddressesWeights": { - "#map": [ - [ - "alice", - { - "#bigint": "60" - } - ], - [ - "bob", - { - "#bigint": "30" - } - ], - [ - "john", - { - "#bigint": "10" - } - ] - ] - } - } - ] - ] - }, - "totalWeight": { - "#bigint": "100" - } - }, - "lastEmitted": { - "name": "None", - "round": { - "#bigint": "1" - }, - "value": "null" - } - } - ] -} diff --git a/Code/itf/tests/fixtures/votekeeper/voteBookkeeper_polkaAnyTest_6.itf.json b/Code/itf/tests/fixtures/votekeeper/voteBookkeeper_polkaAnyTest_6.itf.json new file mode 100644 index 000000000..e766285a1 --- /dev/null +++ b/Code/itf/tests/fixtures/votekeeper/voteBookkeeper_polkaAnyTest_6.itf.json @@ -0,0 +1 @@ +{"#meta":{"format":"ITF","format-description":"https://apalache.informal.systems/docs/adr/015adr-trace.html","source":"voteBookkeeper.qnt","status":"passed","description":"Created by Quint on Fri Nov 10 2023 14:26:21 GMT+0100 (GMT+01:00)","timestamp":1699622781761},"vars":["lastEmitted","bookkeeper"],"states":[{"#meta":{"index":0},"bookkeeper":{"height":{"#bigint":"10"},"rounds":{"#map":[]},"totalWeight":{"#bigint":"100"}},"lastEmitted":{"name":"","round":{"#bigint":"-1"},"value":"null"}},{"#meta":{"index":1},"bookkeeper":{"height":{"#bigint":"10"},"rounds":{"#map":[[{"#bigint":"1"},{"emittedEvents":{"#set":[]},"height":{"#bigint":"10"},"precommits":{"totalWeight":{"#bigint":"100"},"valuesWeights":{"#map":[]},"votesAddresses":{"#set":[]}},"prevotes":{"totalWeight":{"#bigint":"100"},"valuesWeights":{"#map":[["proposal",{"#bigint":"60"}]]},"votesAddresses":{"#set":["alice"]}},"round":{"#bigint":"1"},"votesAddressesWeights":{"#map":[["alice",{"#bigint":"60"}]]}}]]},"totalWeight":{"#bigint":"100"}},"lastEmitted":{"name":"None","round":{"#bigint":"1"},"value":"null"}},{"#meta":{"index":2},"bookkeeper":{"height":{"#bigint":"10"},"rounds":{"#map":[[{"#bigint":"1"},{"emittedEvents":{"#set":[]},"height":{"#bigint":"10"},"precommits":{"totalWeight":{"#bigint":"100"},"valuesWeights":{"#map":[]},"votesAddresses":{"#set":[]}},"prevotes":{"totalWeight":{"#bigint":"100"},"valuesWeights":{"#map":[["proposal",{"#bigint":"60"}]]},"votesAddresses":{"#set":["alice"]}},"round":{"#bigint":"1"},"votesAddressesWeights":{"#map":[["alice",{"#bigint":"60"}]]}}]]},"totalWeight":{"#bigint":"100"}},"lastEmitted":{"name":"None","round":{"#bigint":"1"},"value":"null"}},{"#meta":{"index":3},"bookkeeper":{"height":{"#bigint":"10"},"rounds":{"#map":[[{"#bigint":"1"},{"emittedEvents":{"#set":[{"name":"PolkaValue","round":{"#bigint":"1"},"value":"proposal"}]},"height":{"#bigint":"10"},"precommits":{"totalWeight":{"#bigint":"100"},"valuesWeights":{"#map":[]},"votesAddresses":{"#set":[]}},"prevotes":{"totalWeight":{"#bigint":"100"},"valuesWeights":{"#map":[["proposal",{"#bigint":"70"}]]},"votesAddresses":{"#set":["alice","john"]}},"round":{"#bigint":"1"},"votesAddressesWeights":{"#map":[["alice",{"#bigint":"60"}],["john",{"#bigint":"10"}]]}}]]},"totalWeight":{"#bigint":"100"}},"lastEmitted":{"name":"PolkaValue","round":{"#bigint":"1"},"value":"proposal"}},{"#meta":{"index":4},"bookkeeper":{"height":{"#bigint":"10"},"rounds":{"#map":[[{"#bigint":"1"},{"emittedEvents":{"#set":[{"name":"PolkaValue","round":{"#bigint":"1"},"value":"proposal"}]},"height":{"#bigint":"10"},"precommits":{"totalWeight":{"#bigint":"100"},"valuesWeights":{"#map":[]},"votesAddresses":{"#set":[]}},"prevotes":{"totalWeight":{"#bigint":"100"},"valuesWeights":{"#map":[["proposal",{"#bigint":"70"}]]},"votesAddresses":{"#set":["alice","john"]}},"round":{"#bigint":"1"},"votesAddressesWeights":{"#map":[["alice",{"#bigint":"60"}],["john",{"#bigint":"10"}]]}}]]},"totalWeight":{"#bigint":"100"}},"lastEmitted":{"name":"PolkaValue","round":{"#bigint":"1"},"value":"proposal"}},{"#meta":{"index":5},"bookkeeper":{"height":{"#bigint":"10"},"rounds":{"#map":[[{"#bigint":"1"},{"emittedEvents":{"#set":[{"name":"PolkaValue","round":{"#bigint":"1"},"value":"proposal"}]},"height":{"#bigint":"10"},"precommits":{"totalWeight":{"#bigint":"100"},"valuesWeights":{"#map":[]},"votesAddresses":{"#set":[]}},"prevotes":{"totalWeight":{"#bigint":"100"},"valuesWeights":{"#map":[["proposal",{"#bigint":"100"}]]},"votesAddresses":{"#set":["alice","bob","john"]}},"round":{"#bigint":"1"},"votesAddressesWeights":{"#map":[["alice",{"#bigint":"60"}],["bob",{"#bigint":"30"}],["john",{"#bigint":"10"}]]}}]]},"totalWeight":{"#bigint":"100"}},"lastEmitted":{"name":"None","round":{"#bigint":"1"},"value":"null"}},{"#meta":{"index":6},"bookkeeper":{"height":{"#bigint":"10"},"rounds":{"#map":[[{"#bigint":"1"},{"emittedEvents":{"#set":[{"name":"PolkaValue","round":{"#bigint":"1"},"value":"proposal"}]},"height":{"#bigint":"10"},"precommits":{"totalWeight":{"#bigint":"100"},"valuesWeights":{"#map":[]},"votesAddresses":{"#set":[]}},"prevotes":{"totalWeight":{"#bigint":"100"},"valuesWeights":{"#map":[["proposal",{"#bigint":"100"}]]},"votesAddresses":{"#set":["alice","bob","john"]}},"round":{"#bigint":"1"},"votesAddressesWeights":{"#map":[["alice",{"#bigint":"60"}],["bob",{"#bigint":"30"}],["john",{"#bigint":"10"}]]}}]]},"totalWeight":{"#bigint":"100"}},"lastEmitted":{"name":"None","round":{"#bigint":"1"},"value":"null"}},{"#meta":{"index":7},"bookkeeper":{"height":{"#bigint":"10"},"rounds":{"#map":[[{"#bigint":"1"},{"emittedEvents":{"#set":[{"name":"PolkaValue","round":{"#bigint":"1"},"value":"proposal"}]},"height":{"#bigint":"10"},"precommits":{"totalWeight":{"#bigint":"100"},"valuesWeights":{"#map":[["proposal",{"#bigint":"30"}]]},"votesAddresses":{"#set":["bob"]}},"prevotes":{"totalWeight":{"#bigint":"100"},"valuesWeights":{"#map":[["proposal",{"#bigint":"100"}]]},"votesAddresses":{"#set":["alice","bob","john"]}},"round":{"#bigint":"1"},"votesAddressesWeights":{"#map":[["alice",{"#bigint":"60"}],["bob",{"#bigint":"30"}],["john",{"#bigint":"10"}]]}}]]},"totalWeight":{"#bigint":"100"}},"lastEmitted":{"name":"None","round":{"#bigint":"1"},"value":"null"}},{"#meta":{"index":8},"bookkeeper":{"height":{"#bigint":"10"},"rounds":{"#map":[[{"#bigint":"1"},{"emittedEvents":{"#set":[{"name":"PolkaValue","round":{"#bigint":"1"},"value":"proposal"}]},"height":{"#bigint":"10"},"precommits":{"totalWeight":{"#bigint":"100"},"valuesWeights":{"#map":[["proposal",{"#bigint":"30"}]]},"votesAddresses":{"#set":["bob"]}},"prevotes":{"totalWeight":{"#bigint":"100"},"valuesWeights":{"#map":[["proposal",{"#bigint":"100"}]]},"votesAddresses":{"#set":["alice","bob","john"]}},"round":{"#bigint":"1"},"votesAddressesWeights":{"#map":[["alice",{"#bigint":"60"}],["bob",{"#bigint":"30"}],["john",{"#bigint":"10"}]]}}]]},"totalWeight":{"#bigint":"100"}},"lastEmitted":{"name":"None","round":{"#bigint":"1"},"value":"null"}},{"#meta":{"index":9},"bookkeeper":{"height":{"#bigint":"10"},"rounds":{"#map":[[{"#bigint":"1"},{"emittedEvents":{"#set":[{"name":"PolkaValue","round":{"#bigint":"1"},"value":"proposal"}]},"height":{"#bigint":"10"},"precommits":{"totalWeight":{"#bigint":"100"},"valuesWeights":{"#map":[["proposal",{"#bigint":"40"}]]},"votesAddresses":{"#set":["bob","john"]}},"prevotes":{"totalWeight":{"#bigint":"100"},"valuesWeights":{"#map":[["proposal",{"#bigint":"100"}]]},"votesAddresses":{"#set":["alice","bob","john"]}},"round":{"#bigint":"1"},"votesAddressesWeights":{"#map":[["alice",{"#bigint":"60"}],["bob",{"#bigint":"30"}],["john",{"#bigint":"10"}]]}}]]},"totalWeight":{"#bigint":"100"}},"lastEmitted":{"name":"None","round":{"#bigint":"1"},"value":"null"}},{"#meta":{"index":10},"bookkeeper":{"height":{"#bigint":"10"},"rounds":{"#map":[[{"#bigint":"1"},{"emittedEvents":{"#set":[{"name":"PolkaValue","round":{"#bigint":"1"},"value":"proposal"}]},"height":{"#bigint":"10"},"precommits":{"totalWeight":{"#bigint":"100"},"valuesWeights":{"#map":[["proposal",{"#bigint":"40"}]]},"votesAddresses":{"#set":["bob","john"]}},"prevotes":{"totalWeight":{"#bigint":"100"},"valuesWeights":{"#map":[["proposal",{"#bigint":"100"}]]},"votesAddresses":{"#set":["alice","bob","john"]}},"round":{"#bigint":"1"},"votesAddressesWeights":{"#map":[["alice",{"#bigint":"60"}],["bob",{"#bigint":"30"}],["john",{"#bigint":"10"}]]}}]]},"totalWeight":{"#bigint":"100"}},"lastEmitted":{"name":"None","round":{"#bigint":"1"},"value":"null"}},{"#meta":{"index":11},"bookkeeper":{"height":{"#bigint":"10"},"rounds":{"#map":[[{"#bigint":"1"},{"emittedEvents":{"#set":[{"name":"PolkaValue","round":{"#bigint":"1"},"value":"proposal"},{"name":"PrecommitValue","round":{"#bigint":"1"},"value":"proposal"}]},"height":{"#bigint":"10"},"precommits":{"totalWeight":{"#bigint":"100"},"valuesWeights":{"#map":[["proposal",{"#bigint":"100"}]]},"votesAddresses":{"#set":["alive","bob","john"]}},"prevotes":{"totalWeight":{"#bigint":"100"},"valuesWeights":{"#map":[["proposal",{"#bigint":"100"}]]},"votesAddresses":{"#set":["alice","bob","john"]}},"round":{"#bigint":"1"},"votesAddressesWeights":{"#map":[["alice",{"#bigint":"60"}],["alive",{"#bigint":"60"}],["bob",{"#bigint":"30"}],["john",{"#bigint":"10"}]]}}]]},"totalWeight":{"#bigint":"100"}},"lastEmitted":{"name":"PrecommitValue","round":{"#bigint":"1"},"value":"proposal"}}]} \ No newline at end of file diff --git a/Code/itf/tests/fixtures/votekeeper/voteBookkeeper_polkaNilTest_7.itf.json b/Code/itf/tests/fixtures/votekeeper/voteBookkeeper_polkaNilTest_7.itf.json new file mode 100644 index 000000000..b5bf98cda --- /dev/null +++ b/Code/itf/tests/fixtures/votekeeper/voteBookkeeper_polkaNilTest_7.itf.json @@ -0,0 +1 @@ +{"#meta":{"format":"ITF","format-description":"https://apalache.informal.systems/docs/adr/015adr-trace.html","source":"voteBookkeeper.qnt","status":"passed","description":"Created by Quint on Fri Nov 10 2023 14:26:21 GMT+0100 (GMT+01:00)","timestamp":1699622781765},"vars":["lastEmitted","bookkeeper"],"states":[{"#meta":{"index":0},"bookkeeper":{"height":{"#bigint":"10"},"rounds":{"#map":[]},"totalWeight":{"#bigint":"100"}},"lastEmitted":{"name":"","round":{"#bigint":"-1"},"value":"null"}},{"#meta":{"index":1},"bookkeeper":{"height":{"#bigint":"10"},"rounds":{"#map":[[{"#bigint":"1"},{"emittedEvents":{"#set":[]},"height":{"#bigint":"10"},"precommits":{"totalWeight":{"#bigint":"100"},"valuesWeights":{"#map":[]},"votesAddresses":{"#set":[]}},"prevotes":{"totalWeight":{"#bigint":"100"},"valuesWeights":{"#map":[["proposal",{"#bigint":"60"}]]},"votesAddresses":{"#set":["alice"]}},"round":{"#bigint":"1"},"votesAddressesWeights":{"#map":[["alice",{"#bigint":"60"}]]}}]]},"totalWeight":{"#bigint":"100"}},"lastEmitted":{"name":"None","round":{"#bigint":"1"},"value":"null"}},{"#meta":{"index":2},"bookkeeper":{"height":{"#bigint":"10"},"rounds":{"#map":[[{"#bigint":"1"},{"emittedEvents":{"#set":[]},"height":{"#bigint":"10"},"precommits":{"totalWeight":{"#bigint":"100"},"valuesWeights":{"#map":[]},"votesAddresses":{"#set":[]}},"prevotes":{"totalWeight":{"#bigint":"100"},"valuesWeights":{"#map":[["proposal",{"#bigint":"60"}]]},"votesAddresses":{"#set":["alice"]}},"round":{"#bigint":"1"},"votesAddressesWeights":{"#map":[["alice",{"#bigint":"60"}]]}}]]},"totalWeight":{"#bigint":"100"}},"lastEmitted":{"name":"None","round":{"#bigint":"1"},"value":"null"}},{"#meta":{"index":3},"bookkeeper":{"height":{"#bigint":"10"},"rounds":{"#map":[[{"#bigint":"1"},{"emittedEvents":{"#set":[{"name":"PolkaValue","round":{"#bigint":"1"},"value":"proposal"}]},"height":{"#bigint":"10"},"precommits":{"totalWeight":{"#bigint":"100"},"valuesWeights":{"#map":[]},"votesAddresses":{"#set":[]}},"prevotes":{"totalWeight":{"#bigint":"100"},"valuesWeights":{"#map":[["proposal",{"#bigint":"70"}]]},"votesAddresses":{"#set":["alice","john"]}},"round":{"#bigint":"1"},"votesAddressesWeights":{"#map":[["alice",{"#bigint":"60"}],["john",{"#bigint":"10"}]]}}]]},"totalWeight":{"#bigint":"100"}},"lastEmitted":{"name":"PolkaValue","round":{"#bigint":"1"},"value":"proposal"}},{"#meta":{"index":4},"bookkeeper":{"height":{"#bigint":"10"},"rounds":{"#map":[[{"#bigint":"1"},{"emittedEvents":{"#set":[{"name":"PolkaValue","round":{"#bigint":"1"},"value":"proposal"}]},"height":{"#bigint":"10"},"precommits":{"totalWeight":{"#bigint":"100"},"valuesWeights":{"#map":[]},"votesAddresses":{"#set":[]}},"prevotes":{"totalWeight":{"#bigint":"100"},"valuesWeights":{"#map":[["proposal",{"#bigint":"70"}]]},"votesAddresses":{"#set":["alice","john"]}},"round":{"#bigint":"1"},"votesAddressesWeights":{"#map":[["alice",{"#bigint":"60"}],["john",{"#bigint":"10"}]]}}]]},"totalWeight":{"#bigint":"100"}},"lastEmitted":{"name":"PolkaValue","round":{"#bigint":"1"},"value":"proposal"}},{"#meta":{"index":5},"bookkeeper":{"height":{"#bigint":"10"},"rounds":{"#map":[[{"#bigint":"1"},{"emittedEvents":{"#set":[{"name":"PolkaValue","round":{"#bigint":"1"},"value":"proposal"}]},"height":{"#bigint":"10"},"precommits":{"totalWeight":{"#bigint":"100"},"valuesWeights":{"#map":[]},"votesAddresses":{"#set":[]}},"prevotes":{"totalWeight":{"#bigint":"100"},"valuesWeights":{"#map":[["proposal",{"#bigint":"100"}]]},"votesAddresses":{"#set":["alice","bob","john"]}},"round":{"#bigint":"1"},"votesAddressesWeights":{"#map":[["alice",{"#bigint":"60"}],["bob",{"#bigint":"30"}],["john",{"#bigint":"10"}]]}}]]},"totalWeight":{"#bigint":"100"}},"lastEmitted":{"name":"None","round":{"#bigint":"1"},"value":"null"}},{"#meta":{"index":6},"bookkeeper":{"height":{"#bigint":"10"},"rounds":{"#map":[[{"#bigint":"1"},{"emittedEvents":{"#set":[{"name":"PolkaValue","round":{"#bigint":"1"},"value":"proposal"}]},"height":{"#bigint":"10"},"precommits":{"totalWeight":{"#bigint":"100"},"valuesWeights":{"#map":[]},"votesAddresses":{"#set":[]}},"prevotes":{"totalWeight":{"#bigint":"100"},"valuesWeights":{"#map":[["proposal",{"#bigint":"100"}]]},"votesAddresses":{"#set":["alice","bob","john"]}},"round":{"#bigint":"1"},"votesAddressesWeights":{"#map":[["alice",{"#bigint":"60"}],["bob",{"#bigint":"30"}],["john",{"#bigint":"10"}]]}}]]},"totalWeight":{"#bigint":"100"}},"lastEmitted":{"name":"None","round":{"#bigint":"1"},"value":"null"}},{"#meta":{"index":7},"bookkeeper":{"height":{"#bigint":"10"},"rounds":{"#map":[[{"#bigint":"1"},{"emittedEvents":{"#set":[{"name":"PolkaValue","round":{"#bigint":"1"},"value":"proposal"}]},"height":{"#bigint":"10"},"precommits":{"totalWeight":{"#bigint":"100"},"valuesWeights":{"#map":[["proposal",{"#bigint":"30"}]]},"votesAddresses":{"#set":["bob"]}},"prevotes":{"totalWeight":{"#bigint":"100"},"valuesWeights":{"#map":[["proposal",{"#bigint":"100"}]]},"votesAddresses":{"#set":["alice","bob","john"]}},"round":{"#bigint":"1"},"votesAddressesWeights":{"#map":[["alice",{"#bigint":"60"}],["bob",{"#bigint":"30"}],["john",{"#bigint":"10"}]]}}]]},"totalWeight":{"#bigint":"100"}},"lastEmitted":{"name":"None","round":{"#bigint":"1"},"value":"null"}},{"#meta":{"index":8},"bookkeeper":{"height":{"#bigint":"10"},"rounds":{"#map":[[{"#bigint":"1"},{"emittedEvents":{"#set":[{"name":"PolkaValue","round":{"#bigint":"1"},"value":"proposal"}]},"height":{"#bigint":"10"},"precommits":{"totalWeight":{"#bigint":"100"},"valuesWeights":{"#map":[["proposal",{"#bigint":"30"}]]},"votesAddresses":{"#set":["bob"]}},"prevotes":{"totalWeight":{"#bigint":"100"},"valuesWeights":{"#map":[["proposal",{"#bigint":"100"}]]},"votesAddresses":{"#set":["alice","bob","john"]}},"round":{"#bigint":"1"},"votesAddressesWeights":{"#map":[["alice",{"#bigint":"60"}],["bob",{"#bigint":"30"}],["john",{"#bigint":"10"}]]}}]]},"totalWeight":{"#bigint":"100"}},"lastEmitted":{"name":"None","round":{"#bigint":"1"},"value":"null"}},{"#meta":{"index":9},"bookkeeper":{"height":{"#bigint":"10"},"rounds":{"#map":[[{"#bigint":"1"},{"emittedEvents":{"#set":[{"name":"PolkaValue","round":{"#bigint":"1"},"value":"proposal"}]},"height":{"#bigint":"10"},"precommits":{"totalWeight":{"#bigint":"100"},"valuesWeights":{"#map":[["proposal",{"#bigint":"40"}]]},"votesAddresses":{"#set":["bob","john"]}},"prevotes":{"totalWeight":{"#bigint":"100"},"valuesWeights":{"#map":[["proposal",{"#bigint":"100"}]]},"votesAddresses":{"#set":["alice","bob","john"]}},"round":{"#bigint":"1"},"votesAddressesWeights":{"#map":[["alice",{"#bigint":"60"}],["bob",{"#bigint":"30"}],["john",{"#bigint":"10"}]]}}]]},"totalWeight":{"#bigint":"100"}},"lastEmitted":{"name":"None","round":{"#bigint":"1"},"value":"null"}},{"#meta":{"index":10},"bookkeeper":{"height":{"#bigint":"10"},"rounds":{"#map":[[{"#bigint":"1"},{"emittedEvents":{"#set":[{"name":"PolkaValue","round":{"#bigint":"1"},"value":"proposal"}]},"height":{"#bigint":"10"},"precommits":{"totalWeight":{"#bigint":"100"},"valuesWeights":{"#map":[["proposal",{"#bigint":"40"}]]},"votesAddresses":{"#set":["bob","john"]}},"prevotes":{"totalWeight":{"#bigint":"100"},"valuesWeights":{"#map":[["proposal",{"#bigint":"100"}]]},"votesAddresses":{"#set":["alice","bob","john"]}},"round":{"#bigint":"1"},"votesAddressesWeights":{"#map":[["alice",{"#bigint":"60"}],["bob",{"#bigint":"30"}],["john",{"#bigint":"10"}]]}}]]},"totalWeight":{"#bigint":"100"}},"lastEmitted":{"name":"None","round":{"#bigint":"1"},"value":"null"}},{"#meta":{"index":11},"bookkeeper":{"height":{"#bigint":"10"},"rounds":{"#map":[[{"#bigint":"1"},{"emittedEvents":{"#set":[{"name":"PolkaValue","round":{"#bigint":"1"},"value":"proposal"},{"name":"PrecommitValue","round":{"#bigint":"1"},"value":"proposal"}]},"height":{"#bigint":"10"},"precommits":{"totalWeight":{"#bigint":"100"},"valuesWeights":{"#map":[["proposal",{"#bigint":"100"}]]},"votesAddresses":{"#set":["alive","bob","john"]}},"prevotes":{"totalWeight":{"#bigint":"100"},"valuesWeights":{"#map":[["proposal",{"#bigint":"100"}]]},"votesAddresses":{"#set":["alice","bob","john"]}},"round":{"#bigint":"1"},"votesAddressesWeights":{"#map":[["alice",{"#bigint":"60"}],["alive",{"#bigint":"60"}],["bob",{"#bigint":"30"}],["john",{"#bigint":"10"}]]}}]]},"totalWeight":{"#bigint":"100"}},"lastEmitted":{"name":"PrecommitValue","round":{"#bigint":"1"},"value":"proposal"}}]} \ No newline at end of file diff --git a/Code/itf/tests/fixtures/votekeeper/voteBookkeeper_synchronousConsensusTest_5.itf.json b/Code/itf/tests/fixtures/votekeeper/voteBookkeeper_synchronousConsensusTest_5.itf.json new file mode 100644 index 000000000..75bc07e59 --- /dev/null +++ b/Code/itf/tests/fixtures/votekeeper/voteBookkeeper_synchronousConsensusTest_5.itf.json @@ -0,0 +1 @@ +{"#meta":{"format":"ITF","format-description":"https://apalache.informal.systems/docs/adr/015adr-trace.html","source":"voteBookkeeper.qnt","status":"passed","description":"Created by Quint on Fri Nov 10 2023 14:26:21 GMT+0100 (GMT+01:00)","timestamp":1699622781758},"vars":["lastEmitted","bookkeeper"],"states":[{"#meta":{"index":0},"bookkeeper":{"height":{"#bigint":"10"},"rounds":{"#map":[]},"totalWeight":{"#bigint":"100"}},"lastEmitted":{"name":"","round":{"#bigint":"-1"},"value":"null"}},{"#meta":{"index":1},"bookkeeper":{"height":{"#bigint":"10"},"rounds":{"#map":[[{"#bigint":"1"},{"emittedEvents":{"#set":[]},"height":{"#bigint":"10"},"precommits":{"totalWeight":{"#bigint":"100"},"valuesWeights":{"#map":[]},"votesAddresses":{"#set":[]}},"prevotes":{"totalWeight":{"#bigint":"100"},"valuesWeights":{"#map":[["proposal",{"#bigint":"60"}]]},"votesAddresses":{"#set":["alice"]}},"round":{"#bigint":"1"},"votesAddressesWeights":{"#map":[["alice",{"#bigint":"60"}]]}}]]},"totalWeight":{"#bigint":"100"}},"lastEmitted":{"name":"None","round":{"#bigint":"1"},"value":"null"}},{"#meta":{"index":2},"bookkeeper":{"height":{"#bigint":"10"},"rounds":{"#map":[[{"#bigint":"1"},{"emittedEvents":{"#set":[]},"height":{"#bigint":"10"},"precommits":{"totalWeight":{"#bigint":"100"},"valuesWeights":{"#map":[]},"votesAddresses":{"#set":[]}},"prevotes":{"totalWeight":{"#bigint":"100"},"valuesWeights":{"#map":[["proposal",{"#bigint":"60"}]]},"votesAddresses":{"#set":["alice"]}},"round":{"#bigint":"1"},"votesAddressesWeights":{"#map":[["alice",{"#bigint":"60"}]]}}]]},"totalWeight":{"#bigint":"100"}},"lastEmitted":{"name":"None","round":{"#bigint":"1"},"value":"null"}},{"#meta":{"index":3},"bookkeeper":{"height":{"#bigint":"10"},"rounds":{"#map":[[{"#bigint":"1"},{"emittedEvents":{"#set":[{"name":"PolkaValue","round":{"#bigint":"1"},"value":"proposal"}]},"height":{"#bigint":"10"},"precommits":{"totalWeight":{"#bigint":"100"},"valuesWeights":{"#map":[]},"votesAddresses":{"#set":[]}},"prevotes":{"totalWeight":{"#bigint":"100"},"valuesWeights":{"#map":[["proposal",{"#bigint":"70"}]]},"votesAddresses":{"#set":["alice","john"]}},"round":{"#bigint":"1"},"votesAddressesWeights":{"#map":[["alice",{"#bigint":"60"}],["john",{"#bigint":"10"}]]}}]]},"totalWeight":{"#bigint":"100"}},"lastEmitted":{"name":"PolkaValue","round":{"#bigint":"1"},"value":"proposal"}},{"#meta":{"index":4},"bookkeeper":{"height":{"#bigint":"10"},"rounds":{"#map":[[{"#bigint":"1"},{"emittedEvents":{"#set":[{"name":"PolkaValue","round":{"#bigint":"1"},"value":"proposal"}]},"height":{"#bigint":"10"},"precommits":{"totalWeight":{"#bigint":"100"},"valuesWeights":{"#map":[]},"votesAddresses":{"#set":[]}},"prevotes":{"totalWeight":{"#bigint":"100"},"valuesWeights":{"#map":[["proposal",{"#bigint":"70"}]]},"votesAddresses":{"#set":["alice","john"]}},"round":{"#bigint":"1"},"votesAddressesWeights":{"#map":[["alice",{"#bigint":"60"}],["john",{"#bigint":"10"}]]}}]]},"totalWeight":{"#bigint":"100"}},"lastEmitted":{"name":"PolkaValue","round":{"#bigint":"1"},"value":"proposal"}},{"#meta":{"index":5},"bookkeeper":{"height":{"#bigint":"10"},"rounds":{"#map":[[{"#bigint":"1"},{"emittedEvents":{"#set":[{"name":"PolkaValue","round":{"#bigint":"1"},"value":"proposal"}]},"height":{"#bigint":"10"},"precommits":{"totalWeight":{"#bigint":"100"},"valuesWeights":{"#map":[]},"votesAddresses":{"#set":[]}},"prevotes":{"totalWeight":{"#bigint":"100"},"valuesWeights":{"#map":[["proposal",{"#bigint":"100"}]]},"votesAddresses":{"#set":["alice","bob","john"]}},"round":{"#bigint":"1"},"votesAddressesWeights":{"#map":[["alice",{"#bigint":"60"}],["bob",{"#bigint":"30"}],["john",{"#bigint":"10"}]]}}]]},"totalWeight":{"#bigint":"100"}},"lastEmitted":{"name":"None","round":{"#bigint":"1"},"value":"null"}},{"#meta":{"index":6},"bookkeeper":{"height":{"#bigint":"10"},"rounds":{"#map":[[{"#bigint":"1"},{"emittedEvents":{"#set":[{"name":"PolkaValue","round":{"#bigint":"1"},"value":"proposal"}]},"height":{"#bigint":"10"},"precommits":{"totalWeight":{"#bigint":"100"},"valuesWeights":{"#map":[]},"votesAddresses":{"#set":[]}},"prevotes":{"totalWeight":{"#bigint":"100"},"valuesWeights":{"#map":[["proposal",{"#bigint":"100"}]]},"votesAddresses":{"#set":["alice","bob","john"]}},"round":{"#bigint":"1"},"votesAddressesWeights":{"#map":[["alice",{"#bigint":"60"}],["bob",{"#bigint":"30"}],["john",{"#bigint":"10"}]]}}]]},"totalWeight":{"#bigint":"100"}},"lastEmitted":{"name":"None","round":{"#bigint":"1"},"value":"null"}},{"#meta":{"index":7},"bookkeeper":{"height":{"#bigint":"10"},"rounds":{"#map":[[{"#bigint":"1"},{"emittedEvents":{"#set":[{"name":"PolkaValue","round":{"#bigint":"1"},"value":"proposal"}]},"height":{"#bigint":"10"},"precommits":{"totalWeight":{"#bigint":"100"},"valuesWeights":{"#map":[["proposal",{"#bigint":"30"}]]},"votesAddresses":{"#set":["bob"]}},"prevotes":{"totalWeight":{"#bigint":"100"},"valuesWeights":{"#map":[["proposal",{"#bigint":"100"}]]},"votesAddresses":{"#set":["alice","bob","john"]}},"round":{"#bigint":"1"},"votesAddressesWeights":{"#map":[["alice",{"#bigint":"60"}],["bob",{"#bigint":"30"}],["john",{"#bigint":"10"}]]}}]]},"totalWeight":{"#bigint":"100"}},"lastEmitted":{"name":"None","round":{"#bigint":"1"},"value":"null"}},{"#meta":{"index":8},"bookkeeper":{"height":{"#bigint":"10"},"rounds":{"#map":[[{"#bigint":"1"},{"emittedEvents":{"#set":[{"name":"PolkaValue","round":{"#bigint":"1"},"value":"proposal"}]},"height":{"#bigint":"10"},"precommits":{"totalWeight":{"#bigint":"100"},"valuesWeights":{"#map":[["proposal",{"#bigint":"30"}]]},"votesAddresses":{"#set":["bob"]}},"prevotes":{"totalWeight":{"#bigint":"100"},"valuesWeights":{"#map":[["proposal",{"#bigint":"100"}]]},"votesAddresses":{"#set":["alice","bob","john"]}},"round":{"#bigint":"1"},"votesAddressesWeights":{"#map":[["alice",{"#bigint":"60"}],["bob",{"#bigint":"30"}],["john",{"#bigint":"10"}]]}}]]},"totalWeight":{"#bigint":"100"}},"lastEmitted":{"name":"None","round":{"#bigint":"1"},"value":"null"}},{"#meta":{"index":9},"bookkeeper":{"height":{"#bigint":"10"},"rounds":{"#map":[[{"#bigint":"1"},{"emittedEvents":{"#set":[{"name":"PolkaValue","round":{"#bigint":"1"},"value":"proposal"}]},"height":{"#bigint":"10"},"precommits":{"totalWeight":{"#bigint":"100"},"valuesWeights":{"#map":[["proposal",{"#bigint":"40"}]]},"votesAddresses":{"#set":["bob","john"]}},"prevotes":{"totalWeight":{"#bigint":"100"},"valuesWeights":{"#map":[["proposal",{"#bigint":"100"}]]},"votesAddresses":{"#set":["alice","bob","john"]}},"round":{"#bigint":"1"},"votesAddressesWeights":{"#map":[["alice",{"#bigint":"60"}],["bob",{"#bigint":"30"}],["john",{"#bigint":"10"}]]}}]]},"totalWeight":{"#bigint":"100"}},"lastEmitted":{"name":"None","round":{"#bigint":"1"},"value":"null"}},{"#meta":{"index":10},"bookkeeper":{"height":{"#bigint":"10"},"rounds":{"#map":[[{"#bigint":"1"},{"emittedEvents":{"#set":[{"name":"PolkaValue","round":{"#bigint":"1"},"value":"proposal"}]},"height":{"#bigint":"10"},"precommits":{"totalWeight":{"#bigint":"100"},"valuesWeights":{"#map":[["proposal",{"#bigint":"40"}]]},"votesAddresses":{"#set":["bob","john"]}},"prevotes":{"totalWeight":{"#bigint":"100"},"valuesWeights":{"#map":[["proposal",{"#bigint":"100"}]]},"votesAddresses":{"#set":["alice","bob","john"]}},"round":{"#bigint":"1"},"votesAddressesWeights":{"#map":[["alice",{"#bigint":"60"}],["bob",{"#bigint":"30"}],["john",{"#bigint":"10"}]]}}]]},"totalWeight":{"#bigint":"100"}},"lastEmitted":{"name":"None","round":{"#bigint":"1"},"value":"null"}},{"#meta":{"index":11},"bookkeeper":{"height":{"#bigint":"10"},"rounds":{"#map":[[{"#bigint":"1"},{"emittedEvents":{"#set":[{"name":"PolkaValue","round":{"#bigint":"1"},"value":"proposal"},{"name":"PrecommitValue","round":{"#bigint":"1"},"value":"proposal"}]},"height":{"#bigint":"10"},"precommits":{"totalWeight":{"#bigint":"100"},"valuesWeights":{"#map":[["proposal",{"#bigint":"100"}]]},"votesAddresses":{"#set":["alive","bob","john"]}},"prevotes":{"totalWeight":{"#bigint":"100"},"valuesWeights":{"#map":[["proposal",{"#bigint":"100"}]]},"votesAddresses":{"#set":["alice","bob","john"]}},"round":{"#bigint":"1"},"votesAddressesWeights":{"#map":[["alice",{"#bigint":"60"}],["alive",{"#bigint":"60"}],["bob",{"#bigint":"30"}],["john",{"#bigint":"10"}]]}}]]},"totalWeight":{"#bigint":"100"}},"lastEmitted":{"name":"PrecommitValue","round":{"#bigint":"1"},"value":"proposal"}}]} \ No newline at end of file diff --git a/Code/itf/tests/votekeeper.rs b/Code/itf/tests/votekeeper.rs index 9624e4556..994becff8 100644 --- a/Code/itf/tests/votekeeper.rs +++ b/Code/itf/tests/votekeeper.rs @@ -1,15 +1,19 @@ use malachite_itf::votekeeper::State; -const FIXTURES: &[&str] = &["votekeeper.itf.json"]; - #[test] fn parse_fixtures() { - for fixture in FIXTURES { - println!("Parsing '{fixture}'"); + // read fixtures files in test/fixtures/votekeeper/ + let folder = format!("{}/tests/fixtures/votekeeper", env!("CARGO_MANIFEST_DIR")); + + let fixtures = std::fs::read_dir(folder) + .unwrap() + .map(|entry| entry.unwrap().path()) + .collect::>(); - let path = format!("{}/tests/fixtures/{}", env!("CARGO_MANIFEST_DIR"), fixture); + for fixture in fixtures { + println!("Parsing '{}'", fixture.display()); - let json = std::fs::read_to_string(&path).unwrap(); + let json = std::fs::read_to_string(&fixture).unwrap(); let trace = itf::trace_from_str::(&json).unwrap(); dbg!(trace);