this derivation will be built: /nix/store/dya24l1lmm138d3b1826q2h2fhp5vrh2-spec-protocol.drv these 4 paths will be fetched (568.0 MiB download, 852.7 MiB unpacked): /nix/store/ij5q131fzyqw8wh76y9nrj5jl45zviqw-openjdk-21.0.12+8 /nix/store/s90yin0j1q75gr8iyr11qxqzbjdssv25-quint-0.32.0 /nix/store/mx71fx62163cbid5nc6k7vvcmpg8r609-quint-cli-0.32.0 /nix/store/ma9wr3rh0rr0plzz5dmh87dxk734n7hk-set-java-classpath-hook building '/nix/store/dya24l1lmm138d3b1826q2h2fhp5vrh2-spec-protocol.drv' spec-protocol> > [1/3] Checking whether the inductive invariant 'indInv' holds in the initial state(s) defined by 'init'... spec-protocol> # Usage statistics is OFF. We care about your privacy. spec-protocol> # If you want to help our project, consider enabling statistics with config --enable-stats=true. spec-protocol> spec-protocol> Output directory: /build/_apalache-out/server/2026-09-01T10-45-10_10572760993453108643 spec-protocol> # APALACHE version: 0.56.1 | build: 70cdaf4 I@10:45:10.363 spec-protocol> Starting checker server on port 8822... I@10:45:10.400 spec-protocol> The Apalache server is running on port 8822. Press Ctrl-C to stop. spec-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.298 spec-protocol> Sep 01, 2026 10:45:16 AM com.google.protobuf.GeneratedMessage warnPre22Gencode spec-protocol> WARNING: Vulnerable protobuf generated type in use: io.grpc.reflection.v1alpha.ServerReflectionRequest spec-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-j3g2 spec-protocol> PASS #0: SanyParser I@10:45:17.340 spec-protocol> PASS #1: TypeCheckerSnowcat I@10:45:18.464 spec-protocol> > Running Snowcat .::. I@10:45:18.464 spec-protocol> > Your types are purrfect! I@10:45:24.515 spec-protocol> > All expressions are typed I@10:45:24.515 spec-protocol> PASS #2: ConfigurationPass I@10:45:24.517 spec-protocol> > Set the initialization predicate to q::init I@10:45:24.523 spec-protocol> > Set the transition predicate to q::step I@10:45:24.524 spec-protocol> > Set an invariant to q::inductiveInv I@10:45:24.524 spec-protocol> PASS #3: DesugarerPass I@10:45:24.534 spec-protocol> > Desugaring... I@10:45:24.534 spec-protocol> PASS #4: InlinePass I@10:45:24.561 spec-protocol> Leaving only relevant operators: CInitPrimed, q::inductiveInv, q::init, q::initPrimed, q::step I@10:45:24.561 spec-protocol> PASS #5: TemporalPass I@10:45:24.729 spec-protocol> > Rewriting temporal operators... I@10:45:24.729 spec-protocol> > No temporal property specified, nothing to encode I@10:45:24.729 spec-protocol> PASS #6: InlinePass I@10:45:24.732 spec-protocol> Leaving only relevant operators: CInitPrimed, q::inductiveInv, q::init, q::initPrimed, q::step I@10:45:24.732 spec-protocol> PASS #7: PrimingPass I@10:45:24.778 spec-protocol> > Introducing q::initPrimed for q::init' I@10:45:24.781 spec-protocol> PASS #8: VCGen I@10:45:24.783 spec-protocol> > Producing verification conditions from the invariant q::inductiveInv I@10:45:24.784 spec-protocol> > VCGen produced 39 verification condition(s) I@10:45:24.794 spec-protocol> PASS #9: PreprocessingPass I@10:45:24.800 spec-protocol> > Before preprocessing: unique renaming I@10:45:24.800 spec-protocol> > Applying standard transformations: I@10:45:24.807 spec-protocol> > PrimePropagation I@10:45:24.807 spec-protocol> > Desugarer I@10:45:24.821 spec-protocol> > UniqueRenamer I@10:45:24.839 spec-protocol> > Normalizer I@10:45:24.895 spec-protocol> > Keramelizer I@10:45:24.931 spec-protocol> > After preprocessing: UniqueRenamer I@10:45:24.983 spec-protocol> PASS #10: TransitionFinderPass I@10:45:25.033 spec-protocol> > Found 1 initializing transitions I@10:45:25.045 spec-protocol> > Found 24 transitions I@10:45:25.094 spec-protocol> > No constant initializer I@10:45:25.095 spec-protocol> > Applying unique renaming I@10:45:25.096 spec-protocol> PASS #11: OptimizationPass I@10:45:25.141 spec-protocol> > Applying optimizations: I@10:45:25.148 spec-protocol> > ConstSimplifier I@10:45:25.149 spec-protocol> > ExprOptimizer I@10:45:25.229 spec-protocol> > SetMembershipSimplifier I@10:45:25.259 spec-protocol> > ConstSimplifier I@10:45:25.270 spec-protocol> PASS #12: AnalysisPass I@10:45:25.345 spec-protocol> > Marking skolemizable existentials and sets to be expanded... I@10:45:25.347 spec-protocol> > Skolemization I@10:45:25.348 spec-protocol> > Expansion I@10:45:25.358 spec-protocol> > Remove unused let-in defs I@10:45:25.386 spec-protocol> > Running analyzers... I@10:45:25.405 spec-protocol> > Introduced expression grades I@10:45:25.417 spec-protocol> PASS #13: BoundedChecker I@10:45:25.418 spec-protocol> State 0: Checking 39 state invariants I@10:45:25.888 spec-protocol> State 0: state invariant 0 holds. I@10:45:25.892 spec-protocol> State 0: state invariant 1 holds. I@10:45:25.965 spec-protocol> State 0: state invariant 2 holds. I@10:45:25.966 spec-protocol> State 0: state invariant 3 holds. I@10:45:25.969 spec-protocol> State 0: state invariant 4 holds. I@10:45:26.008 spec-protocol> State 0: state invariant 5 holds. I@10:45:26.027 spec-protocol> State 0: state invariant 6 holds. I@10:45:26.031 spec-protocol> State 0: state invariant 7 holds. I@10:45:26.032 spec-protocol> State 0: state invariant 8 holds. I@10:45:26.035 spec-protocol> State 0: state invariant 9 holds. I@10:45:26.052 spec-protocol> State 0: state invariant 10 holds. I@10:45:26.055 spec-protocol> State 0: state invariant 11 holds. I@10:45:26.056 spec-protocol> State 0: state invariant 12 holds. I@10:45:26.091 spec-protocol> State 0: state invariant 13 holds. I@10:45:26.095 spec-protocol> State 0: state invariant 14 holds. I@10:45:26.109 spec-protocol> State 0: state invariant 15 holds. I@10:45:26.116 spec-protocol> State 0: state invariant 16 holds. I@10:45:26.119 spec-protocol> State 0: state invariant 17 holds. I@10:45:26.120 spec-protocol> State 0: state invariant 18 holds. I@10:45:26.126 spec-protocol> State 0: state invariant 19 holds. I@10:45:26.131 spec-protocol> State 0: state invariant 20 holds. I@10:45:26.156 spec-protocol> State 0: state invariant 21 holds. I@10:45:26.182 spec-protocol> State 0: state invariant 22 holds. I@10:45:26.187 spec-protocol> State 0: state invariant 23 holds. I@10:45:26.218 spec-protocol> State 0: state invariant 24 holds. I@10:45:26.223 spec-protocol> State 0: state invariant 25 holds. I@10:45:26.224 spec-protocol> State 0: state invariant 26 holds. I@10:45:26.238 spec-protocol> State 0: state invariant 27 holds. I@10:45:26.250 spec-protocol> State 0: state invariant 28 holds. I@10:45:26.275 spec-protocol> State 0: state invariant 29 holds. I@10:45:26.287 spec-protocol> State 0: state invariant 30 holds. I@10:45:26.316 spec-protocol> State 0: state invariant 31 holds. I@10:45:26.369 spec-protocol> State 0: state invariant 32 holds. I@10:45:26.411 spec-protocol> State 0: state invariant 33 holds. I@10:45:26.412 spec-protocol> State 0: state invariant 34 holds. I@10:45:26.418 spec-protocol> State 0: state invariant 35 holds. I@10:45:26.423 spec-protocol> State 0: state invariant 36 holds. I@10:45:26.425 spec-protocol> State 0: state invariant 37 holds. I@10:45:26.426 spec-protocol> State 0: state invariant 38 holds. I@10:45:26.427 spec-protocol> Step 0: picking a transition out of 1 transition(s) I@10:45:26.427 spec-protocol> The outcome is: NoError I@10:45:26.437 spec-protocol> > [2/3] Checking whether 'step' preserves the inductive invariant 'indInv'... spec-protocol> PASS #0: SanyParser I@10:45:26.888 spec-protocol> PASS #1: TypeCheckerSnowcat I@10:45:27.120 spec-protocol> > Running Snowcat .::. I@10:45:27.120 spec-protocol> > Your types are purrfect! I@10:45:31.268 spec-protocol> > All expressions are typed I@10:45:31.269 spec-protocol> PASS #2: ConfigurationPass I@10:45:31.269 spec-protocol> > Set the initialization predicate to q::inductiveInv I@10:45:31.270 spec-protocol> > Set the transition predicate to q::step I@10:45:31.270 spec-protocol> > Set an invariant to q::inductiveInv I@10:45:31.270 spec-protocol> PASS #3: DesugarerPass I@10:45:31.274 spec-protocol> > Desugaring... I@10:45:31.274 spec-protocol> PASS #4: InlinePass I@10:45:31.277 spec-protocol> Leaving only relevant operators: CInitPrimed, q::inductiveInv, q::inductiveInvPrimed, q::step I@10:45:31.278 spec-protocol> PASS #5: TemporalPass I@10:45:31.349 spec-protocol> > Rewriting temporal operators... I@10:45:31.349 spec-protocol> > No temporal property specified, nothing to encode I@10:45:31.349 spec-protocol> PASS #6: InlinePass I@10:45:31.349 spec-protocol> Leaving only relevant operators: CInitPrimed, q::inductiveInv, q::inductiveInvPrimed, q::step I@10:45:31.349 spec-protocol> PASS #7: PrimingPass I@10:45:31.375 spec-protocol> > Introducing q::inductiveInvPrimed for q::inductiveInv' I@10:45:31.375 spec-protocol> PASS #8: VCGen I@10:45:31.378 spec-protocol> > Producing verification conditions from the invariant q::inductiveInv I@10:45:31.378 spec-protocol> > VCGen produced 39 verification condition(s) I@10:45:31.380 spec-protocol> PASS #9: PreprocessingPass I@10:45:31.385 spec-protocol> > Before preprocessing: unique renaming I@10:45:31.386 spec-protocol> > Applying standard transformations: I@10:45:31.386 spec-protocol> > PrimePropagation I@10:45:31.386 spec-protocol> > Desugarer I@10:45:31.392 spec-protocol> > UniqueRenamer I@10:45:31.403 spec-protocol> > Normalizer I@10:45:31.432 spec-protocol> > Keramelizer I@10:45:31.465 spec-protocol> > After preprocessing: UniqueRenamer I@10:45:31.501 spec-protocol> PASS #10: TransitionFinderPass I@10:45:31.543 spec-protocol> > Found 1 initializing transitions I@10:45:31.549 spec-protocol> > Found 24 transitions I@10:45:31.575 spec-protocol> > No constant initializer I@10:45:31.575 spec-protocol> > Applying unique renaming I@10:45:31.576 spec-protocol> PASS #11: OptimizationPass I@10:45:31.624 spec-protocol> > Applying optimizations: I@10:45:31.624 spec-protocol> > ConstSimplifier I@10:45:31.624 spec-protocol> > ExprOptimizer I@10:45:31.757 spec-protocol> > SetMembershipSimplifier I@10:45:31.814 spec-protocol> > ConstSimplifier I@10:45:31.825 spec-protocol> PASS #12: AnalysisPass I@10:45:31.937 spec-protocol> > Marking skolemizable existentials and sets to be expanded... I@10:45:31.937 spec-protocol> > Skolemization I@10:45:31.937 spec-protocol> > Expansion I@10:45:31.946 spec-protocol> > Remove unused let-in defs I@10:45:31.990 spec-protocol> > Running analyzers... I@10:45:32.001 spec-protocol> > Introduced expression grades I@10:45:32.007 spec-protocol> PASS #13: BoundedChecker I@10:45:32.007 spec-protocol> State 0: Checking 39 state invariants I@10:45:33.226 spec-protocol> State 0: state invariant 0 holds. I@10:45:33.227 spec-protocol> State 0: state invariant 1 holds. I@10:45:33.261 spec-protocol> State 0: state invariant 2 holds. I@10:45:33.265 spec-protocol> State 0: state invariant 3 holds. I@10:45:33.268 spec-protocol> State 0: state invariant 4 holds. I@10:45:33.300 spec-protocol> State 0: state invariant 5 holds. I@10:45:33.321 spec-protocol> State 0: state invariant 6 holds. I@10:45:33.324 spec-protocol> State 0: state invariant 7 holds. I@10:45:33.325 spec-protocol> State 0: state invariant 8 holds. I@10:45:33.327 spec-protocol> State 0: state invariant 9 holds. I@10:45:33.330 spec-protocol> State 0: state invariant 10 holds. I@10:45:33.333 spec-protocol> State 0: state invariant 11 holds. I@10:45:33.335 spec-protocol> State 0: state invariant 12 holds. I@10:45:33.348 spec-protocol> State 0: state invariant 13 holds. I@10:45:33.352 spec-protocol> State 0: state invariant 14 holds. I@10:45:33.367 spec-protocol> State 0: state invariant 15 holds. I@10:45:33.370 spec-protocol> State 0: state invariant 16 holds. I@10:45:33.372 spec-protocol> State 0: state invariant 17 holds. I@10:45:33.374 spec-protocol> State 0: state invariant 18 holds. I@10:45:33.385 spec-protocol> State 0: state invariant 19 holds. I@10:45:33.396 spec-protocol> State 0: state invariant 20 holds. I@10:45:33.409 spec-protocol> State 0: state invariant 21 holds. I@10:45:33.434 spec-protocol> State 0: state invariant 22 holds. I@10:45:33.456 spec-protocol> State 0: state invariant 23 holds. I@10:45:33.470 spec-protocol> State 0: state invariant 24 holds. I@10:45:33.472 spec-protocol> State 0: state invariant 25 holds. I@10:45:33.473 spec-protocol> State 0: state invariant 26 holds. I@10:45:33.476 spec-protocol> State 0: state invariant 27 holds. I@10:45:33.484 spec-protocol> State 0: state invariant 28 holds. I@10:45:33.545 spec-protocol> State 0: state invariant 29 holds. I@10:45:33.559 spec-protocol> State 0: state invariant 30 holds. I@10:45:33.773 spec-protocol> State 0: state invariant 31 holds. I@10:45:33.969 spec-protocol> State 0: state invariant 32 holds. I@10:45:34.205 spec-protocol> State 0: state invariant 33 holds. I@10:45:34.209 spec-protocol> State 0: state invariant 34 holds. I@10:45:34.217 spec-protocol> State 0: state invariant 35 holds. I@10:45:34.226 spec-protocol> State 0: state invariant 36 holds. I@10:45:34.228 spec-protocol> State 0: state invariant 37 holds. I@10:45:34.231 spec-protocol> State 0: state invariant 38 holds. I@10:45:34.233 spec-protocol> Step 0: picking a transition out of 1 transition(s) I@10:45:34.234 spec-protocol> State 1: Checking 12 state invariants I@10:45:34.272 spec-protocol> State 1: state invariant 0 holds. I@10:45:34.274 spec-protocol> State 1: state invariant 1 holds. I@10:45:34.311 spec-protocol> State 1: state invariant 18 holds. I@10:45:34.324 spec-protocol> State 1: state invariant 19 holds. I@10:45:34.333 spec-protocol> State 1: state invariant 20 holds. I@10:45:34.345 spec-protocol> State 1: state invariant 21 holds. I@10:45:34.359 spec-protocol> State 1: state invariant 27 holds. I@10:45:34.374 spec-protocol> State 1: state invariant 28 holds. I@10:45:34.413 spec-protocol> State 1: state invariant 29 holds. I@10:45:34.422 spec-protocol> State 1: state invariant 30 holds. I@10:45:34.631 spec-protocol> State 1: state invariant 31 holds. I@10:45:34.848 spec-protocol> State 1: state invariant 32 holds. I@10:45:35.115 spec-protocol> State 1: Checking 4 state invariants I@10:45:35.217 spec-protocol> State 1: state invariant 13 holds. I@10:45:35.220 spec-protocol> State 1: state invariant 29 holds. I@10:45:35.230 spec-protocol> State 1: state invariant 30 holds. I@10:45:35.640 spec-protocol> State 1: state invariant 31 holds. I@10:45:35.952 spec-protocol> State 1: Checking 16 state invariants I@10:45:36.126 spec-protocol> State 1: state invariant 0 holds. I@10:45:36.130 spec-protocol> State 1: state invariant 1 holds. I@10:45:36.171 spec-protocol> State 1: state invariant 3 holds. I@10:45:36.179 spec-protocol> State 1: state invariant 4 holds. I@10:45:36.225 spec-protocol> State 1: state invariant 5 holds. I@10:45:36.241 spec-protocol> State 1: state invariant 18 holds. I@10:45:36.252 spec-protocol> State 1: state invariant 19 holds. I@10:45:36.263 spec-protocol> State 1: state invariant 20 holds. I@10:45:36.275 spec-protocol> State 1: state invariant 21 holds. I@10:45:36.289 spec-protocol> State 1: state invariant 23 holds. I@10:45:36.305 spec-protocol> State 1: state invariant 27 holds. I@10:45:36.312 spec-protocol> State 1: state invariant 28 holds. I@10:45:36.340 spec-protocol> State 1: state invariant 29 holds. I@10:45:36.348 spec-protocol> State 1: state invariant 30 holds. I@10:45:36.463 spec-protocol> State 1: state invariant 31 holds. I@10:45:36.593 spec-protocol> State 1: state invariant 32 holds. I@10:45:36.805 spec-protocol> State 1: Checking 6 state invariants I@10:45:36.824 spec-protocol> State 1: state invariant 2 holds. I@10:45:36.826 spec-protocol> State 1: state invariant 27 holds. I@10:45:36.839 spec-protocol> State 1: state invariant 29 holds. I@10:45:36.846 spec-protocol> State 1: state invariant 30 holds. I@10:45:37.026 spec-protocol> State 1: state invariant 31 holds. I@10:45:37.177 spec-protocol> State 1: state invariant 38 holds. I@10:45:37.181 spec-protocol> State 1: Checking 15 state invariants I@10:45:37.204 spec-protocol> State 1: state invariant 0 holds. I@10:45:37.205 spec-protocol> State 1: state invariant 1 holds. I@10:45:37.237 spec-protocol> State 1: state invariant 2 holds. I@10:45:37.239 spec-protocol> State 1: state invariant 12 holds. I@10:45:37.252 spec-protocol> State 1: state invariant 18 holds. I@10:45:37.266 spec-protocol> State 1: state invariant 19 holds. I@10:45:37.275 spec-protocol> State 1: state invariant 20 holds. I@10:45:37.289 spec-protocol> State 1: state invariant 21 holds. I@10:45:37.307 spec-protocol> State 1: state invariant 27 holds. I@10:45:37.321 spec-protocol> State 1: state invariant 28 holds. I@10:45:37.364 spec-protocol> State 1: state invariant 29 holds. I@10:45:37.373 spec-protocol> State 1: state invariant 30 holds. I@10:45:37.575 spec-protocol> State 1: state invariant 31 holds. I@10:45:37.753 spec-protocol> State 1: state invariant 32 holds. I@10:45:37.920 spec-protocol> State 1: state invariant 37 holds. I@10:45:37.923 spec-protocol> State 1: Checking 18 state invariants I@10:45:38.202 spec-protocol> State 1: state invariant 9 holds. I@10:45:38.209 spec-protocol> State 1: state invariant 10 holds. I@10:45:38.211 spec-protocol> State 1: state invariant 11 holds. I@10:45:38.213 spec-protocol> State 1: state invariant 14 holds. I@10:45:38.223 spec-protocol> State 1: state invariant 15 holds. I@10:45:38.226 spec-protocol> State 1: state invariant 17 holds. I@10:45:38.228 spec-protocol> State 1: state invariant 22 holds. I@10:45:38.239 spec-protocol> State 1: state invariant 24 holds. I@10:45:38.242 spec-protocol> State 1: state invariant 26 holds. I@10:45:38.246 spec-protocol> State 1: state invariant 27 holds. I@10:45:38.258 spec-protocol> State 1: state invariant 28 holds. I@10:45:38.292 spec-protocol> State 1: state invariant 29 holds. I@10:45:38.303 spec-protocol> State 1: state invariant 30 holds. I@10:45:38.386 spec-protocol> State 1: state invariant 31 holds. I@10:45:38.490 spec-protocol> State 1: state invariant 32 holds. I@10:45:38.668 spec-protocol> State 1: state invariant 33 holds. I@10:45:38.676 spec-protocol> State 1: state invariant 34 holds. I@10:45:38.684 spec-protocol> State 1: state invariant 35 holds. I@10:45:38.704 spec-protocol> State 1: Checking 14 state invariants I@10:45:39.277 spec-protocol> State 1: state invariant 9 holds. I@10:45:39.287 spec-protocol> State 1: state invariant 10 holds. I@10:45:39.291 spec-protocol> State 1: state invariant 11 holds. I@10:45:39.294 spec-protocol> State 1: state invariant 14 holds. I@10:45:39.319 spec-protocol> State 1: state invariant 15 holds. I@10:45:39.333 spec-protocol> State 1: state invariant 17 holds. I@10:45:39.340 spec-protocol> State 1: state invariant 24 holds. I@10:45:39.350 spec-protocol> State 1: state invariant 26 holds. I@10:45:39.362 spec-protocol> State 1: state invariant 27 holds. I@10:45:39.387 spec-protocol> State 1: state invariant 28 holds. I@10:45:39.442 spec-protocol> State 1: state invariant 29 holds. I@10:45:39.467 spec-protocol> State 1: state invariant 30 holds. I@10:45:39.658 spec-protocol> State 1: state invariant 31 holds. I@10:45:39.921 spec-protocol> State 1: state invariant 32 holds. I@10:45:40.035 spec-protocol> State 1: Checking 26 state invariants I@10:45:40.334 spec-protocol> State 1: state invariant 0 holds. I@10:45:40.338 spec-protocol> State 1: state invariant 1 holds. I@10:45:40.387 spec-protocol> State 1: state invariant 9 holds. I@10:45:40.404 spec-protocol> State 1: state invariant 10 holds. I@10:45:40.408 spec-protocol> State 1: state invariant 11 holds. I@10:45:40.413 spec-protocol> State 1: state invariant 12 holds. I@10:45:40.429 spec-protocol> State 1: state invariant 14 holds. I@10:45:40.450 spec-protocol> State 1: state invariant 15 holds. I@10:45:40.481 spec-protocol> State 1: state invariant 17 holds. I@10:45:40.487 spec-protocol> State 1: state invariant 18 holds. I@10:45:40.534 spec-protocol> State 1: state invariant 19 holds. I@10:45:40.548 spec-protocol> State 1: state invariant 20 holds. I@10:45:40.569 spec-protocol> State 1: state invariant 21 holds. I@10:45:40.605 spec-protocol> State 1: state invariant 22 holds. I@10:45:40.627 spec-protocol> State 1: state invariant 23 holds. I@10:45:40.641 spec-protocol> State 1: state invariant 24 holds. I@10:45:40.646 spec-protocol> State 1: state invariant 26 holds. I@10:45:40.657 spec-protocol> State 1: state invariant 27 holds. I@10:45:40.699 spec-protocol> State 1: state invariant 28 holds. I@10:45:40.810 spec-protocol> State 1: state invariant 29 holds. I@10:45:40.824 spec-protocol> State 1: state invariant 30 holds. I@10:45:41.384 spec-protocol> State 1: state invariant 31 holds. I@10:45:42.104 spec-protocol> State 1: state invariant 32 holds. I@10:45:42.589 spec-protocol> State 1: state invariant 33 holds. I@10:45:42.597 spec-protocol> State 1: state invariant 34 holds. I@10:45:42.612 spec-protocol> State 1: state invariant 35 holds. I@10:45:42.640 spec-protocol> State 1: Checking 22 state invariants I@10:45:43.039 spec-protocol> State 1: state invariant 0 holds. I@10:45:43.043 spec-protocol> State 1: state invariant 1 holds. I@10:45:43.135 spec-protocol> State 1: state invariant 9 holds. I@10:45:43.171 spec-protocol> State 1: state invariant 10 holds. I@10:45:43.183 spec-protocol> State 1: state invariant 11 holds. I@10:45:43.195 spec-protocol> State 1: state invariant 12 holds. I@10:45:43.228 spec-protocol> State 1: state invariant 14 holds. I@10:45:43.277 spec-protocol> State 1: state invariant 15 holds. I@10:45:43.348 spec-protocol> State 1: state invariant 17 holds. I@10:45:43.360 spec-protocol> State 1: state invariant 18 holds. I@10:45:43.416 spec-protocol> State 1: state invariant 19 holds. I@10:45:43.583 spec-protocol> State 1: state invariant 20 holds. I@10:45:43.643 spec-protocol> State 1: state invariant 21 holds. I@10:45:43.677 spec-protocol> State 1: state invariant 23 holds. I@10:45:43.696 spec-protocol> State 1: state invariant 24 holds. I@10:45:43.708 spec-protocol> State 1: state invariant 26 holds. I@10:45:43.753 spec-protocol> State 1: state invariant 27 holds. I@10:45:43.806 spec-protocol> State 1: state invariant 28 holds. I@10:45:43.977 spec-protocol> State 1: state invariant 29 holds. I@10:45:43.993 spec-protocol> State 1: state invariant 30 holds. I@10:45:44.967 spec-protocol> State 1: state invariant 31 holds. I@10:45:45.628 spec-protocol> State 1: state invariant 32 holds. I@10:45:46.066 spec-protocol> Step 1: Transition #10 is disabled I@10:45:46.130 spec-protocol> Step 1: Transition #11 is disabled I@10:45:46.191 spec-protocol> State 1: Checking 27 state invariants I@10:45:46.702 spec-protocol> State 1: state invariant 0 holds. I@10:45:46.713 spec-protocol> State 1: state invariant 1 holds. I@10:45:46.840 spec-protocol> State 1: state invariant 9 holds. I@10:45:46.901 spec-protocol> State 1: state invariant 10 holds. I@10:45:46.910 spec-protocol> State 1: state invariant 12 holds. I@10:45:46.944 spec-protocol> State 1: state invariant 13 holds. I@10:45:46.961 spec-protocol> State 1: state invariant 14 holds. I@10:45:47.014 spec-protocol> State 1: state invariant 15 holds. I@10:45:47.108 spec-protocol> State 1: state invariant 16 holds. I@10:45:47.115 spec-protocol> State 1: state invariant 17 holds. I@10:45:47.120 spec-protocol> State 1: state invariant 18 holds. I@10:45:47.145 spec-protocol> State 1: state invariant 19 holds. I@10:45:47.177 spec-protocol> State 1: state invariant 20 holds. I@10:45:47.204 spec-protocol> State 1: state invariant 21 holds. I@10:45:47.234 spec-protocol> State 1: state invariant 22 holds. I@10:45:47.281 spec-protocol> State 1: state invariant 23 holds. I@10:45:47.320 spec-protocol> State 1: state invariant 24 holds. I@10:45:47.332 spec-protocol> State 1: state invariant 26 holds. I@10:45:47.346 spec-protocol> State 1: state invariant 27 holds. I@10:45:47.450 spec-protocol> State 1: state invariant 28 holds. I@10:45:47.568 spec-protocol> State 1: state invariant 29 holds. I@10:45:47.582 spec-protocol> State 1: state invariant 30 holds. I@10:45:48.436 spec-protocol> State 1: state invariant 31 holds. I@10:45:48.843 spec-protocol> State 1: state invariant 32 holds. I@10:45:49.350 spec-protocol> State 1: state invariant 33 holds. I@10:45:49.358 spec-protocol> State 1: state invariant 34 holds. I@10:45:49.376 spec-protocol> State 1: state invariant 35 holds. I@10:45:49.407 spec-protocol> State 1: Checking 23 state invariants I@10:45:49.854 spec-protocol> State 1: state invariant 0 holds. I@10:45:49.862 spec-protocol> State 1: state invariant 1 holds. I@10:45:49.911 spec-protocol> State 1: state invariant 9 holds. I@10:45:49.934 spec-protocol> State 1: state invariant 10 holds. I@10:45:49.939 spec-protocol> State 1: state invariant 12 holds. I@10:45:49.955 spec-protocol> State 1: state invariant 13 holds. I@10:45:49.962 spec-protocol> State 1: state invariant 14 holds. I@10:45:49.977 spec-protocol> State 1: state invariant 15 holds. I@10:45:49.997 spec-protocol> State 1: state invariant 16 holds. I@10:45:50.003 spec-protocol> State 1: state invariant 17 holds. I@10:45:50.008 spec-protocol> State 1: state invariant 18 holds. I@10:45:50.022 spec-protocol> State 1: state invariant 19 holds. I@10:45:50.068 spec-protocol> State 1: state invariant 20 holds. I@10:45:50.089 spec-protocol> State 1: state invariant 21 holds. I@10:45:50.122 spec-protocol> State 1: state invariant 23 holds. I@10:45:50.138 spec-protocol> State 1: state invariant 24 holds. I@10:45:50.144 spec-protocol> State 1: state invariant 26 holds. I@10:45:50.158 spec-protocol> State 1: state invariant 27 holds. I@10:45:50.177 spec-protocol> State 1: state invariant 28 holds. I@10:45:50.283 spec-protocol> State 1: state invariant 29 holds. I@10:45:50.306 spec-protocol> State 1: state invariant 30 holds. I@10:45:51.088 spec-protocol> State 1: state invariant 31 holds. I@10:45:51.687 spec-protocol> State 1: state invariant 32 holds. I@10:45:52.039 spec-protocol> State 1: Checking 26 state invariants I@10:45:53.220 spec-protocol> State 1: state invariant 0 holds. I@10:45:53.237 spec-protocol> State 1: state invariant 1 holds. I@10:45:53.319 spec-protocol> State 1: state invariant 9 holds. I@10:45:53.471 spec-protocol> State 1: state invariant 10 holds. I@10:45:53.478 spec-protocol> State 1: state invariant 12 holds. I@10:45:53.497 spec-protocol> State 1: state invariant 14 holds. I@10:45:53.530 spec-protocol> State 1: state invariant 15 holds. I@10:45:53.736 spec-protocol> State 1: state invariant 16 holds. I@10:45:53.753 spec-protocol> State 1: state invariant 17 holds. I@10:45:53.768 spec-protocol> State 1: state invariant 18 holds. I@10:45:53.881 spec-protocol> State 1: state invariant 19 holds. I@10:45:53.973 spec-protocol> State 1: state invariant 20 holds. I@10:45:54.014 spec-protocol> State 1: state invariant 21 holds. I@10:45:54.066 spec-protocol> State 1: state invariant 22 holds. I@10:45:54.105 spec-protocol> State 1: state invariant 23 holds. I@10:45:54.123 spec-protocol> State 1: state invariant 24 holds. I@10:45:54.137 spec-protocol> State 1: state invariant 26 holds. I@10:45:54.210 spec-protocol> State 1: state invariant 27 holds. I@10:45:54.234 spec-protocol> State 1: state invariant 28 holds. I@10:45:54.296 spec-protocol> State 1: state invariant 29 holds. I@10:45:54.311 spec-protocol> State 1: state invariant 30 holds. I@10:45:55.700 spec-protocol> State 1: state invariant 31 holds. I@10:45:56.259 spec-protocol> State 1: state invariant 32 holds. I@10:45:56.979 spec-protocol> State 1: state invariant 33 holds. I@10:45:57.027 spec-protocol> State 1: state invariant 34 holds. I@10:45:57.046 spec-protocol> State 1: state invariant 35 holds. I@10:45:57.082 spec-protocol> State 1: Checking 22 state invariants I@10:45:57.843 spec-protocol> State 1: state invariant 0 holds. I@10:45:57.847 spec-protocol> State 1: state invariant 1 holds. I@10:45:57.897 spec-protocol> State 1: state invariant 9 holds. I@10:45:57.916 spec-protocol> State 1: state invariant 10 holds. I@10:45:57.921 spec-protocol> State 1: state invariant 12 holds. I@10:45:57.942 spec-protocol> State 1: state invariant 14 holds. I@10:45:57.959 spec-protocol> State 1: state invariant 15 holds. I@10:45:57.983 spec-protocol> State 1: state invariant 16 holds. I@10:45:57.988 spec-protocol> State 1: state invariant 17 holds. I@10:45:58.000 spec-protocol> State 1: state invariant 18 holds. I@10:45:58.057 spec-protocol> State 1: state invariant 19 holds. I@10:45:58.155 spec-protocol> State 1: state invariant 20 holds. I@10:45:58.220 spec-protocol> State 1: state invariant 21 holds. I@10:45:58.293 spec-protocol> State 1: state invariant 23 holds. I@10:45:58.314 spec-protocol> State 1: state invariant 24 holds. I@10:45:58.321 spec-protocol> State 1: state invariant 26 holds. I@10:45:58.336 spec-protocol> State 1: state invariant 27 holds. I@10:45:58.392 spec-protocol> State 1: state invariant 28 holds. I@10:45:58.486 spec-protocol> State 1: state invariant 29 holds. I@10:45:58.517 spec-protocol> State 1: state invariant 30 holds. I@10:45:59.064 spec-protocol> State 1: state invariant 31 holds. I@10:45:59.344 spec-protocol> State 1: state invariant 32 holds. I@10:45:59.712 spec-protocol> Step 1: Transition #16 is disabled I@10:45:59.859 spec-protocol> State 1: Checking 21 state invariants I@10:46:00.204 spec-protocol> State 1: state invariant 0 holds. I@10:46:00.208 spec-protocol> State 1: state invariant 1 holds. I@10:46:00.314 spec-protocol> State 1: state invariant 9 holds. I@10:46:00.349 spec-protocol> State 1: state invariant 10 holds. I@10:46:00.369 spec-protocol> State 1: state invariant 12 holds. I@10:46:00.406 spec-protocol> State 1: state invariant 14 holds. I@10:46:00.425 spec-protocol> State 1: state invariant 15 holds. I@10:46:00.504 spec-protocol> State 1: state invariant 17 holds. I@10:46:00.510 spec-protocol> State 1: state invariant 18 holds. I@10:46:00.586 spec-protocol> State 1: state invariant 19 holds. I@10:46:00.957 spec-protocol> State 1: state invariant 20 holds. I@10:46:01.232 spec-protocol> State 1: state invariant 21 holds. I@10:46:01.696 spec-protocol> State 1: state invariant 23 holds. I@10:46:01.711 spec-protocol> State 1: state invariant 24 holds. I@10:46:01.718 spec-protocol> State 1: state invariant 26 holds. I@10:46:01.727 spec-protocol> State 1: state invariant 27 holds. I@10:46:01.765 spec-protocol> State 1: state invariant 28 holds. I@10:46:01.868 spec-protocol> State 1: state invariant 29 holds. I@10:46:01.884 spec-protocol> State 1: state invariant 30 holds. I@10:46:02.907 spec-protocol> State 1: state invariant 31 holds. I@10:46:03.713 spec-protocol> State 1: state invariant 32 holds. I@10:46:04.702 spec-protocol> Step 1: Transition #18 is disabled I@10:46:04.796 spec-protocol> State 1: Checking 21 state invariants I@10:46:05.079 spec-protocol> State 1: state invariant 0 holds. I@10:46:05.093 spec-protocol> State 1: state invariant 1 holds. I@10:46:05.210 spec-protocol> State 1: state invariant 9 holds. I@10:46:05.316 spec-protocol> State 1: state invariant 10 holds. I@10:46:05.341 spec-protocol> State 1: state invariant 12 holds. I@10:46:05.383 spec-protocol> State 1: state invariant 14 holds. I@10:46:05.457 spec-protocol> State 1: state invariant 15 holds. I@10:46:05.514 spec-protocol> State 1: state invariant 17 holds. I@10:46:05.557 spec-protocol> State 1: state invariant 18 holds. I@10:46:05.591 spec-protocol> State 1: state invariant 19 holds. I@10:46:05.616 spec-protocol> State 1: state invariant 20 holds. I@10:46:05.642 spec-protocol> State 1: state invariant 21 holds. I@10:46:05.701 spec-protocol> State 1: state invariant 23 holds. I@10:46:05.726 spec-protocol> State 1: state invariant 24 holds. I@10:46:05.735 spec-protocol> State 1: state invariant 26 holds. I@10:46:05.745 spec-protocol> State 1: state invariant 27 holds. I@10:46:05.821 spec-protocol> State 1: state invariant 28 holds. I@10:46:05.970 spec-protocol> State 1: state invariant 29 holds. I@10:46:05.986 spec-protocol> State 1: state invariant 30 holds. I@10:46:09.534 spec-protocol> State 1: state invariant 31 holds. I@10:46:11.863 spec-protocol> State 1: state invariant 32 holds. I@10:46:13.077 spec-protocol> Step 1: Transition #20 is disabled I@10:46:13.170 spec-protocol> Step 1: Transition #21 is disabled I@10:46:13.371 spec-protocol> State 1: Checking 14 state invariants I@10:46:13.912 spec-protocol> State 1: state invariant 6 holds. I@10:46:13.916 spec-protocol> State 1: state invariant 7 holds. I@10:46:13.926 spec-protocol> State 1: state invariant 22 holds. I@10:46:13.969 spec-protocol> State 1: state invariant 25 holds. I@10:46:13.974 spec-protocol> State 1: state invariant 27 holds. I@10:46:14.036 spec-protocol> State 1: state invariant 28 holds. I@10:46:14.165 spec-protocol> State 1: state invariant 29 holds. I@10:46:14.178 spec-protocol> State 1: state invariant 30 holds. I@10:46:15.284 spec-protocol> State 1: state invariant 31 holds. I@10:46:15.760