First quint draft that is somewhat complete with consensus, executor, voteKeeper

.github/workflows/quint.yml

@@ -15,15 +15,22 @@ jobs:
   quint-typecheck:
     name: Typecheck
     runs-on: ubuntu-latest
-    defaults:
-      run:
-        working-directory: ./Specs/Quint
     steps:
       - uses: actions/checkout@v4
       - uses: actions/setup-node@v3
         with:
           node-version: "18"
       - run: npm install -g @informalsystems/quint
-      - run: npx @informalsystems/quint typecheck consensus.qnt
-      - run: npx @informalsystems/quint typecheck voteBookkeeper.qnt
+      - run: bash Scripts/quint-forall.sh typecheck Specs/Quint/*.qnt
+
+  quint-test:
+    name: Test
+    runs-on: ubuntu-latest
+    steps:
+      - uses: actions/checkout@v4
+      - uses: actions/setup-node@v3
+        with:
+          node-version: "18"
+      - run: npm install -g @informalsystems/quint
+      - run: bash Scripts/quint-forall.sh test Specs/Quint/*.qnt
 

Scripts/quint-forall.sh

@@ -0,0 +1,48 @@
+#!/bin/env bash
+
+BLUE=$(tput setaf 4)
+RED=$(tput setaf 1)
+RESET=$(tput sgr0)
+UNDERLINE=$(tput smul)
+
+# [INFO] message in blue
+info()
+{
+  echo "${BLUE}[INFO] $*${RESET}"
+} 
+
+# [ERROR] message in red
+error()
+{
+  echo "${RED}[ERROR] $*${RESET} "
+}
+
+# Run `quint $command` on all given files.
+
+cmd="$1"
+files=("${@:2}")
+
+if [[ "${#files[@]}" -eq 0 ]]; then
+  echo "${UNDERLINE}Usage:${RESET} $0 <command> <file> [<file> ...]"
+  exit 1
+fi
+
+failed=0
+failed_files=()
+
+for file in "${files[@]}"; do
+  info "Running: quint $cmd ${UNDERLINE}$file"
+  if ! npx @informalsystems/quint "$cmd" "$file"; then
+    failed_files+=("$file")
+    failed=$((failed + 1))
+  fi
+  echo ""
+done
+
+if [[ "$failed" -gt 0 ]]; then
+  error "Failed on $failed files:"
+  for file in "${failed_files[@]}"; do
+    error " - ${UNDERLINE}$file"
+  done
+  exit 1
+fi

Specs/Quint/AsyncModels.qnt

@@ -0,0 +1,81 @@
+// -*- mode: Bluespec; -*-
+
+module AsyncModels {
+
+import statemachineAsync(
+    validators = Set("v1", "v2", "v3", "v4"),
+    validatorSet = Set("v1", "v2", "v3", "v4").mapBy(x => 1),
+    Faulty = Set("v1"),
+    Values = Set("a", "b"),
+    Rounds = Set(0, 1, 2, 3),
+    Heights = Set(0) // , 1, 2, 3)
+) as N4F1 from "./statemachineAsync"
+
+// quint run --init=N4F1::init --step=N4F1::step --invariant=N4F1::AgreementInv AsyncModels.qnt
+// quint run --init=N4F1::init --step=N4F1::step --invariant=N4F1::ConsensusOutputInv AsyncModels.qnt
+
+import statemachineAsync(
+    validators = Set("v1", "v2", "v3", "v4"),
+    validatorSet = Set("v1", "v2", "v3", "v4").mapBy(x => 1),
+    Faulty = Set("v1", "v2"),
+    Values = Set("a", "b"),
+    Rounds = Set(0),  // , 1, 2, 3)
+    Heights = Set(0) // , 1, 2, 3)
+) as N4F2 from "./statemachineAsync"
+
+// v3 and v4 are correct. v2 is a N4N4F22aulty proposal and proposes diN4N4F22N4N4F22erently to v3 and v4
+// this run leads to disagreement
+run DisagreementTest = {
+    N4F2::init
+    .then(N4F2::valStep("v3"))
+    .then(N4F2::valStep("v4"))
+    .then(N4F2::deliverProposal("v3", { height: 0, proposal: "b", round: 0, src: "v2", validRound: -1 }))
+    .then(N4F2::deliverProposal("v4", { height: 0, proposal: "a", round: 0, src: "v2", validRound: -1 }))
+    .then(N4F2::valStep("v3"))
+    .then(N4F2::valStep("v4"))
+    .then(all{
+        // they voted diN4F2N4F2erently
+        assert(N4F2::voteBuffer == Map(
+            "v3" -> Set({ height: 0, id: "a", round: 0, src: "v4", step: "Prevote" },  
+                        { height: 0, id: "b", round: 0, src: "v3", step: "Prevote" }),
+            "v4" -> Set({ height: 0, id: "a", round: 0, src: "v4", step: "Prevote" }, 
+                        { height: 0, id: "b", round: 0, src: "v3", step: "Prevote" }))),
+            N4F2::deliverVote("v4", { height: 0, id: "a", round: 0, src: "v1", step: "Prevote" })
+    })
+    .then(N4F2::deliverVote("v4", { height: 0, id: "a", round: 0, src: "v2", step: "Prevote" }))
+    .then(N4F2::deliverVote("v3", { height: 0, id: "b", round: 0, src: "v1", step: "Prevote" }))
+    .then(N4F2::deliverVote("v3", { height: 0, id: "b", round: 0, src: "v2", step: "Prevote" }))
+    .then(N4F2::deliverVote("v3", { height: 0, id: "b", round: 0, src: "v3", step: "Prevote" }))
+    .then(N4F2::deliverVote("v4", { height: 0, id: "a", round: 0, src: "v4", step: "Prevote" }))
+    .then(N4F2::valStep("v3"))  
+    .then(N4F2::valStep("v3"))   
+    .then(N4F2::valStep("v3"))
+    .then(N4F2::valStep("v4"))
+    .then(N4F2::valStep("v4"))
+    .then(N4F2::valStep("v4"))
+    .then(all{
+        // they precommited diN4F2N4F2erently
+        assert( N4F2::voteBuffer.get("v3").contains({ height: 0, id: "a", round: 0, src: "v4", step: "Precommit" }) and
+                N4F2::voteBuffer.get("v4").contains({ height: 0, id: "b", round: 0, src: "v3", step: "Precommit" })), 
+        N4F2::deliverVote("v4", { height: 0, id: "a", round: 0, src: "v1", step: "Precommit" }) })
+    .then(N4F2::deliverVote("v4", { height: 0, id: "a", round: 0, src: "v2", step: "Precommit" }))    
+    .then(N4F2::deliverVote("v3", { height: 0, id: "b", round: 0, src: "v1", step: "Precommit" })) 
+    .then(N4F2::deliverVote("v3", { height: 0, id: "b", round: 0, src: "v2", step: "Precommit" })) 
+    .then(N4F2::valStep("v3"))  
+    .then(N4F2::valStep("v3"))   
+    .then(N4F2::valStep("v4"))
+    .then(N4F2::valStep("v4"))
+    .then(all{
+        assert(N4F2::AgreementInv),
+        N4F2::deliverVote("v4", { height: 0, id: "a", round: 0, src: "v4", step: "Precommit" }) })
+    .then(N4F2::deliverVote("v3", { height: 0, id: "b", round: 0, src: "v3", step: "Precommit" }))
+    .then(N4F2::valStep("v3"))   
+    .then(N4F2::valStep("v4"))
+    .then(all{
+        assert(not(N4F2::AgreementInv)),
+        N4F2::unchangedAll})   
+}
+
+
+
+}