1this derivation will be built:2 /nix/store/dya24l1lmm138d3b1826q2h2fhp5vrh2-spec-protocol.drv3these 4 paths will be fetched (568.0 MiB download, 852.7 MiB unpacked):4 /nix/store/ij5q131fzyqw8wh76y9nrj5jl45zviqw-openjdk-21.0.12+85 /nix/store/s90yin0j1q75gr8iyr11qxqzbjdssv25-quint-0.32.06 /nix/store/mx71fx62163cbid5nc6k7vvcmpg8r609-quint-cli-0.32.07 /nix/store/ma9wr3rh0rr0plzz5dmh87dxk734n7hk-set-java-classpath-hook8building '/nix/store/dya24l1lmm138d3b1826q2h2fhp5vrh2-spec-protocol.drv'9spec-protocol> > [1/3] Checking whether the inductive invariant 'indInv' holds in the initial state(s) defined by 'init'...10spec-protocol> # Usage statistics is OFF. We care about your privacy.11spec-protocol> # If you want to help our project, consider enabling statistics with config --enable-stats=true.12spec-protocol> 13spec-protocol> Output directory: /build/_apalache-out/server/2026-09-01T10-45-10_1057276099345310864314spec-protocol> # APALACHE version: 0.56.1 | build: 70cdaf4 I@10:45:10.36315spec-protocol> Starting checker server on port 8822... I@10:45:10.40016spec-protocol> The Apalache server is running on port 8822. Press Ctrl-C to stop.17spec-protocol> Failed to find a usable hardware address from the network interfaces; using random bytes: 72:1b:39:fd:09:42:45:61 W@10:45:12.29818spec-protocol> Sep 01, 2026 10:45:16 AM com.google.protobuf.GeneratedMessage warnPre22Gencode19spec-protocol> WARNING: Vulnerable protobuf generated type in use: io.grpc.reflection.v1alpha.ServerReflectionRequest20spec-protocol> As of 2022/09/29 (release 21.7) makeExtensionsImmutable should not be called from protobuf gencode. If you are seeing this message, your gencode is vulnerable to a denial of service attack. You should regenerate your code using protobuf 25.6 or later. Use the latest version that meets your needs. However, if you understand the risks and wish to continue with vulnerable gencode, you can set the system property `-Dcom.google.protobuf.use_unsafe_pre22_gencode` on the command line to silence this warning. You also can set `-Dcom.google.protobuf.error_on_unsafe_pre22_gencode` to throw an error instead. See security vulnerability: https://github.com/protocolbuffers/protobuf/security/advisories/GHSA-h4h5-3hr4-j3g221spec-protocol> PASS #0: SanyParser I@10:45:17.34022spec-protocol> PASS #1: TypeCheckerSnowcat I@10:45:18.46423spec-protocol> > Running Snowcat .::. I@10:45:18.46424spec-protocol> > Your types are purrfect! I@10:45:24.51525spec-protocol> > All expressions are typed I@10:45:24.51526spec-protocol> PASS #2: ConfigurationPass I@10:45:24.51727spec-protocol> > Set the initialization predicate to q::init I@10:45:24.52328spec-protocol> > Set the transition predicate to q::step I@10:45:24.52429spec-protocol> > Set an invariant to q::inductiveInv I@10:45:24.52430spec-protocol> PASS #3: DesugarerPass I@10:45:24.53431spec-protocol> > Desugaring... I@10:45:24.53432spec-protocol> PASS #4: InlinePass I@10:45:24.56133spec-protocol> Leaving only relevant operators: CInitPrimed, q::inductiveInv, q::init, q::initPrimed, q::step I@10:45:24.56134spec-protocol> PASS #5: TemporalPass I@10:45:24.72935spec-protocol> > Rewriting temporal operators... I@10:45:24.72936spec-protocol> > No temporal property specified, nothing to encode I@10:45:24.72937spec-protocol> PASS #6: InlinePass I@10:45:24.73238spec-protocol> Leaving only relevant operators: CInitPrimed, q::inductiveInv, q::init, q::initPrimed, q::step I@10:45:24.73239spec-protocol> PASS #7: PrimingPass I@10:45:24.77840spec-protocol> > Introducing q::initPrimed for q::init' I@10:45:24.78141spec-protocol> PASS #8: VCGen I@10:45:24.78342spec-protocol> > Producing verification conditions from the invariant q::inductiveInv I@10:45:24.78443spec-protocol> > VCGen produced 39 verification condition(s) I@10:45:24.79444spec-protocol> PASS #9: PreprocessingPass I@10:45:24.80045spec-protocol> > Before preprocessing: unique renaming I@10:45:24.80046spec-protocol> > Applying standard transformations: I@10:45:24.80747spec-protocol> > PrimePropagation I@10:45:24.80748spec-protocol> > Desugarer I@10:45:24.82149spec-protocol> > UniqueRenamer I@10:45:24.83950spec-protocol> > Normalizer I@10:45:24.89551spec-protocol> > Keramelizer I@10:45:24.93152spec-protocol> > After preprocessing: UniqueRenamer I@10:45:24.98353spec-protocol> PASS #10: TransitionFinderPass I@10:45:25.03354spec-protocol> > Found 1 initializing transitions I@10:45:25.04555spec-protocol> > Found 24 transitions I@10:45:25.09456spec-protocol> > No constant initializer I@10:45:25.09557spec-protocol> > Applying unique renaming I@10:45:25.09658spec-protocol> PASS #11: OptimizationPass I@10:45:25.14159spec-protocol> > Applying optimizations: I@10:45:25.14860spec-protocol> > ConstSimplifier I@10:45:25.14961spec-protocol> > ExprOptimizer I@10:45:25.22962spec-protocol> > SetMembershipSimplifier I@10:45:25.25963spec-protocol> > ConstSimplifier I@10:45:25.27064spec-protocol> PASS #12: AnalysisPass I@10:45:25.34565spec-protocol> > Marking skolemizable existentials and sets to be expanded... I@10:45:25.34766spec-protocol> > Skolemization I@10:45:25.34867spec-protocol> > Expansion I@10:45:25.35868spec-protocol> > Remove unused let-in defs I@10:45:25.38669spec-protocol> > Running analyzers... I@10:45:25.40570spec-protocol> > Introduced expression grades I@10:45:25.41771spec-protocol> PASS #13: BoundedChecker I@10:45:25.41872spec-protocol> State 0: Checking 39 state invariants I@10:45:25.88873spec-protocol> State 0: state invariant 0 holds. I@10:45:25.89274spec-protocol> State 0: state invariant 1 holds. I@10:45:25.96575spec-protocol> State 0: state invariant 2 holds. I@10:45:25.96676spec-protocol> State 0: state invariant 3 holds. I@10:45:25.96977spec-protocol> State 0: state invariant 4 holds. I@10:45:26.00878spec-protocol> State 0: state invariant 5 holds. I@10:45:26.02779spec-protocol> State 0: state invariant 6 holds. I@10:45:26.03180spec-protocol> State 0: state invariant 7 holds. I@10:45:26.03281spec-protocol> State 0: state invariant 8 holds. I@10:45:26.03582spec-protocol> State 0: state invariant 9 holds. I@10:45:26.05283spec-protocol> State 0: state invariant 10 holds. I@10:45:26.05584spec-protocol> State 0: state invariant 11 holds. I@10:45:26.05685spec-protocol> State 0: state invariant 12 holds. I@10:45:26.09186spec-protocol> State 0: state invariant 13 holds. I@10:45:26.09587spec-protocol> State 0: state invariant 14 holds. I@10:45:26.10988spec-protocol> State 0: state invariant 15 holds. I@10:45:26.11689spec-protocol> State 0: state invariant 16 holds. I@10:45:26.11990spec-protocol> State 0: state invariant 17 holds. I@10:45:26.12091spec-protocol> State 0: state invariant 18 holds. I@10:45:26.12692spec-protocol> State 0: state invariant 19 holds. I@10:45:26.13193spec-protocol> State 0: state invariant 20 holds. I@10:45:26.15694spec-protocol> State 0: state invariant 21 holds. I@10:45:26.18295spec-protocol> State 0: state invariant 22 holds. I@10:45:26.18796spec-protocol> State 0: state invariant 23 holds. I@10:45:26.21897spec-protocol> State 0: state invariant 24 holds. I@10:45:26.22398spec-protocol> State 0: state invariant 25 holds. I@10:45:26.22499spec-protocol> State 0: state invariant 26 holds. I@10:45:26.238100spec-protocol> State 0: state invariant 27 holds. I@10:45:26.250101spec-protocol> State 0: state invariant 28 holds. I@10:45:26.275102spec-protocol> State 0: state invariant 29 holds. I@10:45:26.287103spec-protocol> State 0: state invariant 30 holds. I@10:45:26.316104spec-protocol> State 0: state invariant 31 holds. I@10:45:26.369105spec-protocol> State 0: state invariant 32 holds. I@10:45:26.411106spec-protocol> State 0: state invariant 33 holds. I@10:45:26.412107spec-protocol> State 0: state invariant 34 holds. I@10:45:26.418108spec-protocol> State 0: state invariant 35 holds. I@10:45:26.423109spec-protocol> State 0: state invariant 36 holds. I@10:45:26.425110spec-protocol> State 0: state invariant 37 holds. I@10:45:26.426111spec-protocol> State 0: state invariant 38 holds. I@10:45:26.427112spec-protocol> Step 0: picking a transition out of 1 transition(s) I@10:45:26.427113spec-protocol> The outcome is: NoError I@10:45:26.437114spec-protocol> > [2/3] Checking whether 'step' preserves the inductive invariant 'indInv'...115spec-protocol> PASS #0: SanyParser I@10:45:26.888116spec-protocol> PASS #1: TypeCheckerSnowcat I@10:45:27.120117spec-protocol> > Running Snowcat .::. I@10:45:27.120118spec-protocol> > Your types are purrfect! I@10:45:31.268119spec-protocol> > All expressions are typed I@10:45:31.269120spec-protocol> PASS #2: ConfigurationPass I@10:45:31.269121spec-protocol> > Set the initialization predicate to q::inductiveInv I@10:45:31.270122spec-protocol> > Set the transition predicate to q::step I@10:45:31.270123spec-protocol> > Set an invariant to q::inductiveInv I@10:45:31.270124spec-protocol> PASS #3: DesugarerPass I@10:45:31.274125spec-protocol> > Desugaring... I@10:45:31.274126spec-protocol> PASS #4: InlinePass I@10:45:31.277127spec-protocol> Leaving only relevant operators: CInitPrimed, q::inductiveInv, q::inductiveInvPrimed, q::step I@10:45:31.278128spec-protocol> PASS #5: TemporalPass I@10:45:31.349129spec-protocol> > Rewriting temporal operators... I@10:45:31.349130spec-protocol> > No temporal property specified, nothing to encode I@10:45:31.349131spec-protocol> PASS #6: InlinePass I@10:45:31.349132spec-protocol> Leaving only relevant operators: CInitPrimed, q::inductiveInv, q::inductiveInvPrimed, q::step I@10:45:31.349133spec-protocol> PASS #7: PrimingPass I@10:45:31.375134spec-protocol> > Introducing q::inductiveInvPrimed for q::inductiveInv' I@10:45:31.375135spec-protocol> PASS #8: VCGen I@10:45:31.378136spec-protocol> > Producing verification conditions from the invariant q::inductiveInv I@10:45:31.378137spec-protocol> > VCGen produced 39 verification condition(s) I@10:45:31.380138spec-protocol> PASS #9: PreprocessingPass I@10:45:31.385139spec-protocol> > Before preprocessing: unique renaming I@10:45:31.386140spec-protocol> > Applying standard transformations: I@10:45:31.386141spec-protocol> > PrimePropagation I@10:45:31.386142spec-protocol> > Desugarer I@10:45:31.392143spec-protocol> > UniqueRenamer I@10:45:31.403144spec-protocol> > Normalizer I@10:45:31.432145spec-protocol> > Keramelizer I@10:45:31.465146spec-protocol> > After preprocessing: UniqueRenamer I@10:45:31.501147spec-protocol> PASS #10: TransitionFinderPass I@10:45:31.543148spec-protocol> > Found 1 initializing transitions I@10:45:31.549149spec-protocol> > Found 24 transitions I@10:45:31.575150spec-protocol> > No constant initializer I@10:45:31.575151spec-protocol> > Applying unique renaming I@10:45:31.576152spec-protocol> PASS #11: OptimizationPass I@10:45:31.624153spec-protocol> > Applying optimizations: I@10:45:31.624154spec-protocol> > ConstSimplifier I@10:45:31.624155spec-protocol> > ExprOptimizer I@10:45:31.757156spec-protocol> > SetMembershipSimplifier I@10:45:31.814157spec-protocol> > ConstSimplifier I@10:45:31.825158spec-protocol> PASS #12: AnalysisPass I@10:45:31.937159spec-protocol> > Marking skolemizable existentials and sets to be expanded... I@10:45:31.937160spec-protocol> > Skolemization I@10:45:31.937161spec-protocol> > Expansion I@10:45:31.946162spec-protocol> > Remove unused let-in defs I@10:45:31.990163spec-protocol> > Running analyzers... I@10:45:32.001164spec-protocol> > Introduced expression grades I@10:45:32.007165spec-protocol> PASS #13: BoundedChecker I@10:45:32.007166spec-protocol> State 0: Checking 39 state invariants I@10:45:33.226167spec-protocol> State 0: state invariant 0 holds. I@10:45:33.227168spec-protocol> State 0: state invariant 1 holds. I@10:45:33.261169spec-protocol> State 0: state invariant 2 holds. I@10:45:33.265170spec-protocol> State 0: state invariant 3 holds. I@10:45:33.268171spec-protocol> State 0: state invariant 4 holds. I@10:45:33.300172spec-protocol> State 0: state invariant 5 holds. I@10:45:33.321173spec-protocol> State 0: state invariant 6 holds. I@10:45:33.324174spec-protocol> State 0: state invariant 7 holds. I@10:45:33.325175spec-protocol> State 0: state invariant 8 holds. I@10:45:33.327176spec-protocol> State 0: state invariant 9 holds. I@10:45:33.330177spec-protocol> State 0: state invariant 10 holds. I@10:45:33.333178spec-protocol> State 0: state invariant 11 holds. I@10:45:33.335179spec-protocol> State 0: state invariant 12 holds. I@10:45:33.348180spec-protocol> State 0: state invariant 13 holds. I@10:45:33.352181spec-protocol> State 0: state invariant 14 holds. I@10:45:33.367182spec-protocol> State 0: state invariant 15 holds. I@10:45:33.370183spec-protocol> State 0: state invariant 16 holds. I@10:45:33.372184spec-protocol> State 0: state invariant 17 holds. I@10:45:33.374185spec-protocol> State 0: state invariant 18 holds. I@10:45:33.385186spec-protocol> State 0: state invariant 19 holds. I@10:45:33.396187spec-protocol> State 0: state invariant 20 holds. I@10:45:33.409188spec-protocol> State 0: state invariant 21 holds. I@10:45:33.434189spec-protocol> State 0: state invariant 22 holds. I@10:45:33.456190spec-protocol> State 0: state invariant 23 holds. I@10:45:33.470191spec-protocol> State 0: state invariant 24 holds. I@10:45:33.472192spec-protocol> State 0: state invariant 25 holds. I@10:45:33.473193spec-protocol> State 0: state invariant 26 holds. I@10:45:33.476194spec-protocol> State 0: state invariant 27 holds. I@10:45:33.484195spec-protocol> State 0: state invariant 28 holds. I@10:45:33.545196spec-protocol> State 0: state invariant 29 holds. I@10:45:33.559197spec-protocol> State 0: state invariant 30 holds. I@10:45:33.773198spec-protocol> State 0: state invariant 31 holds. I@10:45:33.969199spec-protocol> State 0: state invariant 32 holds. I@10:45:34.205200spec-protocol> State 0: state invariant 33 holds. I@10:45:34.209201spec-protocol> State 0: state invariant 34 holds. I@10:45:34.217202spec-protocol> State 0: state invariant 35 holds. I@10:45:34.226203spec-protocol> State 0: state invariant 36 holds. I@10:45:34.228204spec-protocol> State 0: state invariant 37 holds. I@10:45:34.231205spec-protocol> State 0: state invariant 38 holds. I@10:45:34.233206spec-protocol> Step 0: picking a transition out of 1 transition(s) I@10:45:34.234207spec-protocol> State 1: Checking 12 state invariants I@10:45:34.272208spec-protocol> State 1: state invariant 0 holds. I@10:45:34.274209spec-protocol> State 1: state invariant 1 holds. I@10:45:34.311210spec-protocol> State 1: state invariant 18 holds. I@10:45:34.324211spec-protocol> State 1: state invariant 19 holds. I@10:45:34.333212spec-protocol> State 1: state invariant 20 holds. I@10:45:34.345213spec-protocol> State 1: state invariant 21 holds. I@10:45:34.359214spec-protocol> State 1: state invariant 27 holds. I@10:45:34.374215spec-protocol> State 1: state invariant 28 holds. I@10:45:34.413216spec-protocol> State 1: state invariant 29 holds. I@10:45:34.422217spec-protocol> State 1: state invariant 30 holds. I@10:45:34.631218spec-protocol> State 1: state invariant 31 holds. I@10:45:34.848219spec-protocol> State 1: state invariant 32 holds. I@10:45:35.115220spec-protocol> State 1: Checking 4 state invariants I@10:45:35.217221spec-protocol> State 1: state invariant 13 holds. I@10:45:35.220222spec-protocol> State 1: state invariant 29 holds. I@10:45:35.230223spec-protocol> State 1: state invariant 30 holds. I@10:45:35.640224spec-protocol> State 1: state invariant 31 holds. I@10:45:35.952225spec-protocol> State 1: Checking 16 state invariants I@10:45:36.126226spec-protocol> State 1: state invariant 0 holds. I@10:45:36.130227spec-protocol> State 1: state invariant 1 holds. I@10:45:36.171228spec-protocol> State 1: state invariant 3 holds. I@10:45:36.179229spec-protocol> State 1: state invariant 4 holds. I@10:45:36.225230spec-protocol> State 1: state invariant 5 holds. I@10:45:36.241231spec-protocol> State 1: state invariant 18 holds. I@10:45:36.252232spec-protocol> State 1: state invariant 19 holds. I@10:45:36.263233spec-protocol> State 1: state invariant 20 holds. I@10:45:36.275234spec-protocol> State 1: state invariant 21 holds. I@10:45:36.289235spec-protocol> State 1: state invariant 23 holds. I@10:45:36.305236spec-protocol> State 1: state invariant 27 holds. I@10:45:36.312237spec-protocol> State 1: state invariant 28 holds. I@10:45:36.340238spec-protocol> State 1: state invariant 29 holds. I@10:45:36.348239spec-protocol> State 1: state invariant 30 holds. I@10:45:36.463240spec-protocol> State 1: state invariant 31 holds. I@10:45:36.593241spec-protocol> State 1: state invariant 32 holds. I@10:45:36.805242spec-protocol> State 1: Checking 6 state invariants I@10:45:36.824243spec-protocol> State 1: state invariant 2 holds. I@10:45:36.826244spec-protocol> State 1: state invariant 27 holds. I@10:45:36.839245spec-protocol> State 1: state invariant 29 holds. I@10:45:36.846246spec-protocol> State 1: state invariant 30 holds. I@10:45:37.026247spec-protocol> State 1: state invariant 31 holds. I@10:45:37.177248spec-protocol> State 1: state invariant 38 holds. I@10:45:37.181249spec-protocol> State 1: Checking 15 state invariants I@10:45:37.204250spec-protocol> State 1: state invariant 0 holds. I@10:45:37.205251spec-protocol> State 1: state invariant 1 holds. I@10:45:37.237252spec-protocol> State 1: state invariant 2 holds. I@10:45:37.239253spec-protocol> State 1: state invariant 12 holds. I@10:45:37.252254spec-protocol> State 1: state invariant 18 holds. I@10:45:37.266255spec-protocol> State 1: state invariant 19 holds. I@10:45:37.275256spec-protocol> State 1: state invariant 20 holds. I@10:45:37.289257spec-protocol> State 1: state invariant 21 holds. I@10:45:37.307258spec-protocol> State 1: state invariant 27 holds. I@10:45:37.321259spec-protocol> State 1: state invariant 28 holds. I@10:45:37.364260spec-protocol> State 1: state invariant 29 holds. I@10:45:37.373261spec-protocol> State 1: state invariant 30 holds. I@10:45:37.575262spec-protocol> State 1: state invariant 31 holds. I@10:45:37.753263spec-protocol> State 1: state invariant 32 holds. I@10:45:37.920264spec-protocol> State 1: state invariant 37 holds. I@10:45:37.923265spec-protocol> State 1: Checking 18 state invariants I@10:45:38.202266spec-protocol> State 1: state invariant 9 holds. I@10:45:38.209267spec-protocol> State 1: state invariant 10 holds. I@10:45:38.211268spec-protocol> State 1: state invariant 11 holds. I@10:45:38.213269spec-protocol> State 1: state invariant 14 holds. I@10:45:38.223270spec-protocol> State 1: state invariant 15 holds. I@10:45:38.226271spec-protocol> State 1: state invariant 17 holds. I@10:45:38.228272spec-protocol> State 1: state invariant 22 holds. I@10:45:38.239273spec-protocol> State 1: state invariant 24 holds. I@10:45:38.242274spec-protocol> State 1: state invariant 26 holds. I@10:45:38.246275spec-protocol> State 1: state invariant 27 holds. I@10:45:38.258276spec-protocol> State 1: state invariant 28 holds. I@10:45:38.292277spec-protocol> State 1: state invariant 29 holds. I@10:45:38.303278spec-protocol> State 1: state invariant 30 holds. I@10:45:38.386279spec-protocol> State 1: state invariant 31 holds. I@10:45:38.490280spec-protocol> State 1: state invariant 32 holds. I@10:45:38.668281spec-protocol> State 1: state invariant 33 holds. I@10:45:38.676282spec-protocol> State 1: state invariant 34 holds. I@10:45:38.684283spec-protocol> State 1: state invariant 35 holds. I@10:45:38.704284spec-protocol> State 1: Checking 14 state invariants I@10:45:39.277285spec-protocol> State 1: state invariant 9 holds. I@10:45:39.287286spec-protocol> State 1: state invariant 10 holds. I@10:45:39.291287spec-protocol> State 1: state invariant 11 holds. I@10:45:39.294288spec-protocol> State 1: state invariant 14 holds. I@10:45:39.319289spec-protocol> State 1: state invariant 15 holds. I@10:45:39.333290spec-protocol> State 1: state invariant 17 holds. I@10:45:39.340291spec-protocol> State 1: state invariant 24 holds. I@10:45:39.350292spec-protocol> State 1: state invariant 26 holds. I@10:45:39.362293spec-protocol> State 1: state invariant 27 holds. I@10:45:39.387294spec-protocol> State 1: state invariant 28 holds. I@10:45:39.442295spec-protocol> State 1: state invariant 29 holds. I@10:45:39.467296spec-protocol> State 1: state invariant 30 holds. I@10:45:39.658297spec-protocol> State 1: state invariant 31 holds. I@10:45:39.921298spec-protocol> State 1: state invariant 32 holds. I@10:45:40.035299spec-protocol> State 1: Checking 26 state invariants I@10:45:40.334300spec-protocol> State 1: state invariant 0 holds. I@10:45:40.338301spec-protocol> State 1: state invariant 1 holds. I@10:45:40.387302spec-protocol> State 1: state invariant 9 holds. I@10:45:40.404303spec-protocol> State 1: state invariant 10 holds. I@10:45:40.408304spec-protocol> State 1: state invariant 11 holds. I@10:45:40.413305spec-protocol> State 1: state invariant 12 holds. I@10:45:40.429306spec-protocol> State 1: state invariant 14 holds. I@10:45:40.450307spec-protocol> State 1: state invariant 15 holds. I@10:45:40.481308spec-protocol> State 1: state invariant 17 holds. I@10:45:40.487309spec-protocol> State 1: state invariant 18 holds. I@10:45:40.534310spec-protocol> State 1: state invariant 19 holds. I@10:45:40.548311spec-protocol> State 1: state invariant 20 holds. I@10:45:40.569312spec-protocol> State 1: state invariant 21 holds. I@10:45:40.605313spec-protocol> State 1: state invariant 22 holds. I@10:45:40.627314spec-protocol> State 1: state invariant 23 holds. I@10:45:40.641315spec-protocol> State 1: state invariant 24 holds. I@10:45:40.646316spec-protocol> State 1: state invariant 26 holds. I@10:45:40.657317spec-protocol> State 1: state invariant 27 holds. I@10:45:40.699318spec-protocol> State 1: state invariant 28 holds. I@10:45:40.810319spec-protocol> State 1: state invariant 29 holds. I@10:45:40.824320spec-protocol> State 1: state invariant 30 holds. I@10:45:41.384321spec-protocol> State 1: state invariant 31 holds. I@10:45:42.104322spec-protocol> State 1: state invariant 32 holds. I@10:45:42.589323spec-protocol> State 1: state invariant 33 holds. I@10:45:42.597324spec-protocol> State 1: state invariant 34 holds. I@10:45:42.612325spec-protocol> State 1: state invariant 35 holds. I@10:45:42.640326spec-protocol> State 1: Checking 22 state invariants I@10:45:43.039327spec-protocol> State 1: state invariant 0 holds. I@10:45:43.043328spec-protocol> State 1: state invariant 1 holds. I@10:45:43.135329spec-protocol> State 1: state invariant 9 holds. I@10:45:43.171330spec-protocol> State 1: state invariant 10 holds. I@10:45:43.183331spec-protocol> State 1: state invariant 11 holds. I@10:45:43.195332spec-protocol> State 1: state invariant 12 holds. I@10:45:43.228333spec-protocol> State 1: state invariant 14 holds. I@10:45:43.277334spec-protocol> State 1: state invariant 15 holds. I@10:45:43.348335spec-protocol> State 1: state invariant 17 holds. I@10:45:43.360336spec-protocol> State 1: state invariant 18 holds. I@10:45:43.416337spec-protocol> State 1: state invariant 19 holds. I@10:45:43.583338spec-protocol> State 1: state invariant 20 holds. I@10:45:43.643339spec-protocol> State 1: state invariant 21 holds. I@10:45:43.677340spec-protocol> State 1: state invariant 23 holds. I@10:45:43.696341spec-protocol> State 1: state invariant 24 holds. I@10:45:43.708342spec-protocol> State 1: state invariant 26 holds. I@10:45:43.753343spec-protocol> State 1: state invariant 27 holds. I@10:45:43.806344spec-protocol> State 1: state invariant 28 holds. I@10:45:43.977345spec-protocol> State 1: state invariant 29 holds. I@10:45:43.993346spec-protocol> State 1: state invariant 30 holds. I@10:45:44.967347spec-protocol> State 1: state invariant 31 holds. I@10:45:45.628348spec-protocol> State 1: state invariant 32 holds. I@10:45:46.066349spec-protocol> Step 1: Transition #10 is disabled I@10:45:46.130350spec-protocol> Step 1: Transition #11 is disabled I@10:45:46.191351spec-protocol> State 1: Checking 27 state invariants I@10:45:46.702352spec-protocol> State 1: state invariant 0 holds. I@10:45:46.713353spec-protocol> State 1: state invariant 1 holds. I@10:45:46.840354spec-protocol> State 1: state invariant 9 holds. I@10:45:46.901355spec-protocol> State 1: state invariant 10 holds. I@10:45:46.910356spec-protocol> State 1: state invariant 12 holds. I@10:45:46.944357spec-protocol> State 1: state invariant 13 holds. I@10:45:46.961358spec-protocol> State 1: state invariant 14 holds. I@10:45:47.014359spec-protocol> State 1: state invariant 15 holds. I@10:45:47.108360spec-protocol> State 1: state invariant 16 holds. I@10:45:47.115361spec-protocol> State 1: state invariant 17 holds. I@10:45:47.120362spec-protocol> State 1: state invariant 18 holds. I@10:45:47.145363spec-protocol> State 1: state invariant 19 holds. I@10:45:47.177364spec-protocol> State 1: state invariant 20 holds. I@10:45:47.204365spec-protocol> State 1: state invariant 21 holds. I@10:45:47.234366spec-protocol> State 1: state invariant 22 holds. I@10:45:47.281367spec-protocol> State 1: state invariant 23 holds. I@10:45:47.320368spec-protocol> State 1: state invariant 24 holds. I@10:45:47.332369spec-protocol> State 1: state invariant 26 holds. I@10:45:47.346370spec-protocol> State 1: state invariant 27 holds. I@10:45:47.450371spec-protocol> State 1: state invariant 28 holds. I@10:45:47.568372spec-protocol> State 1: state invariant 29 holds. I@10:45:47.582373spec-protocol> State 1: state invariant 30 holds. I@10:45:48.436374spec-protocol> State 1: state invariant 31 holds. I@10:45:48.843375spec-protocol> State 1: state invariant 32 holds. I@10:45:49.350376spec-protocol> State 1: state invariant 33 holds. I@10:45:49.358377spec-protocol> State 1: state invariant 34 holds. I@10:45:49.376378spec-protocol> State 1: state invariant 35 holds. I@10:45:49.407379spec-protocol> State 1: Checking 23 state invariants I@10:45:49.854380spec-protocol> State 1: state invariant 0 holds. I@10:45:49.862381spec-protocol> State 1: state invariant 1 holds. I@10:45:49.911382spec-protocol> State 1: state invariant 9 holds. I@10:45:49.934383spec-protocol> State 1: state invariant 10 holds. I@10:45:49.939384spec-protocol> State 1: state invariant 12 holds. I@10:45:49.955385spec-protocol> State 1: state invariant 13 holds. I@10:45:49.962386spec-protocol> State 1: state invariant 14 holds. I@10:45:49.977387spec-protocol> State 1: state invariant 15 holds. I@10:45:49.997388spec-protocol> State 1: state invariant 16 holds. I@10:45:50.003389spec-protocol> State 1: state invariant 17 holds. I@10:45:50.008390spec-protocol> State 1: state invariant 18 holds. I@10:45:50.022391spec-protocol> State 1: state invariant 19 holds. I@10:45:50.068392spec-protocol> State 1: state invariant 20 holds. I@10:45:50.089393spec-protocol> State 1: state invariant 21 holds. I@10:45:50.122394spec-protocol> State 1: state invariant 23 holds. I@10:45:50.138395spec-protocol> State 1: state invariant 24 holds. I@10:45:50.144396spec-protocol> State 1: state invariant 26 holds. I@10:45:50.158397spec-protocol> State 1: state invariant 27 holds. I@10:45:50.177398spec-protocol> State 1: state invariant 28 holds. I@10:45:50.283399spec-protocol> State 1: state invariant 29 holds. I@10:45:50.306400spec-protocol> State 1: state invariant 30 holds. I@10:45:51.088401spec-protocol> State 1: state invariant 31 holds. I@10:45:51.687402spec-protocol> State 1: state invariant 32 holds. I@10:45:52.039403spec-protocol> State 1: Checking 26 state invariants I@10:45:53.220404spec-protocol> State 1: state invariant 0 holds. I@10:45:53.237405spec-protocol> State 1: state invariant 1 holds. I@10:45:53.319406spec-protocol> State 1: state invariant 9 holds. I@10:45:53.471407spec-protocol> State 1: state invariant 10 holds. I@10:45:53.478408spec-protocol> State 1: state invariant 12 holds. I@10:45:53.497409spec-protocol> State 1: state invariant 14 holds. I@10:45:53.530410spec-protocol> State 1: state invariant 15 holds. I@10:45:53.736411spec-protocol> State 1: state invariant 16 holds. I@10:45:53.753412spec-protocol> State 1: state invariant 17 holds. I@10:45:53.768413spec-protocol> State 1: state invariant 18 holds. I@10:45:53.881414spec-protocol> State 1: state invariant 19 holds. I@10:45:53.973415spec-protocol> State 1: state invariant 20 holds. I@10:45:54.014416spec-protocol> State 1: state invariant 21 holds. I@10:45:54.066417spec-protocol> State 1: state invariant 22 holds. I@10:45:54.105418spec-protocol> State 1: state invariant 23 holds. I@10:45:54.123419spec-protocol> State 1: state invariant 24 holds. I@10:45:54.137420spec-protocol> State 1: state invariant 26 holds. I@10:45:54.210421spec-protocol> State 1: state invariant 27 holds. I@10:45:54.234422spec-protocol> State 1: state invariant 28 holds. I@10:45:54.296423spec-protocol> State 1: state invariant 29 holds. I@10:45:54.311424spec-protocol> State 1: state invariant 30 holds. I@10:45:55.700425spec-protocol> State 1: state invariant 31 holds. I@10:45:56.259426spec-protocol> State 1: state invariant 32 holds. I@10:45:56.979427spec-protocol> State 1: state invariant 33 holds. I@10:45:57.027428spec-protocol> State 1: state invariant 34 holds. I@10:45:57.046429spec-protocol> State 1: state invariant 35 holds. I@10:45:57.082430spec-protocol> State 1: Checking 22 state invariants I@10:45:57.843431spec-protocol> State 1: state invariant 0 holds. I@10:45:57.847432spec-protocol> State 1: state invariant 1 holds. I@10:45:57.897433spec-protocol> State 1: state invariant 9 holds. I@10:45:57.916434spec-protocol> State 1: state invariant 10 holds. I@10:45:57.921435spec-protocol> State 1: state invariant 12 holds. I@10:45:57.942436spec-protocol> State 1: state invariant 14 holds. I@10:45:57.959437spec-protocol> State 1: state invariant 15 holds. I@10:45:57.983438spec-protocol> State 1: state invariant 16 holds. I@10:45:57.988439spec-protocol> State 1: state invariant 17 holds. I@10:45:58.000440spec-protocol> State 1: state invariant 18 holds. I@10:45:58.057441spec-protocol> State 1: state invariant 19 holds. I@10:45:58.155442spec-protocol> State 1: state invariant 20 holds. I@10:45:58.220443spec-protocol> State 1: state invariant 21 holds. I@10:45:58.293444spec-protocol> State 1: state invariant 23 holds. I@10:45:58.314445spec-protocol> State 1: state invariant 24 holds. I@10:45:58.321446spec-protocol> State 1: state invariant 26 holds. I@10:45:58.336447spec-protocol> State 1: state invariant 27 holds. I@10:45:58.392448spec-protocol> State 1: state invariant 28 holds. I@10:45:58.486449spec-protocol> State 1: state invariant 29 holds. I@10:45:58.517450spec-protocol> State 1: state invariant 30 holds. I@10:45:59.064451spec-protocol> State 1: state invariant 31 holds. I@10:45:59.344452spec-protocol> State 1: state invariant 32 holds. I@10:45:59.712453spec-protocol> Step 1: Transition #16 is disabled I@10:45:59.859454spec-protocol> State 1: Checking 21 state invariants I@10:46:00.204455spec-protocol> State 1: state invariant 0 holds. I@10:46:00.208456spec-protocol> State 1: state invariant 1 holds. I@10:46:00.314457spec-protocol> State 1: state invariant 9 holds. I@10:46:00.349458spec-protocol> State 1: state invariant 10 holds. I@10:46:00.369459spec-protocol> State 1: state invariant 12 holds. I@10:46:00.406460spec-protocol> State 1: state invariant 14 holds. I@10:46:00.425461spec-protocol> State 1: state invariant 15 holds. I@10:46:00.504462spec-protocol> State 1: state invariant 17 holds. I@10:46:00.510463spec-protocol> State 1: state invariant 18 holds. I@10:46:00.586464spec-protocol> State 1: state invariant 19 holds. I@10:46:00.957465spec-protocol> State 1: state invariant 20 holds. I@10:46:01.232466spec-protocol> State 1: state invariant 21 holds. I@10:46:01.696467spec-protocol> State 1: state invariant 23 holds. I@10:46:01.711468spec-protocol> State 1: state invariant 24 holds. I@10:46:01.718469spec-protocol> State 1: state invariant 26 holds. I@10:46:01.727470spec-protocol> State 1: state invariant 27 holds. I@10:46:01.765471spec-protocol> State 1: state invariant 28 holds. I@10:46:01.868472spec-protocol> State 1: state invariant 29 holds. I@10:46:01.884473spec-protocol> State 1: state invariant 30 holds. I@10:46:02.907474spec-protocol> State 1: state invariant 31 holds. I@10:46:03.713475spec-protocol> State 1: state invariant 32 holds. I@10:46:04.702476spec-protocol> Step 1: Transition #18 is disabled I@10:46:04.796477spec-protocol> State 1: Checking 21 state invariants I@10:46:05.079478spec-protocol> State 1: state invariant 0 holds. I@10:46:05.093479spec-protocol> State 1: state invariant 1 holds. I@10:46:05.210480spec-protocol> State 1: state invariant 9 holds. I@10:46:05.316481spec-protocol> State 1: state invariant 10 holds. I@10:46:05.341482spec-protocol> State 1: state invariant 12 holds. I@10:46:05.383483spec-protocol> State 1: state invariant 14 holds. I@10:46:05.457484spec-protocol> State 1: state invariant 15 holds. I@10:46:05.514485spec-protocol> State 1: state invariant 17 holds. I@10:46:05.557486spec-protocol> State 1: state invariant 18 holds. I@10:46:05.591487spec-protocol> State 1: state invariant 19 holds. I@10:46:05.616488spec-protocol> State 1: state invariant 20 holds. I@10:46:05.642489spec-protocol> State 1: state invariant 21 holds. I@10:46:05.701490spec-protocol> State 1: state invariant 23 holds. I@10:46:05.726491spec-protocol> State 1: state invariant 24 holds. I@10:46:05.735492spec-protocol> State 1: state invariant 26 holds. I@10:46:05.745493spec-protocol> State 1: state invariant 27 holds. I@10:46:05.821494spec-protocol> State 1: state invariant 28 holds. I@10:46:05.970495spec-protocol> State 1: state invariant 29 holds. I@10:46:05.986496spec-protocol> State 1: state invariant 30 holds. I@10:46:09.534497spec-protocol> State 1: state invariant 31 holds. I@10:46:11.863498spec-protocol> State 1: state invariant 32 holds. I@10:46:13.077499spec-protocol> Step 1: Transition #20 is disabled I@10:46:13.170500spec-protocol> Step 1: Transition #21 is disabled I@10:46:13.371501spec-protocol> State 1: Checking 14 state invariants I@10:46:13.912502spec-protocol> State 1: state invariant 6 holds. I@10:46:13.916503spec-protocol> State 1: state invariant 7 holds. I@10:46:13.926504spec-protocol> State 1: state invariant 22 holds. I@10:46:13.969505spec-protocol> State 1: state invariant 25 holds. I@10:46:13.974506spec-protocol> State 1: state invariant 27 holds. I@10:46:14.036507spec-protocol> State 1: state invariant 28 holds. I@10:46:14.165508spec-protocol> State 1: state invariant 29 holds. I@10:46:14.178509spec-protocol> State 1: state invariant 30 holds. I@10:46:15.284510spec-protocol> State 1: state invariant 31 holds. I@10:46:15.760