Skip to content

Commit

Permalink
Start rewriting model
Browse files Browse the repository at this point in the history
  • Loading branch information
p-offtermatt committed Sep 18, 2023
1 parent 2126eac commit 1320b95
Show file tree
Hide file tree
Showing 10 changed files with 790 additions and 551 deletions.
1,241 changes: 691 additions & 550 deletions tests/difference/core/quint_model/ccv.qnt

Large diffs are not rendered by default.

1 change: 0 additions & 1 deletion tests/difference/core/quint_model/extraSpells.qnt
Original file line number Diff line number Diff line change
@@ -1,4 +1,3 @@
-*- mode: Bluespec; -*-
// This module is just a library with utility functions (sometimes called spells in Quint).
module extraSpells {

Expand Down
Original file line number Diff line number Diff line change
@@ -0,0 +1,18 @@
# 2023/09/12 12:33:37 TestActionMarshalling [rapid] draw Action: main.StartChainAction{Chain:"", Validators:[]main.StartChainValidator{}, GenesisChanges:"", SkipGentx:false}
# 2023/09/12 12:33:37 TestActionMarshalling error marshalling and unmarshalling chain state: any(
# - main.StartChainAction{Validators: []main.StartChainValidator{}},
# + map[string]any{
# + "Chain": string(""),
# + "GenesisChanges": string(""),
# + "SkipGentx": bool(false),
# + "Validators": []any{},
# + },
# )
#
v0.4.8#6863100771198181688
0x0
0x1
0x0
0x0
0x0
0x0
Original file line number Diff line number Diff line change
@@ -0,0 +1,14 @@
# 2023/09/12 12:35:17 TestActionMarshalling [rapid] draw Action: main.SendTokensAction{Chain:"", From:"", To:"", Amount:0x0}
# 2023/09/12 12:35:17 TestActionMarshalling error marshalling and unmarshalling action: got (+), want (-):   any(
# -  main.SendTokensAction{},
# +  map[string]any{"Amount": float64(0), "Chain": string(""), "From": string(""), "To": string("")},
#   )
#
v0.4.8#14250065908211800578
0x0
0x0
0x0
0x0
0x0
0x0
0x0
Original file line number Diff line number Diff line change
@@ -0,0 +1,14 @@
# 2023/09/12 12:35:56 TestActionMarshalling [rapid] draw Action: main.SendTokensAction{Chain:"", From:"", To:"", Amount:0x0}
# 2023/09/12 12:35:56 TestActionMarshalling error marshalling and unmarshalling action: got (-), want (+):   any(
# -  main.SendTokensAction{},
# +  map[string]any{"Amount": float64(0), "Chain": string(""), "From": string(""), "To": string("")},
#   )
#
v0.4.8#9176735344445930654
0x0
0x0
0x0
0x0
0x0
0x0
0x0
Original file line number Diff line number Diff line change
@@ -0,0 +1,18 @@
# 2023/09/12 12:36:09 TestActionMarshalling [rapid] draw Action: main.StartChainAction{Chain:"", Validators:[]main.StartChainValidator{}, GenesisChanges:"", SkipGentx:false}
# 2023/09/12 12:36:09 TestActionMarshalling error marshalling and unmarshalling action: got (-), want (+): any(
# - main.StartChainAction{Validators: []main.StartChainValidator{}},
# + map[string]any{
# + "Chain": string(""),
# + "GenesisChanges": string(""),
# + "SkipGentx": bool(false),
# + "Validators": []any{},
# + },
# )
#
v0.4.8#17927886955469684979
0x0
0x1
0x0
0x0
0x0
0x0
Original file line number Diff line number Diff line change
@@ -0,0 +1,8 @@
# 2023/09/12 12:38:22 TestActionMarshalling [rapid] draw Action: main.addChainToRelayerAction{Chain:"", Validator:""}
# 2023/09/12 12:38:22 TestActionMarshalling error marshalling and unmarshalling action: error unmarshalling action inside step: unknown action name: main.addChainToRelayerAction
#
v0.4.8#17613601115647214278
0x9867f1f40f739
0x9
0x0
0x0
Original file line number Diff line number Diff line change
@@ -0,0 +1,8 @@
# 2023/09/13 15:18:26 TestActionMarshalling [rapid] draw Action: main.lightClientEquivocationAttackAction{Validator:"", Chain:""}
# 2023/09/13 15:18:26 TestActionMarshalling error marshalling and unmarshalling action: error unmarshalling action inside step: unknown action name: main.lightClientEquivocationAttackAction
#
v0.4.8#7694661539125204314
0xc05c654ab866b
0x1f
0x0
0x0
Original file line number Diff line number Diff line change
@@ -0,0 +1,8 @@
# 2023/09/13 15:19:17 TestActionMarshalling [rapid] draw Action: main.lightClientLunaticAttackAction{Validator:"", Chain:""}
# 2023/09/13 15:19:17 TestActionMarshalling error marshalling and unmarshalling action: error unmarshalling action inside step: unknown action name: main.lightClientLunaticAttackAction
#
v0.4.8#10796173543550944397
0x1f2b5a0e61c3a6
0x0
0x0
0x0
Original file line number Diff line number Diff line change
@@ -0,0 +1,11 @@
# 2023/09/13 15:19:20 TestReadAndWriteTrace [rapid] draw Trace: []main.Step{main.Step{Action:main.lightClientEquivocationAttackAction{Validator:"", Chain:""}, State:main.State{}}}
# 2023/09/13 15:19:20 TestReadAndWriteTrace error writing and reading trace: error reading trace from file: unknown action name: main.lightClientEquivocationAttackAction
#
v0.4.8#17668525343613541116
0x5555555555555
0xc05c654ab866b
0x1f
0x0
0x0
0x0
0x0

0 comments on commit 1320b95

Please sign in to comment.