lemmy
commented
3 months ago FWIW: Replacing Tstamp and Views with finite sets makes Apalache start bounded model checking. However, some construct causes it to expand the sets.
diff --git a/pbft.tla b/pbft.tla
index 8f90780..201a18d 100644
--- a/pbft.tla
+++ b/pbft.tla
@@ -37,7 +37,7 @@ ASSUME ByzR \subseteq R
\* Set of request timestamps
\* We use just natural numbers as there's a single client
-Tstamps == Nat
+Tstamps == 0..0
\* Set of sequence numbers
\* Bounding sequence numbers to the total number of requests
@@ -59,7 +59,7 @@ States == SeqNums \union {0}
Results == SeqNums
\* Set of possible views
-Views == Nat
+Views == 0..100
\* RequestDigest takes a client request and returns a unique identifier
\* Since we are assuming timestamps are unique, we can use them as the digest-> % ./apalache-0.44.11/bin/apalache-mc check --cinit=ConstInit --inv=Inv --no-deadlock MCpbft.tla
20:27:55.744 [main] INFO at.forsyte.apalache.tla.tooling.opt.CheckCmd -- Loading configuration
20:27:55.769 [main] INFO at.forsyte.apalache.tla.tooling.opt.CheckCmd -- > TLC config file found in specification directory. To enable it, pass --config=MCpbft.cfg.
# Usage statistics is ON. Thank you!
# If you have changed your mind, disable the statistics with config --enable-stats=false.
Output directory: /Users/markus/src/TLA/_specs/MSFT/pbft-tlaplus/_apalache-out/MCpbft.tla/2024-07-28T20-27-55_3165530396224552025
# APALACHE version: 0.44.11 | build: 5dee24e I@20:27:55.968
Tuning: search.outputTraces=false I@20:27:55.987
PASS #0: SanyParser I@20:27:56.123
Parsing file /Users/markus/src/TLA/_specs/MSFT/pbft-tlaplus/MCpbft.tla
Parsing file /Users/markus/src/TLA/_specs/MSFT/pbft-tlaplus/pbft.tla
Parsing file /private/var/folders/7d/4x6z2cc91jl588ysynlc1tfc0000gn/T/Integers.tla
Parsing file /private/var/folders/7d/4x6z2cc91jl588ysynlc1tfc0000gn/T/FiniteSets.tla
Parsing file /private/var/folders/7d/4x6z2cc91jl588ysynlc1tfc0000gn/T/__rewire_tlc_in_apalache.tla
Parsing file /private/var/folders/7d/4x6z2cc91jl588ysynlc1tfc0000gn/T/Naturals.tla
Parsing file /private/var/folders/7d/4x6z2cc91jl588ysynlc1tfc0000gn/T/__rewire_sequences_in_apalache.tla
Parsing file /private/var/folders/7d/4x6z2cc91jl588ysynlc1tfc0000gn/T/__apalache_folds.tla
PASS #1: TypeCheckerSnowcat I@20:27:56.592
> Running Snowcat .::. I@20:27:56.592
> Your types are purrfect! I@20:27:58.087
> All expressions are typed I@20:27:58.087
PASS #2: ConfigurationPass I@20:27:58.088
> Set the initialization predicate to Init I@20:27:58.092
> Set the transition predicate to Next I@20:27:58.092
> Set the constant initialization predicate to ConstInit I@20:27:58.093
> Set an invariant to Inv I@20:27:58.093
PASS #3: DesugarerPass I@20:27:58.098
> Desugaring... I@20:27:58.098
PASS #4: InlinePass I@20:27:58.270
Leaving only relevant operators: ConstInit, ConstInitPrimed, Init, InitPrimed, Inv, Next I@20:27:58.270
PASS #5: TemporalPass I@20:27:58.350
> Rewriting temporal operators... I@20:27:58.351
> No temporal property specified, nothing to encode I@20:27:58.351
PASS #6: InlinePass I@20:27:58.351
Leaving only relevant operators: ConstInit, ConstInitPrimed, Init, InitPrimed, Inv, Next I@20:27:58.351
PASS #7: PrimingPass I@20:27:58.364
> Introducing ConstInitPrimed for ConstInit' I@20:27:58.366
> Introducing InitPrimed for Init' I@20:27:58.369
PASS #8: VCGen I@20:27:58.369
> Producing verification conditions from the invariant Inv I@20:27:58.370
> VCGen produced 8 verification condition(s) I@20:27:58.375
PASS #9: PreprocessingPass I@20:27:58.376
> Before preprocessing: unique renaming I@20:27:58.376
> Applying standard transformations: I@20:27:58.382
> PrimePropagation I@20:27:58.382
> Desugarer I@20:27:58.386
> UniqueRenamer I@20:27:58.391
> Normalizer I@20:27:58.399
> Keramelizer I@20:27:58.423
> After preprocessing: UniqueRenamer I@20:27:58.465
PASS #10: TransitionFinderPass I@20:27:58.482
> Found 1 initializing transitions I@20:27:58.527
> Found 13 transitions I@20:27:58.539
> Found constant initializer ConstInit I@20:27:58.540
> Applying unique renaming I@20:27:58.542
PASS #11: OptimizationPass I@20:27:58.554
> Applying optimizations: I@20:27:58.559
> ConstSimplifier I@20:27:58.559
> ExprOptimizer I@20:27:58.578
> SetMembershipSimplifier I@20:27:58.593
> ConstSimplifier I@20:27:58.597
PASS #12: AnalysisPass I@20:27:58.615
> Marking skolemizable existentials and sets to be expanded... I@20:27:58.617
> Skolemization I@20:27:58.617
> Expansion I@20:27:58.618
> Remove unused let-in defs I@20:27:58.628
> Running analyzers... I@20:27:58.635
> Introduced expression grades I@20:27:58.647
PASS #13: BoundedChecker I@20:27:58.648
State 0: Checking 8 state invariants I@20:28:00.305
The set $C$2265 is expanded, producing O(2^404) constraints. This may slow down the solver. W@20:28:00.750
<unknown>: rewriter error: Attempted to expand a powerset of size 2^404 E@20:28:00.769
at.forsyte.apalache.infra.AdaptedException: <unknown>: rewriter error: Attempted to expand a powerset of size 2^404
at at.forsyte.apalache.infra.passes.PassChainExecutor$.run(PassChainExecutor.scala:39)
at at.forsyte.apalache.tla.tooling.opt.CheckCmd.run(CheckCmd.scala:129)
at at.forsyte.apalache.tla.Tool$.runCommand(Tool.scala:138)
at at.forsyte.apalache.tla.Tool$.run(Tool.scala:118)
at at.forsyte.apalache.tla.Tool$.main(Tool.scala:40)
at at.forsyte.apalache.tla.Tool.main(Tool.scala)
Please report an issue at [https://github.com/informalsystems/apalache/issues]: at.forsyte.apalache.infra.AdaptedException: <unknown>: rewriter error: Attempted to expand a powerset of size 2^404
A bug report template has been generated at [/Users/markus/src/TLA/_specs/MSFT/pbft-tlaplus/_apalache-out/MCpbft.tla/2024-07-28T20-27-55_3165530396224552025/BugReport.md].
If you choose to use it, please complete the template with a description of the expected behavior and impact.
It took me 0 days 0 hours 0 min 4 sec I@20:28:00.776
Total time: 4.804 sec I@20:28:00.776
EXITCODE: ERROR (255)
heidihoward
Related: https://github.com/apalache-mc/apalache/blob/main/docs/src/lang/records.md https://apalache.informal.systems/docs/adr/002adr-types.html#13-type-system-12-including-precise-records-variants-and-rows https://github.com/apalache-mc/apalache/blob/main/docs/src/adr/014adr-precise-records.md