spec: Fix import paths in specs

informalsystems · Jan 9, 2024 · 07c0d7b · 07c0d7b
1 parent 7fa8926
commit 07c0d7b
Show file tree

Hide file tree

Showing 13 changed files with 27 additions and 27 deletions.
diff --git a/Specs/Quint/specs/driver.qnt b/Specs/Quint/specs/driver.qnt
@@ -6,10 +6,10 @@
 */ 
 
 module driver {
-    import extraSpells.* from "./extraSpells"
+    import extraSpells.* from "../spells/extra"
     import types.* from "./types"
     import consensus.* from "./consensus"
-    import voteBookkeeper.* from "./voteBookkeeper"
+    import voteBookkeeper.* from "./votekeeper"
 
     // *************************************************************************
     // State

diff --git a/Specs/Quint/specs/statemachineAsync.qnt b/Specs/Quint/specs/statemachineAsync.qnt
@@ -21,7 +21,7 @@ import driver.* from "./driver"
 export driver.* 
 import consensus.* from "./consensus"
 export consensus.* 
-import voteBookkeeper.* from "./voteBookkeeper"
+import voteBookkeeper.* from "./votekeeper"
 
 const validators: Set[Address]
 const validatorSet: Address -> Weight

diff --git a/Specs/Quint/specs/votekeeper.qnt b/Specs/Quint/specs/votekeeper.qnt
@@ -3,8 +3,8 @@
 module voteBookkeeper {
 
     import types.* from "./types"
-    import basicSpells.* from "./basicSpells"
-    import extraSpells.* from "./extraSpells"
+    import basicSpells.* from "../spells/basic"
+    import extraSpells.* from "../spells/extra"
 
     // ****************************************************************************
     // Types

diff --git a/Specs/Quint/spells/extra.qnt b/Specs/Quint/spells/extra.qnt
@@ -8,7 +8,7 @@
  */
 module extraSpells {
 
-  import basicSpells.* from "./basicSpells"
+  import basicSpells.* from "./basic"
 
   pure def printVariable(name: str, variable: a): bool = true
 

diff --git a/Specs/Quint/tests/consensus/consensusTest.qnt b/Specs/Quint/tests/consensus/consensusTest.qnt
@@ -2,8 +2,8 @@
 
 module consensusTest {
 
-    import types.* from "./types"
-    import consensus.* from "./consensus"
+    import types.* from "../../specs/types"
+    import consensus.* from "../../specs/consensus"
 
     // *************************************************************************
     // Consensus state machine

diff --git a/Specs/Quint/tests/disagreement/disagreementRun.qnt b/Specs/Quint/tests/disagreement/disagreementRun.qnt
@@ -2,7 +2,7 @@
 
 module disagreementRun {
 
-import TendermintDSL.* from "./TendermintDSL"
+import TendermintDSL.* from "../../specs/TendermintDSL"
 export TendermintDSL.*
 
 const groupA : Set[Address]

diff --git a/Specs/Quint/tests/line28/line28run.qnt b/Specs/Quint/tests/line28/line28run.qnt
@@ -2,7 +2,7 @@
 
 module line28run {
 
-import TendermintDSL.* from "./TendermintDSL"
+import TendermintDSL.* from "../../specs/TendermintDSL"
 export TendermintDSL.*
 
 const otherSet: Set[Address]
@@ -36,4 +36,4 @@ run runToLine28 =
         unchangedAll
     })
 
-}
+}
diff --git a/Specs/Quint/tests/line42/line42run.qnt b/Specs/Quint/tests/line42/line42run.qnt
@@ -2,7 +2,7 @@
 
 module line42run {
 
-import TendermintDSL.* from "./TendermintDSL"
+import TendermintDSL.* from "../../specs/TendermintDSL"
 export TendermintDSL.*
 
 const testedVal : Address

diff --git a/Specs/Quint/tests/multi-round/someMultiRoundRuns.qnt b/Specs/Quint/tests/multi-round/someMultiRoundRuns.qnt
@@ -2,7 +2,7 @@
 
 module someMultiRoundRuns {
 
-import TendermintDSL.* from "./TendermintDSL"
+import TendermintDSL.* from "../../specs/TendermintDSL"
 export TendermintDSL.*
 
 const slow : Address
@@ -104,4 +104,4 @@ run RoundswitchRun = {
 
 
 
-}
+}
diff --git a/Specs/Quint/tests/state-machine/parameterizedTest.qnt b/Specs/Quint/tests/state-machine/parameterizedTest.qnt
@@ -2,16 +2,16 @@
 
 module parameterizedTest {
 
-import types.* from "./types"
-import extraSpells.* from "./extraSpells"
+import types.* from "../../specs/types"
+import extraSpells.* from "./../spells/extra"
 import statemachineAsync(
     validators = Set("v1", "v2", "v3", "v4"),
     validatorSet = Set("v1", "v2", "v3", "v4").mapBy(x => 1),
     Faulty = Set(),
     Values = Set("a", "b"),
     Rounds = Set(0, 1, 2, 3),
     Heights = Set(0) // , 1, 2, 3)
-) as N4F0 from "./statemachineAsync"
+) as N4F0 from "../../specs/statemachineAsync"
 
 val validatorList = N4F0::validators.fold(List(), (s, x) => s.append(x))
 
@@ -96,4 +96,4 @@ run multiRoundTest = {
 
 
 
-}
+}
diff --git a/Specs/Quint/tests/state-machine/statemachineTest.qnt b/Specs/Quint/tests/state-machine/statemachineTest.qnt
@@ -12,11 +12,11 @@
 
 module statemachineTest {
 
-import types.* from "./types"
-import extraSpells.* from "./extraSpells"
-import driver.* from "./driver"
-import consensus.* from "./consensus"
-import voteBookkeeper.* from "./voteBookkeeper"
+import types.* from "../../specs/types"
+import extraSpells.* from "../../spells/extra"
+import driver.* from "../../specs/driver"
+import consensus.* from "../../specs/consensus"
+import voteBookkeeper.* from "../../votekeeper"
 
 val validators = Set("v1", "v2", "v3", "v4")
 val validatorSet = validators.mapBy(x => 1)

diff --git a/Specs/Quint/tests/votekeeper/voteBookkeeperModels.qnt b/Specs/Quint/tests/votekeeper/voteBookkeeperModels.qnt
@@ -6,8 +6,8 @@
 
 module voteBookkeeperSM  {
 
-    import types.* from "./types"
-    import voteBookkeeper.* from "./voteBookkeeper"
+    import types.* from "../../specs/types"
+    import voteBookkeeper.* from "../../specs/votekeeper"
     export voteBookkeeper.*
 
     // ************************************************************************

diff --git a/Specs/Quint/tests/votekeeper/voteBookkeeperTest.qnt b/Specs/Quint/tests/votekeeper/voteBookkeeperTest.qnt
@@ -2,8 +2,8 @@
 
 module voteBookkeeperTest {
 
-    import types.* from "./types"
-    import voteBookkeeper.* from "./voteBookkeeper"
+    import types.* from "../../specs/types"
+    import voteBookkeeper.* from "../../specs/votekeeper"
 
     // ****************************************************************************
     // Tests