nix-grpc-store-spec
checks.x86_64-linux.spec
· build #607
· raw
1tribuchet: building on jamie2An example execution:34[State 0]5{6 schedFixed::scheduler::cl: Map("c1" -> CIdle, "c2" -> CIdle),7 schedFixed::scheduler::crashes: 0,8 schedFixed::scheduler::entry: [],9 schedFixed::scheduler::free: Map("w1" -> 1, "w2" -> 1),10 schedFixed::scheduler::mAssigned: Set(),11 schedFixed::scheduler::mBuild: Set(),12 schedFixed::scheduler::mDone: Set(),13 schedFixed::scheduler::mExpect: Set(),14 schedFixed::scheduler::mResult: Set(),15 schedFixed::scheduler::mRetry: Set(),16 schedFixed::scheduler::mRevoke: Set(),17 schedFixed::scheduler::mSchedule: Set(),18 schedFixed::scheduler::published: 0,19 schedFixed::scheduler::publishedBy: Set(),20 schedFixed::scheduler::ws:21 Map(22 "w1" ->23 {24 attached: Set(),25 built: false,26 expecting: false,27 running: false,28 session: true,29 up: true30 },31 "w2" ->32 {33 attached: Set(),34 built: false,35 expecting: false,36 running: false,37 session: true,38 up: true39 }40 )41}4243[State 1]44{45 schedFixed::scheduler::cl: Map("c1" -> CQueued, "c2" -> CIdle),46 schedFixed::scheduler::crashes: 0,47 schedFixed::scheduler::entry: [],48 schedFixed::scheduler::free: Map("w1" -> 1, "w2" -> 1),49 schedFixed::scheduler::mAssigned: Set(),50 schedFixed::scheduler::mBuild: Set(),51 schedFixed::scheduler::mDone: Set(),52 schedFixed::scheduler::mExpect: Set(),53 schedFixed::scheduler::mResult: Set(),54 schedFixed::scheduler::mRetry: Set(),55 schedFixed::scheduler::mRevoke: Set(),56 schedFixed::scheduler::mSchedule: Set("c1"),57 schedFixed::scheduler::published: 0,58 schedFixed::scheduler::publishedBy: Set(),59 schedFixed::scheduler::ws:60 Map(61 "w1" ->62 {63 attached: Set(),64 built: false,65 expecting: false,66 running: false,67 session: true,68 up: true69 },70 "w2" ->71 {72 attached: Set(),73 built: false,74 expecting: false,75 running: false,76 session: true,77 up: true78 }79 )80}8182[State 2]83{84 schedFixed::scheduler::cl: Map("c1" -> CQueued, "c2" -> CQueued),85 schedFixed::scheduler::crashes: 0,86 schedFixed::scheduler::entry: [],87 schedFixed::scheduler::free: Map("w1" -> 1, "w2" -> 1),88 schedFixed::scheduler::mAssigned: Set(),89 schedFixed::scheduler::mBuild: Set(),90 schedFixed::scheduler::mDone: Set(),91 schedFixed::scheduler::mExpect: Set(),92 schedFixed::scheduler::mResult: Set(),93 schedFixed::scheduler::mRetry: Set(),94 schedFixed::scheduler::mRevoke: Set(),95 schedFixed::scheduler::mSchedule: Set("c1", "c2"),96 schedFixed::scheduler::published: 0,97 schedFixed::scheduler::publishedBy: Set(),98 schedFixed::scheduler::ws:99 Map(100 "w1" ->101 {102 attached: Set(),103 built: false,104 expecting: false,105 running: false,106 session: true,107 up: true108 },109 "w2" ->110 {111 attached: Set(),112 built: false,113 expecting: false,114 running: false,115 session: true,116 up: true117 }118 )119}120121[State 3]122{123 schedFixed::scheduler::cl: Map("c1" -> CQueued, "c2" -> CQueued),124 schedFixed::scheduler::crashes: 0,125 schedFixed::scheduler::entry:126 [{ followers: Set("c2"), leased: true, worker: "w2" }],127 schedFixed::scheduler::free: Map("w1" -> 1, "w2" -> 0),128 schedFixed::scheduler::mAssigned: Set(("c2", "w2")),129 schedFixed::scheduler::mBuild: Set(),130 schedFixed::scheduler::mDone: Set(),131 schedFixed::scheduler::mExpect: Set("w2"),132 schedFixed::scheduler::mResult: Set(),133 schedFixed::scheduler::mRetry: Set(),134 schedFixed::scheduler::mRevoke: Set(),135 schedFixed::scheduler::mSchedule: Set("c1"),136 schedFixed::scheduler::published: 0,137 schedFixed::scheduler::publishedBy: Set(),138 schedFixed::scheduler::ws:139 Map(140 "w1" ->141 {142 attached: Set(),143 built: false,144 expecting: false,145 running: false,146 session: true,147 up: true148 },149 "w2" ->150 {151 attached: Set(),152 built: false,153 expecting: false,154 running: false,155 session: true,156 up: true157 }158 )159}160161[State 4]162{163 schedFixed::scheduler::cl: Map("c1" -> CQueued, "c2" -> CQueued),164 schedFixed::scheduler::crashes: 1,165 schedFixed::scheduler::entry:166 [{ followers: Set("c2"), leased: true, worker: "w2" }],167 schedFixed::scheduler::free: Map("w1" -> 1, "w2" -> 0),168 schedFixed::scheduler::mAssigned: Set(("c2", "w2")),169 schedFixed::scheduler::mBuild: Set(),170 schedFixed::scheduler::mDone: Set(),171 schedFixed::scheduler::mExpect: Set("w2"),172 schedFixed::scheduler::mResult: Set(),173 schedFixed::scheduler::mRetry: Set(),174 schedFixed::scheduler::mRevoke: Set(),175 schedFixed::scheduler::mSchedule: Set("c1"),176 schedFixed::scheduler::published: 0,177 schedFixed::scheduler::publishedBy: Set(),178 schedFixed::scheduler::ws:179 Map(180 "w1" ->181 {182 attached: Set(),183 built: false,184 expecting: false,185 running: false,186 session: false,187 up: false188 },189 "w2" ->190 {191 attached: Set(),192 built: false,193 expecting: false,194 running: false,195 session: true,196 up: true197 }198 )199}200201[State 5]202{203 schedFixed::scheduler::cl: Map("c1" -> CQueued, "c2" -> CQueued),204 schedFixed::scheduler::crashes: 1,205 schedFixed::scheduler::entry:206 [{ followers: Set("c2"), leased: true, worker: "w2" }],207 schedFixed::scheduler::free: Map("w1" -> 1, "w2" -> 0),208 schedFixed::scheduler::mAssigned: Set(("c2", "w2")),209 schedFixed::scheduler::mBuild: Set(),210 schedFixed::scheduler::mDone: Set(),211 schedFixed::scheduler::mExpect: Set(),212 schedFixed::scheduler::mResult: Set(),213 schedFixed::scheduler::mRetry: Set(),214 schedFixed::scheduler::mRevoke: Set(),215 schedFixed::scheduler::mSchedule: Set("c1"),216 schedFixed::scheduler::published: 0,217 schedFixed::scheduler::publishedBy: Set(),218 schedFixed::scheduler::ws:219 Map(220 "w1" ->221 {222 attached: Set(),223 built: false,224 expecting: false,225 running: false,226 session: false,227 up: false228 },229 "w2" ->230 {231 attached: Set(),232 built: false,233 expecting: true,234 running: true,235 session: true,236 up: true237 }238 )239}240241[State 6]242{243 schedFixed::scheduler::cl: Map("c1" -> CQueued, "c2" -> CQueued),244 schedFixed::scheduler::crashes: 2,245 schedFixed::scheduler::entry:246 [{ followers: Set("c2"), leased: true, worker: "w2" }],247 schedFixed::scheduler::free: Map("w1" -> 1, "w2" -> 0),248 schedFixed::scheduler::mAssigned: Set(("c2", "w2")),249 schedFixed::scheduler::mBuild: Set(),250 schedFixed::scheduler::mDone: Set(),251 schedFixed::scheduler::mExpect: Set(),252 schedFixed::scheduler::mResult: Set(),253 schedFixed::scheduler::mRetry: Set(),254 schedFixed::scheduler::mRevoke: Set(),255 schedFixed::scheduler::mSchedule: Set("c1"),256 schedFixed::scheduler::published: 0,257 schedFixed::scheduler::publishedBy: Set(),258 schedFixed::scheduler::ws:259 Map(260 "w1" ->261 {262 attached: Set(),263 built: false,264 expecting: false,265 running: false,266 session: false,267 up: false268 },269 "w2" ->270 {271 attached: Set(),272 built: false,273 expecting: false,274 running: false,275 session: false,276 up: false277 }278 )279}280281[State 7]282{283 schedFixed::scheduler::cl: Map("c1" -> CQueued, "c2" -> CQueued),284 schedFixed::scheduler::crashes: 2,285 schedFixed::scheduler::entry:286 [{ followers: Set("c1", "c2"), leased: true, worker: "w2" }],287 schedFixed::scheduler::free: Map("w1" -> 1, "w2" -> 0),288 schedFixed::scheduler::mAssigned: Set(("c1", "w2"), ("c2", "w2")),289 schedFixed::scheduler::mBuild: Set(),290 schedFixed::scheduler::mDone: Set(),291 schedFixed::scheduler::mExpect: Set(),292 schedFixed::scheduler::mResult: Set(),293 schedFixed::scheduler::mRetry: Set(),294 schedFixed::scheduler::mRevoke: Set(),295 schedFixed::scheduler::mSchedule: Set(),296 schedFixed::scheduler::published: 0,297 schedFixed::scheduler::publishedBy: Set(),298 schedFixed::scheduler::ws:299 Map(300 "w1" ->301 {302 attached: Set(),303 built: false,304 expecting: false,305 running: false,306 session: false,307 up: false308 },309 "w2" ->310 {311 attached: Set(),312 built: false,313 expecting: false,314 running: false,315 session: false,316 up: false317 }318 )319}320321[State 8]322{323 schedFixed::scheduler::cl: Map("c1" -> CQueued, "c2" -> CQueued),324 schedFixed::scheduler::crashes: 2,325 schedFixed::scheduler::entry:326 [{ followers: Set("c1", "c2"), leased: true, worker: "w2" }],327 schedFixed::scheduler::free: Map("w1" -> 1, "w2" -> 0),328 schedFixed::scheduler::mAssigned: Set(("c1", "w2"), ("c2", "w2")),329 schedFixed::scheduler::mBuild: Set(),330 schedFixed::scheduler::mDone: Set(),331 schedFixed::scheduler::mExpect: Set(),332 schedFixed::scheduler::mResult: Set(),333 schedFixed::scheduler::mRetry: Set(),334 schedFixed::scheduler::mRevoke: Set(),335 schedFixed::scheduler::mSchedule: Set(),336 schedFixed::scheduler::published: 0,337 schedFixed::scheduler::publishedBy: Set(),338 schedFixed::scheduler::ws:339 Map(340 "w1" ->341 {342 attached: Set(),343 built: false,344 expecting: false,345 running: false,346 session: true,347 up: true348 },349 "w2" ->350 {351 attached: Set(),352 built: false,353 expecting: false,354 running: false,355 session: false,356 up: false357 }358 )359}360361[State 9]362{363 schedFixed::scheduler::cl: Map("c1" -> CQueued, "c2" -> CSent("w2")),364 schedFixed::scheduler::crashes: 2,365 schedFixed::scheduler::entry:366 [{ followers: Set("c1", "c2"), leased: true, worker: "w2" }],367 schedFixed::scheduler::free: Map("w1" -> 1, "w2" -> 0),368 schedFixed::scheduler::mAssigned: Set(("c1", "w2")),369 schedFixed::scheduler::mBuild: Set(("c2", "w2")),370 schedFixed::scheduler::mDone: Set(),371 schedFixed::scheduler::mExpect: Set(),372 schedFixed::scheduler::mResult: Set(),373 schedFixed::scheduler::mRetry: Set(),374 schedFixed::scheduler::mRevoke: Set(),375 schedFixed::scheduler::mSchedule: Set(),376 schedFixed::scheduler::published: 0,377 schedFixed::scheduler::publishedBy: Set(),378 schedFixed::scheduler::ws:379 Map(380 "w1" ->381 {382 attached: Set(),383 built: false,384 expecting: false,385 running: false,386 session: true,387 up: true388 },389 "w2" ->390 {391 attached: Set(),392 built: false,393 expecting: false,394 running: false,395 session: false,396 up: false397 }398 )399}400401[State 10]402{403 schedFixed::scheduler::cl: Map("c1" -> CQueued, "c2" -> CSent("w2")),404 schedFixed::scheduler::crashes: 2,405 schedFixed::scheduler::entry: [],406 schedFixed::scheduler::free: Map("w1" -> 1, "w2" -> 1),407 schedFixed::scheduler::mAssigned: Set(("c1", "w2")),408 schedFixed::scheduler::mBuild: Set(("c2", "w2")),409 schedFixed::scheduler::mDone: Set(),410 schedFixed::scheduler::mExpect: Set(),411 schedFixed::scheduler::mResult: Set(),412 schedFixed::scheduler::mRetry: Set("c1", "c2"),413 schedFixed::scheduler::mRevoke: Set(),414 schedFixed::scheduler::mSchedule: Set(),415 schedFixed::scheduler::published: 0,416 schedFixed::scheduler::publishedBy: Set(),417 schedFixed::scheduler::ws:418 Map(419 "w1" ->420 {421 attached: Set(),422 built: false,423 expecting: false,424 running: false,425 session: true,426 up: true427 },428 "w2" ->429 {430 attached: Set(),431 built: false,432 expecting: false,433 running: false,434 session: true,435 up: true436 }437 )438}439440[State 11]441{442 schedFixed::scheduler::cl: Map("c1" -> CQueued, "c2" -> CQueued),443 schedFixed::scheduler::crashes: 2,444 schedFixed::scheduler::entry: [],445 schedFixed::scheduler::free: Map("w1" -> 1, "w2" -> 1),446 schedFixed::scheduler::mAssigned: Set(("c1", "w2")),447 schedFixed::scheduler::mBuild: Set(("c2", "w2")),448 schedFixed::scheduler::mDone: Set(),449 schedFixed::scheduler::mExpect: Set(),450 schedFixed::scheduler::mResult: Set(),451 schedFixed::scheduler::mRetry: Set("c1"),452 schedFixed::scheduler::mRevoke: Set(),453 schedFixed::scheduler::mSchedule: Set("c2"),454 schedFixed::scheduler::published: 0,455 schedFixed::scheduler::publishedBy: Set(),456 schedFixed::scheduler::ws:457 Map(458 "w1" ->459 {460 attached: Set(),461 built: false,462 expecting: false,463 running: false,464 session: true,465 up: true466 },467 "w2" ->468 {469 attached: Set(),470 built: false,471 expecting: false,472 running: false,473 session: true,474 up: true475 }476 )477}478479[State 12]480{481 schedFixed::scheduler::cl: Map("c1" -> CSent("w2"), "c2" -> CQueued),482 schedFixed::scheduler::crashes: 2,483 schedFixed::scheduler::entry: [],484 schedFixed::scheduler::free: Map("w1" -> 1, "w2" -> 1),485 schedFixed::scheduler::mAssigned: Set(),486 schedFixed::scheduler::mBuild: Set(("c1", "w2"), ("c2", "w2")),487 schedFixed::scheduler::mDone: Set(),488 schedFixed::scheduler::mExpect: Set(),489 schedFixed::scheduler::mResult: Set(),490 schedFixed::scheduler::mRetry: Set("c1"),491 schedFixed::scheduler::mRevoke: Set(),492 schedFixed::scheduler::mSchedule: Set("c2"),493 schedFixed::scheduler::published: 0,494 schedFixed::scheduler::publishedBy: Set(),495 schedFixed::scheduler::ws:496 Map(497 "w1" ->498 {499 attached: Set(),500 built: false,501 expecting: false,502 running: false,503 session: true,504 up: true505 },506 "w2" ->507 {508 attached: Set(),509 built: false,510 expecting: false,511 running: false,512 session: true,513 up: true514 }515 )516}517518[State 13]519{520 schedFixed::scheduler::cl: Map("c1" -> CSent("w2"), "c2" -> CQueued),521 schedFixed::scheduler::crashes: 2,522 schedFixed::scheduler::entry:523 [{ followers: Set("c2"), leased: true, worker: "w1" }],524 schedFixed::scheduler::free: Map("w1" -> 0, "w2" -> 1),525 schedFixed::scheduler::mAssigned: Set(("c2", "w1")),526 schedFixed::scheduler::mBuild: Set(("c1", "w2"), ("c2", "w2")),527 schedFixed::scheduler::mDone: Set(),528 schedFixed::scheduler::mExpect: Set("w1"),529 schedFixed::scheduler::mResult: Set(),530 schedFixed::scheduler::mRetry: Set("c1"),531 schedFixed::scheduler::mRevoke: Set(),532 schedFixed::scheduler::mSchedule: Set(),533 schedFixed::scheduler::published: 0,534 schedFixed::scheduler::publishedBy: Set(),535 schedFixed::scheduler::ws:536 Map(537 "w1" ->538 {539 attached: Set(),540 built: false,541 expecting: false,542 running: false,543 session: true,544 up: true545 },546 "w2" ->547 {548 attached: Set(),549 built: false,550 expecting: false,551 running: false,552 session: true,553 up: true554 }555 )556}557558[State 14]559{560 schedFixed::scheduler::cl: Map("c1" -> CQueued, "c2" -> CQueued),561 schedFixed::scheduler::crashes: 2,562 schedFixed::scheduler::entry:563 [{ followers: Set("c2"), leased: true, worker: "w1" }],564 schedFixed::scheduler::free: Map("w1" -> 0, "w2" -> 1),565 schedFixed::scheduler::mAssigned: Set(("c2", "w1")),566 schedFixed::scheduler::mBuild: Set(("c1", "w2"), ("c2", "w2")),567 schedFixed::scheduler::mDone: Set(),568 schedFixed::scheduler::mExpect: Set("w1"),569 schedFixed::scheduler::mResult: Set(),570 schedFixed::scheduler::mRetry: Set(),571 schedFixed::scheduler::mRevoke: Set(),572 schedFixed::scheduler::mSchedule: Set("c1"),573 schedFixed::scheduler::published: 0,574 schedFixed::scheduler::publishedBy: Set(),575 schedFixed::scheduler::ws:576 Map(577 "w1" ->578 {579 attached: Set(),580 built: false,581 expecting: false,582 running: false,583 session: true,584 up: true585 },586 "w2" ->587 {588 attached: Set(),589 built: false,590 expecting: false,591 running: false,592 session: true,593 up: true594 }595 )596}597598[State 15]599{600 schedFixed::scheduler::cl: Map("c1" -> CQueued, "c2" -> CQueued),601 schedFixed::scheduler::crashes: 2,602 schedFixed::scheduler::entry:603 [{ followers: Set("c1", "c2"), leased: true, worker: "w1" }],604 schedFixed::scheduler::free: Map("w1" -> 0, "w2" -> 1),605 schedFixed::scheduler::mAssigned: Set(("c1", "w1"), ("c2", "w1")),606 schedFixed::scheduler::mBuild: Set(("c1", "w2"), ("c2", "w2")),607 schedFixed::scheduler::mDone: Set(),608 schedFixed::scheduler::mExpect: Set("w1"),609 schedFixed::scheduler::mResult: Set(),610 schedFixed::scheduler::mRetry: Set(),611 schedFixed::scheduler::mRevoke: Set(),612 schedFixed::scheduler::mSchedule: Set(),613 schedFixed::scheduler::published: 0,614 schedFixed::scheduler::publishedBy: Set(),615 schedFixed::scheduler::ws:616 Map(617 "w1" ->618 {619 attached: Set(),620 built: false,621 expecting: false,622 running: false,623 session: true,624 up: true625 },626 "w2" ->627 {628 attached: Set(),629 built: false,630 expecting: false,631 running: false,632 session: true,633 up: true634 }635 )636}637638[State 16]639{640 schedFixed::scheduler::cl: Map("c1" -> CQueued, "c2" -> CQueued),641 schedFixed::scheduler::crashes: 2,642 schedFixed::scheduler::entry:643 [{ followers: Set("c1", "c2"), leased: true, worker: "w1" }],644 schedFixed::scheduler::free: Map("w1" -> 0, "w2" -> 1),645 schedFixed::scheduler::mAssigned: Set(("c1", "w1"), ("c2", "w1")),646 schedFixed::scheduler::mBuild: Set(("c1", "w2")),647 schedFixed::scheduler::mDone: Set(),648 schedFixed::scheduler::mExpect: Set("w1"),649 schedFixed::scheduler::mResult: Set(),650 schedFixed::scheduler::mRetry: Set("c2"),651 schedFixed::scheduler::mRevoke: Set(),652 schedFixed::scheduler::mSchedule: Set(),653 schedFixed::scheduler::published: 0,654 schedFixed::scheduler::publishedBy: Set(),655 schedFixed::scheduler::ws:656 Map(657 "w1" ->658 {659 attached: Set(),660 built: false,661 expecting: false,662 running: false,663 session: true,664 up: true665 },666 "w2" ->667 {668 attached: Set(),669 built: false,670 expecting: false,671 running: false,672 session: true,673 up: true674 }675 )676}677678[State 17]679{680 schedFixed::scheduler::cl: Map("c1" -> CQueued, "c2" -> CSent("w1")),681 schedFixed::scheduler::crashes: 2,682 schedFixed::scheduler::entry:683 [{ followers: Set("c1", "c2"), leased: true, worker: "w1" }],684 schedFixed::scheduler::free: Map("w1" -> 0, "w2" -> 1),685 schedFixed::scheduler::mAssigned: Set(("c1", "w1")),686 schedFixed::scheduler::mBuild: Set(("c1", "w2"), ("c2", "w1")),687 schedFixed::scheduler::mDone: Set(),688 schedFixed::scheduler::mExpect: Set("w1"),689 schedFixed::scheduler::mResult: Set(),690 schedFixed::scheduler::mRetry: Set("c2"),691 schedFixed::scheduler::mRevoke: Set(),692 schedFixed::scheduler::mSchedule: Set(),693 schedFixed::scheduler::published: 0,694 schedFixed::scheduler::publishedBy: Set(),695 schedFixed::scheduler::ws:696 Map(697 "w1" ->698 {699 attached: Set(),700 built: false,701 expecting: false,702 running: false,703 session: true,704 up: true705 },706 "w2" ->707 {708 attached: Set(),709 built: false,710 expecting: false,711 running: false,712 session: true,713 up: true714 }715 )716}717718[State 18]719{720 schedFixed::scheduler::cl: Map("c1" -> CQueued, "c2" -> CSent("w1")),721 schedFixed::scheduler::crashes: 2,722 schedFixed::scheduler::entry:723 [{ followers: Set("c1", "c2"), leased: true, worker: "w1" }],724 schedFixed::scheduler::free: Map("w1" -> 0, "w2" -> 1),725 schedFixed::scheduler::mAssigned: Set(("c1", "w1")),726 schedFixed::scheduler::mBuild: Set(("c1", "w2"), ("c2", "w1")),727 schedFixed::scheduler::mDone: Set(),728 schedFixed::scheduler::mExpect: Set(),729 schedFixed::scheduler::mResult: Set(),730 schedFixed::scheduler::mRetry: Set("c2"),731 schedFixed::scheduler::mRevoke: Set(),732 schedFixed::scheduler::mSchedule: Set(),733 schedFixed::scheduler::published: 0,734 schedFixed::scheduler::publishedBy: Set(),735 schedFixed::scheduler::ws:736 Map(737 "w1" ->738 {739 attached: Set(),740 built: false,741 expecting: true,742 running: true,743 session: true,744 up: true745 },746 "w2" ->747 {748 attached: Set(),749 built: false,750 expecting: false,751 running: false,752 session: true,753 up: true754 }755 )756}757758[State 19]759{760 schedFixed::scheduler::cl: Map("c1" -> CSent("w1"), "c2" -> CSent("w1")),761 schedFixed::scheduler::crashes: 2,762 schedFixed::scheduler::entry:763 [{ followers: Set("c1", "c2"), leased: true, worker: "w1" }],764 schedFixed::scheduler::free: Map("w1" -> 0, "w2" -> 1),765 schedFixed::scheduler::mAssigned: Set(),766 schedFixed::scheduler::mBuild: Set(("c1", "w1"), ("c1", "w2"), ("c2", "w1")),767 schedFixed::scheduler::mDone: Set(),768 schedFixed::scheduler::mExpect: Set(),769 schedFixed::scheduler::mResult: Set(),770 schedFixed::scheduler::mRetry: Set("c2"),771 schedFixed::scheduler::mRevoke: Set(),772 schedFixed::scheduler::mSchedule: Set(),773 schedFixed::scheduler::published: 0,774 schedFixed::scheduler::publishedBy: Set(),775 schedFixed::scheduler::ws:776 Map(777 "w1" ->778 {779 attached: Set(),780 built: false,781 expecting: true,782 running: true,783 session: true,784 up: true785 },786 "w2" ->787 {788 attached: Set(),789 built: false,790 expecting: false,791 running: false,792 session: true,793 up: true794 }795 )796}797798[State 20]799{800 schedFixed::scheduler::cl: Map("c1" -> CSent("w1"), "c2" -> CSent("w1")),801 schedFixed::scheduler::crashes: 2,802 schedFixed::scheduler::entry:803 [{ followers: Set("c1", "c2"), leased: true, worker: "w1" }],804 schedFixed::scheduler::free: Map("w1" -> 0, "w2" -> 1),805 schedFixed::scheduler::mAssigned: Set(),806 schedFixed::scheduler::mBuild: Set(("c1", "w1"), ("c2", "w1")),807 schedFixed::scheduler::mDone: Set(),808 schedFixed::scheduler::mExpect: Set(),809 schedFixed::scheduler::mResult: Set(),810 schedFixed::scheduler::mRetry: Set("c1", "c2"),811 schedFixed::scheduler::mRevoke: Set(),812 schedFixed::scheduler::mSchedule: Set(),813 schedFixed::scheduler::published: 0,814 schedFixed::scheduler::publishedBy: Set(),815 schedFixed::scheduler::ws:816 Map(817 "w1" ->818 {819 attached: Set(),820 built: false,821 expecting: true,822 running: true,823 session: true,824 up: true825 },826 "w2" ->827 {828 attached: Set(),829 built: false,830 expecting: false,831 running: false,832 session: true,833 up: true834 }835 )836}837838[State 21]839{840 schedFixed::scheduler::cl: Map("c1" -> CSent("w1"), "c2" -> CQueued),841 schedFixed::scheduler::crashes: 2,842 schedFixed::scheduler::entry:843 [{ followers: Set("c1", "c2"), leased: true, worker: "w1" }],844 schedFixed::scheduler::free: Map("w1" -> 0, "w2" -> 1),845 schedFixed::scheduler::mAssigned: Set(),846 schedFixed::scheduler::mBuild: Set(("c1", "w1"), ("c2", "w1")),847 schedFixed::scheduler::mDone: Set(),848 schedFixed::scheduler::mExpect: Set(),849 schedFixed::scheduler::mResult: Set(),850 schedFixed::scheduler::mRetry: Set("c1"),851 schedFixed::scheduler::mRevoke: Set(),852 schedFixed::scheduler::mSchedule: Set("c2"),853 schedFixed::scheduler::published: 0,854 schedFixed::scheduler::publishedBy: Set(),855 schedFixed::scheduler::ws:856 Map(857 "w1" ->858 {859 attached: Set(),860 built: false,861 expecting: true,862 running: true,863 session: true,864 up: true865 },866 "w2" ->867 {868 attached: Set(),869 built: false,870 expecting: false,871 running: false,872 session: true,873 up: true874 }875 )876}877878[State 22]879{880 schedFixed::scheduler::cl: Map("c1" -> CSent("w1"), "c2" -> CQueued),881 schedFixed::scheduler::crashes: 2,882 schedFixed::scheduler::entry:883 [{ followers: Set("c1", "c2"), leased: true, worker: "w1" }],884 schedFixed::scheduler::free: Map("w1" -> 0, "w2" -> 1),885 schedFixed::scheduler::mAssigned: Set(),886 schedFixed::scheduler::mBuild: Set(("c1", "w1")),887 schedFixed::scheduler::mDone: Set(),888 schedFixed::scheduler::mExpect: Set(),889 schedFixed::scheduler::mResult: Set(),890 schedFixed::scheduler::mRetry: Set("c1"),891 schedFixed::scheduler::mRevoke: Set(),892 schedFixed::scheduler::mSchedule: Set("c2"),893 schedFixed::scheduler::published: 0,894 schedFixed::scheduler::publishedBy: Set(),895 schedFixed::scheduler::ws:896 Map(897 "w1" ->898 {899 attached: Set("c2"),900 built: false,901 expecting: true,902 running: true,903 session: true,904 up: true905 },906 "w2" ->907 {908 attached: Set(),909 built: false,910 expecting: false,911 running: false,912 session: true,913 up: true914 }915 )916}917918[State 23]919{920 schedFixed::scheduler::cl: Map("c1" -> CSent("w1"), "c2" -> CQueued),921 schedFixed::scheduler::crashes: 2,922 schedFixed::scheduler::entry:923 [{ followers: Set("c1", "c2"), leased: true, worker: "w1" }],924 schedFixed::scheduler::free: Map("w1" -> 0, "w2" -> 1),925 schedFixed::scheduler::mAssigned: Set(("c2", "w1")),926 schedFixed::scheduler::mBuild: Set(("c1", "w1")),927 schedFixed::scheduler::mDone: Set(),928 schedFixed::scheduler::mExpect: Set(),929 schedFixed::scheduler::mResult: Set(),930 schedFixed::scheduler::mRetry: Set("c1"),931 schedFixed::scheduler::mRevoke: Set(),932 schedFixed::scheduler::mSchedule: Set(),933 schedFixed::scheduler::published: 0,934 schedFixed::scheduler::publishedBy: Set(),935 schedFixed::scheduler::ws:936 Map(937 "w1" ->938 {939 attached: Set("c2"),940 built: false,941 expecting: true,942 running: true,943 session: true,944 up: true945 },946 "w2" ->947 {948 attached: Set(),949 built: false,950 expecting: false,951 running: false,952 session: true,953 up: true954 }955 )956}957958[State 24]959{960 schedFixed::scheduler::cl: Map("c1" -> CSent("w1"), "c2" -> CQueued),961 schedFixed::scheduler::crashes: 2,962 schedFixed::scheduler::entry:963 [{ followers: Set("c1", "c2"), leased: true, worker: "w1" }],964 schedFixed::scheduler::free: Map("w1" -> 0, "w2" -> 1),965 schedFixed::scheduler::mAssigned: Set(("c2", "w1")),966 schedFixed::scheduler::mBuild: Set(("c1", "w1")),967 schedFixed::scheduler::mDone: Set("w1"),968 schedFixed::scheduler::mExpect: Set(),969 schedFixed::scheduler::mResult: Set("c2"),970 schedFixed::scheduler::mRetry: Set("c1"),971 schedFixed::scheduler::mRevoke: Set(),972 schedFixed::scheduler::mSchedule: Set(),973 schedFixed::scheduler::published: 1,974 schedFixed::scheduler::publishedBy: Set("w1"),975 schedFixed::scheduler::ws:976 Map(977 "w1" ->978 {979 attached: Set(),980 built: true,981 expecting: false,982 running: false,983 session: true,984 up: true985 },986 "w2" ->987 {988 attached: Set(),989 built: false,990 expecting: false,991 running: false,992 session: true,993 up: true994 }995 )996}997998[State 25]999{1000 schedFixed::scheduler::cl: Map("c1" -> CSent("w1"), "c2" -> CQueued),1001 schedFixed::scheduler::crashes: 2,1002 schedFixed::scheduler::entry: [],1003 schedFixed::scheduler::free: Map("w1" -> 1, "w2" -> 1),1004 schedFixed::scheduler::mAssigned: Set(("c2", "w1")),1005 schedFixed::scheduler::mBuild: Set(("c1", "w1")),1006 schedFixed::scheduler::mDone: Set(),1007 schedFixed::scheduler::mExpect: Set(),1008 schedFixed::scheduler::mResult: Set("c2"),1009 schedFixed::scheduler::mRetry: Set("c1"),1010 schedFixed::scheduler::mRevoke: Set(),1011 schedFixed::scheduler::mSchedule: Set(),1012 schedFixed::scheduler::published: 1,1013 schedFixed::scheduler::publishedBy: Set("w1"),1014 schedFixed::scheduler::ws:1015 Map(1016 "w1" ->1017 {1018 attached: Set(),1019 built: true,1020 expecting: false,1021 running: false,1022 session: true,1023 up: true1024 },1025 "w2" ->1026 {1027 attached: Set(),1028 built: false,1029 expecting: false,1030 running: false,1031 session: true,1032 up: true1033 }1034 )1035}10361037[State 26]1038{1039 schedFixed::scheduler::cl: Map("c1" -> CQueued, "c2" -> CQueued),1040 schedFixed::scheduler::crashes: 2,1041 schedFixed::scheduler::entry: [],1042 schedFixed::scheduler::free: Map("w1" -> 1, "w2" -> 1),1043 schedFixed::scheduler::mAssigned: Set(("c2", "w1")),1044 schedFixed::scheduler::mBuild: Set(("c1", "w1")),1045 schedFixed::scheduler::mDone: Set(),1046 schedFixed::scheduler::mExpect: Set(),1047 schedFixed::scheduler::mResult: Set("c2"),1048 schedFixed::scheduler::mRetry: Set(),1049 schedFixed::scheduler::mRevoke: Set(),1050 schedFixed::scheduler::mSchedule: Set("c1"),1051 schedFixed::scheduler::published: 1,1052 schedFixed::scheduler::publishedBy: Set("w1"),1053 schedFixed::scheduler::ws:1054 Map(1055 "w1" ->1056 {1057 attached: Set(),1058 built: true,1059 expecting: false,1060 running: false,1061 session: true,1062 up: true1063 },1064 "w2" ->1065 {1066 attached: Set(),1067 built: false,1068 expecting: false,1069 running: false,1070 session: true,1071 up: true1072 }1073 )1074}10751076[State 27]1077{1078 schedFixed::scheduler::cl: Map("c1" -> CQueued, "c2" -> CDone),1079 schedFixed::scheduler::crashes: 2,1080 schedFixed::scheduler::entry: [],1081 schedFixed::scheduler::free: Map("w1" -> 1, "w2" -> 1),1082 schedFixed::scheduler::mAssigned: Set(("c2", "w1")),1083 schedFixed::scheduler::mBuild: Set(("c1", "w1")),1084 schedFixed::scheduler::mDone: Set(),1085 schedFixed::scheduler::mExpect: Set(),1086 schedFixed::scheduler::mResult: Set(),1087 schedFixed::scheduler::mRetry: Set(),1088 schedFixed::scheduler::mRevoke: Set(),1089 schedFixed::scheduler::mSchedule: Set("c1"),1090 schedFixed::scheduler::published: 1,1091 schedFixed::scheduler::publishedBy: Set("w1"),1092 schedFixed::scheduler::ws:1093 Map(1094 "w1" ->1095 {1096 attached: Set(),1097 built: true,1098 expecting: false,1099 running: false,1100 session: true,1101 up: true1102 },1103 "w2" ->1104 {1105 attached: Set(),1106 built: false,1107 expecting: false,1108 running: false,1109 session: true,1110 up: true1111 }1112 )1113}11141115[State 28]1116{1117 schedFixed::scheduler::cl: Map("c1" -> CQueued, "c2" -> CDone),1118 schedFixed::scheduler::crashes: 2,1119 schedFixed::scheduler::entry: [],1120 schedFixed::scheduler::free: Map("w1" -> 1, "w2" -> 1),1121 schedFixed::scheduler::mAssigned: Set(("c2", "w1")),1122 schedFixed::scheduler::mBuild: Set(("c1", "w1")),1123 schedFixed::scheduler::mDone: Set(),1124 schedFixed::scheduler::mExpect: Set(),1125 schedFixed::scheduler::mResult: Set("c1"),1126 schedFixed::scheduler::mRetry: Set(),1127 schedFixed::scheduler::mRevoke: Set(),1128 schedFixed::scheduler::mSchedule: Set(),1129 schedFixed::scheduler::published: 1,1130 schedFixed::scheduler::publishedBy: Set("w1"),1131 schedFixed::scheduler::ws:1132 Map(1133 "w1" ->1134 {1135 attached: Set(),1136 built: true,1137 expecting: false,1138 running: false,1139 session: true,1140 up: true1141 },1142 "w2" ->1143 {1144 attached: Set(),1145 built: false,1146 expecting: false,1147 running: false,1148 session: true,1149 up: true1150 }1151 )1152}11531154[State 29]1155{1156 schedFixed::scheduler::cl: Map("c1" -> CQueued, "c2" -> CDone),1157 schedFixed::scheduler::crashes: 2,1158 schedFixed::scheduler::entry: [],1159 schedFixed::scheduler::free: Map("w1" -> 1, "w2" -> 1),1160 schedFixed::scheduler::mAssigned: Set(("c2", "w1")),1161 schedFixed::scheduler::mBuild: Set(),1162 schedFixed::scheduler::mDone: Set(),1163 schedFixed::scheduler::mExpect: Set(),1164 schedFixed::scheduler::mResult: Set("c1"),1165 schedFixed::scheduler::mRetry: Set(),1166 schedFixed::scheduler::mRevoke: Set(),1167 schedFixed::scheduler::mSchedule: Set(),1168 schedFixed::scheduler::published: 1,1169 schedFixed::scheduler::publishedBy: Set("w1"),1170 schedFixed::scheduler::ws:1171 Map(1172 "w1" ->1173 {1174 attached: Set(),1175 built: true,1176 expecting: false,1177 running: false,1178 session: true,1179 up: true1180 },1181 "w2" ->1182 {1183 attached: Set(),1184 built: false,1185 expecting: false,1186 running: false,1187 session: true,1188 up: true1189 }1190 )1191}11921193[State 30]1194{1195 schedFixed::scheduler::cl: Map("c1" -> CDone, "c2" -> CDone),1196 schedFixed::scheduler::crashes: 2,1197 schedFixed::scheduler::entry: [],1198 schedFixed::scheduler::free: Map("w1" -> 1, "w2" -> 1),1199 schedFixed::scheduler::mAssigned: Set(("c2", "w1")),1200 schedFixed::scheduler::mBuild: Set(),1201 schedFixed::scheduler::mDone: Set(),1202 schedFixed::scheduler::mExpect: Set(),1203 schedFixed::scheduler::mResult: Set(),1204 schedFixed::scheduler::mRetry: Set(),1205 schedFixed::scheduler::mRevoke: Set(),1206 schedFixed::scheduler::mSchedule: Set(),1207 schedFixed::scheduler::published: 1,1208 schedFixed::scheduler::publishedBy: Set("w1"),1209 schedFixed::scheduler::ws:1210 Map(1211 "w1" ->1212 {1213 attached: Set(),1214 built: true,1215 expecting: false,1216 running: false,1217 session: true,1218 up: true1219 },1220 "w2" ->1221 {1222 attached: Set(),1223 built: false,1224 expecting: false,1225 running: false,1226 session: true,1227 up: true1228 }1229 )1230}12311232[ok] No violation found (483ms at 62112 traces/second).1233Trace length statistics: max=29, min=16, average=19.011234You may increase --max-samples and --max-steps.1235Use --verbosity to produce more (or less) output.1236Use --seed=0x369c6da309ae82af --backend=rust to reproduce.1237An example execution:12381239[State 0]1240{1241 schedNoRevoke::scheduler::cl: Map("c1" -> CIdle, "c2" -> CIdle),1242 schedNoRevoke::scheduler::crashes: 0,1243 schedNoRevoke::scheduler::entry: [],1244 schedNoRevoke::scheduler::free: Map("w1" -> 1, "w2" -> 1),1245 schedNoRevoke::scheduler::mAssigned: Set(),1246 schedNoRevoke::scheduler::mBuild: Set(),1247 schedNoRevoke::scheduler::mDone: Set(),1248 schedNoRevoke::scheduler::mExpect: Set(),1249 schedNoRevoke::scheduler::mResult: Set(),1250 schedNoRevoke::scheduler::mRetry: Set(),1251 schedNoRevoke::scheduler::mRevoke: Set(),1252 schedNoRevoke::scheduler::mSchedule: Set(),1253 schedNoRevoke::scheduler::published: 0,1254 schedNoRevoke::scheduler::publishedBy: Set(),1255 schedNoRevoke::scheduler::ws:1256 Map(1257 "w1" ->1258 {1259 attached: Set(),1260 built: false,1261 expecting: false,1262 running: false,1263 session: true,1264 up: true1265 },1266 "w2" ->1267 {1268 attached: Set(),1269 built: false,1270 expecting: false,1271 running: false,1272 session: true,1273 up: true1274 }1275 )1276}12771278[State 1]1279{1280 schedNoRevoke::scheduler::cl: Map("c1" -> CIdle, "c2" -> CIdle),1281 schedNoRevoke::scheduler::crashes: 1,1282 schedNoRevoke::scheduler::entry: [],1283 schedNoRevoke::scheduler::free: Map("w1" -> 1, "w2" -> 1),1284 schedNoRevoke::scheduler::mAssigned: Set(),1285 schedNoRevoke::scheduler::mBuild: Set(),1286 schedNoRevoke::scheduler::mDone: Set(),1287 schedNoRevoke::scheduler::mExpect: Set(),1288 schedNoRevoke::scheduler::mResult: Set(),1289 schedNoRevoke::scheduler::mRetry: Set(),1290 schedNoRevoke::scheduler::mRevoke: Set(),1291 schedNoRevoke::scheduler::mSchedule: Set(),1292 schedNoRevoke::scheduler::published: 0,1293 schedNoRevoke::scheduler::publishedBy: Set(),1294 schedNoRevoke::scheduler::ws:1295 Map(1296 "w1" ->1297 {1298 attached: Set(),1299 built: false,1300 expecting: false,1301 running: false,1302 session: true,1303 up: true1304 },1305 "w2" ->1306 {1307 attached: Set(),1308 built: false,1309 expecting: false,1310 running: false,1311 session: false,1312 up: false1313 }1314 )1315}13161317[State 2]1318{1319 schedNoRevoke::scheduler::cl: Map("c1" -> CIdle, "c2" -> CQueued),1320 schedNoRevoke::scheduler::crashes: 1,1321 schedNoRevoke::scheduler::entry: [],1322 schedNoRevoke::scheduler::free: Map("w1" -> 1, "w2" -> 1),1323 schedNoRevoke::scheduler::mAssigned: Set(),1324 schedNoRevoke::scheduler::mBuild: Set(),1325 schedNoRevoke::scheduler::mDone: Set(),1326 schedNoRevoke::scheduler::mExpect: Set(),1327 schedNoRevoke::scheduler::mResult: Set(),1328 schedNoRevoke::scheduler::mRetry: Set(),1329 schedNoRevoke::scheduler::mRevoke: Set(),1330 schedNoRevoke::scheduler::mSchedule: Set("c2"),1331 schedNoRevoke::scheduler::published: 0,1332 schedNoRevoke::scheduler::publishedBy: Set(),1333 schedNoRevoke::scheduler::ws:1334 Map(1335 "w1" ->1336 {1337 attached: Set(),1338 built: false,1339 expecting: false,1340 running: false,1341 session: true,1342 up: true1343 },1344 "w2" ->1345 {1346 attached: Set(),1347 built: false,1348 expecting: false,1349 running: false,1350 session: false,1351 up: false1352 }1353 )1354}13551356[State 3]1357{1358 schedNoRevoke::scheduler::cl: Map("c1" -> CQueued, "c2" -> CQueued),1359 schedNoRevoke::scheduler::crashes: 1,1360 schedNoRevoke::scheduler::entry: [],1361 schedNoRevoke::scheduler::free: Map("w1" -> 1, "w2" -> 1),1362 schedNoRevoke::scheduler::mAssigned: Set(),1363 schedNoRevoke::scheduler::mBuild: Set(),1364 schedNoRevoke::scheduler::mDone: Set(),1365 schedNoRevoke::scheduler::mExpect: Set(),1366 schedNoRevoke::scheduler::mResult: Set(),1367 schedNoRevoke::scheduler::mRetry: Set(),1368 schedNoRevoke::scheduler::mRevoke: Set(),1369 schedNoRevoke::scheduler::mSchedule: Set("c1", "c2"),1370 schedNoRevoke::scheduler::published: 0,1371 schedNoRevoke::scheduler::publishedBy: Set(),1372 schedNoRevoke::scheduler::ws:1373 Map(1374 "w1" ->1375 {1376 attached: Set(),1377 built: false,1378 expecting: false,1379 running: false,1380 session: true,1381 up: true1382 },1383 "w2" ->1384 {1385 attached: Set(),1386 built: false,1387 expecting: false,1388 running: false,1389 session: false,1390 up: false1391 }1392 )1393}13941395[State 4]1396{1397 schedNoRevoke::scheduler::cl: Map("c1" -> CQueued, "c2" -> CQueued),1398 schedNoRevoke::scheduler::crashes: 1,1399 schedNoRevoke::scheduler::entry:1400 [{ followers: Set("c2"), leased: true, worker: "w1" }],1401 schedNoRevoke::scheduler::free: Map("w1" -> 0, "w2" -> 1),1402 schedNoRevoke::scheduler::mAssigned: Set(("c2", "w1")),1403 schedNoRevoke::scheduler::mBuild: Set(),1404 schedNoRevoke::scheduler::mDone: Set(),1405 schedNoRevoke::scheduler::mExpect: Set("w1"),1406 schedNoRevoke::scheduler::mResult: Set(),1407 schedNoRevoke::scheduler::mRetry: Set(),1408 schedNoRevoke::scheduler::mRevoke: Set(),1409 schedNoRevoke::scheduler::mSchedule: Set("c1"),1410 schedNoRevoke::scheduler::published: 0,1411 schedNoRevoke::scheduler::publishedBy: Set(),1412 schedNoRevoke::scheduler::ws:1413 Map(1414 "w1" ->1415 {1416 attached: Set(),1417 built: false,1418 expecting: false,1419 running: false,1420 session: true,1421 up: true1422 },1423 "w2" ->1424 {1425 attached: Set(),1426 built: false,1427 expecting: false,1428 running: false,1429 session: false,1430 up: false1431 }1432 )1433}14341435[State 5]1436{1437 schedNoRevoke::scheduler::cl: Map("c1" -> CQueued, "c2" -> CQueued),1438 schedNoRevoke::scheduler::crashes: 1,1439 schedNoRevoke::scheduler::entry:1440 [{ followers: Set("c2"), leased: true, worker: "w1" }],1441 schedNoRevoke::scheduler::free: Map("w1" -> 0, "w2" -> 1),1442 schedNoRevoke::scheduler::mAssigned: Set(("c2", "w1")),1443 schedNoRevoke::scheduler::mBuild: Set(),1444 schedNoRevoke::scheduler::mDone: Set(),1445 schedNoRevoke::scheduler::mExpect: Set(),1446 schedNoRevoke::scheduler::mResult: Set(),1447 schedNoRevoke::scheduler::mRetry: Set(),1448 schedNoRevoke::scheduler::mRevoke: Set(),1449 schedNoRevoke::scheduler::mSchedule: Set("c1"),1450 schedNoRevoke::scheduler::published: 0,1451 schedNoRevoke::scheduler::publishedBy: Set(),1452 schedNoRevoke::scheduler::ws:1453 Map(1454 "w1" ->1455 {1456 attached: Set(),1457 built: false,1458 expecting: true,1459 running: true,1460 session: true,1461 up: true1462 },1463 "w2" ->1464 {1465 attached: Set(),1466 built: false,1467 expecting: false,1468 running: false,1469 session: false,1470 up: false1471 }1472 )1473}14741475[State 6]1476{1477 schedNoRevoke::scheduler::cl: Map("c1" -> CQueued, "c2" -> CQueued),1478 schedNoRevoke::scheduler::crashes: 2,1479 schedNoRevoke::scheduler::entry: [],1480 schedNoRevoke::scheduler::free: Map("w1" -> 1, "w2" -> 1),1481 schedNoRevoke::scheduler::mAssigned: Set(),1482 schedNoRevoke::scheduler::mBuild: Set(),1483 schedNoRevoke::scheduler::mDone: Set(),1484 schedNoRevoke::scheduler::mExpect: Set(),1485 schedNoRevoke::scheduler::mResult: Set(),1486 schedNoRevoke::scheduler::mRetry: Set("c1", "c2"),1487 schedNoRevoke::scheduler::mRevoke: Set(),1488 schedNoRevoke::scheduler::mSchedule: Set(),1489 schedNoRevoke::scheduler::published: 0,1490 schedNoRevoke::scheduler::publishedBy: Set(),1491 schedNoRevoke::scheduler::ws:1492 Map(1493 "w1" ->1494 {1495 attached: Set(),1496 built: false,1497 expecting: true,1498 running: true,1499 session: false,1500 up: true1501 },1502 "w2" ->1503 {1504 attached: Set(),1505 built: false,1506 expecting: false,1507 running: false,1508 session: false,1509 up: false1510 }1511 )1512}15131514[State 7]1515{1516 schedNoRevoke::scheduler::cl: Map("c1" -> CQueued, "c2" -> CQueued),1517 schedNoRevoke::scheduler::crashes: 2,1518 schedNoRevoke::scheduler::entry: [],1519 schedNoRevoke::scheduler::free: Map("w1" -> 1, "w2" -> 1),1520 schedNoRevoke::scheduler::mAssigned: Set(),1521 schedNoRevoke::scheduler::mBuild: Set(),1522 schedNoRevoke::scheduler::mDone: Set(),1523 schedNoRevoke::scheduler::mExpect: Set(),1524 schedNoRevoke::scheduler::mResult: Set(),1525 schedNoRevoke::scheduler::mRetry: Set("c1", "c2"),1526 schedNoRevoke::scheduler::mRevoke: Set(),1527 schedNoRevoke::scheduler::mSchedule: Set(),1528 schedNoRevoke::scheduler::published: 0,1529 schedNoRevoke::scheduler::publishedBy: Set(),1530 schedNoRevoke::scheduler::ws:1531 Map(1532 "w1" ->1533 {1534 attached: Set(),1535 built: false,1536 expecting: true,1537 running: true,1538 session: false,1539 up: true1540 },1541 "w2" ->1542 {1543 attached: Set(),1544 built: false,1545 expecting: false,1546 running: false,1547 session: true,1548 up: true1549 }1550 )1551}15521553[State 8]1554{1555 schedNoRevoke::scheduler::cl: Map("c1" -> CQueued, "c2" -> CQueued),1556 schedNoRevoke::scheduler::crashes: 2,1557 schedNoRevoke::scheduler::entry: [],1558 schedNoRevoke::scheduler::free: Map("w1" -> 1, "w2" -> 1),1559 schedNoRevoke::scheduler::mAssigned: Set(),1560 schedNoRevoke::scheduler::mBuild: Set(),1561 schedNoRevoke::scheduler::mDone: Set(),1562 schedNoRevoke::scheduler::mExpect: Set(),1563 schedNoRevoke::scheduler::mResult: Set(),1564 schedNoRevoke::scheduler::mRetry: Set("c1"),1565 schedNoRevoke::scheduler::mRevoke: Set(),1566 schedNoRevoke::scheduler::mSchedule: Set("c2"),1567 schedNoRevoke::scheduler::published: 0,1568 schedNoRevoke::scheduler::publishedBy: Set(),1569 schedNoRevoke::scheduler::ws:1570 Map(1571 "w1" ->1572 {1573 attached: Set(),1574 built: false,1575 expecting: true,1576 running: true,1577 session: false,1578 up: true1579 },1580 "w2" ->1581 {1582 attached: Set(),1583 built: false,1584 expecting: false,1585 running: false,1586 session: true,1587 up: true1588 }1589 )1590}15911592[State 9]1593{1594 schedNoRevoke::scheduler::cl: Map("c1" -> CQueued, "c2" -> CQueued),1595 schedNoRevoke::scheduler::crashes: 2,1596 schedNoRevoke::scheduler::entry:1597 [{ followers: Set("c2"), leased: true, worker: "w2" }],1598 schedNoRevoke::scheduler::free: Map("w1" -> 1, "w2" -> 0),1599 schedNoRevoke::scheduler::mAssigned: Set(("c2", "w2")),1600 schedNoRevoke::scheduler::mBuild: Set(),1601 schedNoRevoke::scheduler::mDone: Set(),1602 schedNoRevoke::scheduler::mExpect: Set("w2"),1603 schedNoRevoke::scheduler::mResult: Set(),1604 schedNoRevoke::scheduler::mRetry: Set("c1"),1605 schedNoRevoke::scheduler::mRevoke: Set(),1606 schedNoRevoke::scheduler::mSchedule: Set(),1607 schedNoRevoke::scheduler::published: 0,1608 schedNoRevoke::scheduler::publishedBy: Set(),1609 schedNoRevoke::scheduler::ws:1610 Map(1611 "w1" ->1612 {1613 attached: Set(),1614 built: false,1615 expecting: true,1616 running: true,1617 session: false,1618 up: true1619 },1620 "w2" ->1621 {1622 attached: Set(),1623 built: false,1624 expecting: false,1625 running: false,1626 session: true,1627 up: true1628 }1629 )1630}16311632[State 10]1633{1634 schedNoRevoke::scheduler::cl: Map("c1" -> CQueued, "c2" -> CQueued),1635 schedNoRevoke::scheduler::crashes: 2,1636 schedNoRevoke::scheduler::entry:1637 [{ followers: Set("c2"), leased: true, worker: "w2" }],1638 schedNoRevoke::scheduler::free: Map("w1" -> 0, "w2" -> 0),1639 schedNoRevoke::scheduler::mAssigned: Set(("c2", "w2")),1640 schedNoRevoke::scheduler::mBuild: Set(),1641 schedNoRevoke::scheduler::mDone: Set(),1642 schedNoRevoke::scheduler::mExpect: Set("w2"),1643 schedNoRevoke::scheduler::mResult: Set(),1644 schedNoRevoke::scheduler::mRetry: Set("c1"),1645 schedNoRevoke::scheduler::mRevoke: Set(),1646 schedNoRevoke::scheduler::mSchedule: Set(),1647 schedNoRevoke::scheduler::published: 0,1648 schedNoRevoke::scheduler::publishedBy: Set(),1649 schedNoRevoke::scheduler::ws:1650 Map(1651 "w1" ->1652 {1653 attached: Set(),1654 built: false,1655 expecting: true,1656 running: true,1657 session: true,1658 up: true1659 },1660 "w2" ->1661 {1662 attached: Set(),1663 built: false,1664 expecting: false,1665 running: false,1666 session: true,1667 up: true1668 }1669 )1670}16711672[State 11]1673{1674 schedNoRevoke::scheduler::cl: Map("c1" -> CQueued, "c2" -> CQueued),1675 schedNoRevoke::scheduler::crashes: 2,1676 schedNoRevoke::scheduler::entry:1677 [{ followers: Set("c2"), leased: true, worker: "w2" }],1678 schedNoRevoke::scheduler::free: Map("w1" -> 0, "w2" -> 0),1679 schedNoRevoke::scheduler::mAssigned: Set(("c2", "w2")),1680 schedNoRevoke::scheduler::mBuild: Set(),1681 schedNoRevoke::scheduler::mDone: Set(),1682 schedNoRevoke::scheduler::mExpect: Set(),1683 schedNoRevoke::scheduler::mResult: Set(),1684 schedNoRevoke::scheduler::mRetry: Set("c1"),1685 schedNoRevoke::scheduler::mRevoke: Set(),1686 schedNoRevoke::scheduler::mSchedule: Set(),1687 schedNoRevoke::scheduler::published: 0,1688 schedNoRevoke::scheduler::publishedBy: Set(),1689 schedNoRevoke::scheduler::ws:1690 Map(1691 "w1" ->1692 {1693 attached: Set(),1694 built: false,1695 expecting: true,1696 running: true,1697 session: true,1698 up: true1699 },1700 "w2" ->1701 {1702 attached: Set(),1703 built: false,1704 expecting: true,1705 running: true,1706 session: true,1707 up: true1708 }1709 )1710}17111712[violation] Found an issue (485ms at 59680 traces/second).1713Use --verbosity=3 to show executions.1714Use --seed=0x6fb330d70beb390d --backend=rust to reproduce.1715error: Invariant violated1716An example execution:17171718[State 0]1719{1720 schedNoFence::scheduler::cl: Map("c1" -> CIdle, "c2" -> CIdle),1721 schedNoFence::scheduler::crashes: 0,1722 schedNoFence::scheduler::entry: [],1723 schedNoFence::scheduler::free: Map("w1" -> 1, "w2" -> 1),1724 schedNoFence::scheduler::mAssigned: Set(),1725 schedNoFence::scheduler::mBuild: Set(),1726 schedNoFence::scheduler::mDone: Set(),1727 schedNoFence::scheduler::mExpect: Set(),1728 schedNoFence::scheduler::mResult: Set(),1729 schedNoFence::scheduler::mRetry: Set(),1730 schedNoFence::scheduler::mRevoke: Set(),1731 schedNoFence::scheduler::mSchedule: Set(),1732 schedNoFence::scheduler::published: 0,1733 schedNoFence::scheduler::publishedBy: Set(),1734 schedNoFence::scheduler::ws:1735 Map(1736 "w1" ->1737 {1738 attached: Set(),1739 built: false,1740 expecting: false,1741 running: false,1742 session: true,1743 up: true1744 },1745 "w2" ->1746 {1747 attached: Set(),1748 built: false,1749 expecting: false,1750 running: false,1751 session: true,1752 up: true1753 }1754 )1755}17561757[State 1]1758{1759 schedNoFence::scheduler::cl: Map("c1" -> CIdle, "c2" -> CQueued),1760 schedNoFence::scheduler::crashes: 0,1761 schedNoFence::scheduler::entry: [],1762 schedNoFence::scheduler::free: Map("w1" -> 1, "w2" -> 1),1763 schedNoFence::scheduler::mAssigned: Set(),1764 schedNoFence::scheduler::mBuild: Set(),1765 schedNoFence::scheduler::mDone: Set(),1766 schedNoFence::scheduler::mExpect: Set(),1767 schedNoFence::scheduler::mResult: Set(),1768 schedNoFence::scheduler::mRetry: Set(),1769 schedNoFence::scheduler::mRevoke: Set(),1770 schedNoFence::scheduler::mSchedule: Set("c2"),1771 schedNoFence::scheduler::published: 0,1772 schedNoFence::scheduler::publishedBy: Set(),1773 schedNoFence::scheduler::ws:1774 Map(1775 "w1" ->1776 {1777 attached: Set(),1778 built: false,1779 expecting: false,1780 running: false,1781 session: true,1782 up: true1783 },1784 "w2" ->1785 {1786 attached: Set(),1787 built: false,1788 expecting: false,1789 running: false,1790 session: true,1791 up: true1792 }1793 )1794}17951796[State 2]1797{1798 schedNoFence::scheduler::cl: Map("c1" -> CIdle, "c2" -> CQueued),1799 schedNoFence::scheduler::crashes: 0,1800 schedNoFence::scheduler::entry:1801 [{ followers: Set("c2"), leased: true, worker: "w1" }],1802 schedNoFence::scheduler::free: Map("w1" -> 0, "w2" -> 1),1803 schedNoFence::scheduler::mAssigned: Set(("c2", "w1")),1804 schedNoFence::scheduler::mBuild: Set(),1805 schedNoFence::scheduler::mDone: Set(),1806 schedNoFence::scheduler::mExpect: Set("w1"),1807 schedNoFence::scheduler::mResult: Set(),1808 schedNoFence::scheduler::mRetry: Set(),1809 schedNoFence::scheduler::mRevoke: Set(),1810 schedNoFence::scheduler::mSchedule: Set(),1811 schedNoFence::scheduler::published: 0,1812 schedNoFence::scheduler::publishedBy: Set(),1813 schedNoFence::scheduler::ws:1814 Map(1815 "w1" ->1816 {1817 attached: Set(),1818 built: false,1819 expecting: false,1820 running: false,1821 session: true,1822 up: true1823 },1824 "w2" ->1825 {1826 attached: Set(),1827 built: false,1828 expecting: false,1829 running: false,1830 session: true,1831 up: true1832 }1833 )1834}18351836[State 3]1837{1838 schedNoFence::scheduler::cl: Map("c1" -> CIdle, "c2" -> CQueued),1839 schedNoFence::scheduler::crashes: 0,1840 schedNoFence::scheduler::entry:1841 [{ followers: Set("c2"), leased: true, worker: "w1" }],1842 schedNoFence::scheduler::free: Map("w1" -> 0, "w2" -> 1),1843 schedNoFence::scheduler::mAssigned: Set(("c2", "w1")),1844 schedNoFence::scheduler::mBuild: Set(),1845 schedNoFence::scheduler::mDone: Set(),1846 schedNoFence::scheduler::mExpect: Set(),1847 schedNoFence::scheduler::mResult: Set(),1848 schedNoFence::scheduler::mRetry: Set(),1849 schedNoFence::scheduler::mRevoke: Set(),1850 schedNoFence::scheduler::mSchedule: Set(),1851 schedNoFence::scheduler::published: 0,1852 schedNoFence::scheduler::publishedBy: Set(),1853 schedNoFence::scheduler::ws:1854 Map(1855 "w1" ->1856 {1857 attached: Set(),1858 built: false,1859 expecting: true,1860 running: true,1861 session: true,1862 up: true1863 },1864 "w2" ->1865 {1866 attached: Set(),1867 built: false,1868 expecting: false,1869 running: false,1870 session: true,1871 up: true1872 }1873 )1874}18751876[State 4]1877{1878 schedNoFence::scheduler::cl: Map("c1" -> CIdle, "c2" -> CSent("w1")),1879 schedNoFence::scheduler::crashes: 0,1880 schedNoFence::scheduler::entry:1881 [{ followers: Set("c2"), leased: true, worker: "w1" }],1882 schedNoFence::scheduler::free: Map("w1" -> 0, "w2" -> 1),1883 schedNoFence::scheduler::mAssigned: Set(),1884 schedNoFence::scheduler::mBuild: Set(("c2", "w1")),1885 schedNoFence::scheduler::mDone: Set(),1886 schedNoFence::scheduler::mExpect: Set(),1887 schedNoFence::scheduler::mResult: Set(),1888 schedNoFence::scheduler::mRetry: Set(),1889 schedNoFence::scheduler::mRevoke: Set(),1890 schedNoFence::scheduler::mSchedule: Set(),1891 schedNoFence::scheduler::published: 0,1892 schedNoFence::scheduler::publishedBy: Set(),1893 schedNoFence::scheduler::ws:1894 Map(1895 "w1" ->1896 {1897 attached: Set(),1898 built: false,1899 expecting: true,1900 running: true,1901 session: true,1902 up: true1903 },1904 "w2" ->1905 {1906 attached: Set(),1907 built: false,1908 expecting: false,1909 running: false,1910 session: true,1911 up: true1912 }1913 )1914}19151916[State 5]1917{1918 schedNoFence::scheduler::cl: Map("c1" -> CIdle, "c2" -> CSent("w1")),1919 schedNoFence::scheduler::crashes: 1,1920 schedNoFence::scheduler::entry: [],1921 schedNoFence::scheduler::free: Map("w1" -> 1, "w2" -> 1),1922 schedNoFence::scheduler::mAssigned: Set(),1923 schedNoFence::scheduler::mBuild: Set(("c2", "w1")),1924 schedNoFence::scheduler::mDone: Set(),1925 schedNoFence::scheduler::mExpect: Set(),1926 schedNoFence::scheduler::mResult: Set(),1927 schedNoFence::scheduler::mRetry: Set(),1928 schedNoFence::scheduler::mRevoke: Set(),1929 schedNoFence::scheduler::mSchedule: Set(),1930 schedNoFence::scheduler::published: 0,1931 schedNoFence::scheduler::publishedBy: Set(),1932 schedNoFence::scheduler::ws:1933 Map(1934 "w1" ->1935 {1936 attached: Set(),1937 built: false,1938 expecting: true,1939 running: true,1940 session: false,1941 up: true1942 },1943 "w2" ->1944 {1945 attached: Set(),1946 built: false,1947 expecting: false,1948 running: false,1949 session: false,1950 up: true1951 }1952 )1953}19541955[State 6]1956{1957 schedNoFence::scheduler::cl: Map("c1" -> CIdle, "c2" -> CSent("w1")),1958 schedNoFence::scheduler::crashes: 2,1959 schedNoFence::scheduler::entry: [],1960 schedNoFence::scheduler::free: Map("w1" -> 1, "w2" -> 1),1961 schedNoFence::scheduler::mAssigned: Set(),1962 schedNoFence::scheduler::mBuild: Set(("c2", "w1")),1963 schedNoFence::scheduler::mDone: Set(),1964 schedNoFence::scheduler::mExpect: Set(),1965 schedNoFence::scheduler::mResult: Set(),1966 schedNoFence::scheduler::mRetry: Set(),1967 schedNoFence::scheduler::mRevoke: Set(),1968 schedNoFence::scheduler::mSchedule: Set(),1969 schedNoFence::scheduler::published: 0,1970 schedNoFence::scheduler::publishedBy: Set(),1971 schedNoFence::scheduler::ws:1972 Map(1973 "w1" ->1974 {1975 attached: Set(),1976 built: false,1977 expecting: true,1978 running: true,1979 session: false,1980 up: true1981 },1982 "w2" ->1983 {1984 attached: Set(),1985 built: false,1986 expecting: false,1987 running: false,1988 session: false,1989 up: false1990 }1991 )1992}19931994[State 7]1995{1996 schedNoFence::scheduler::cl: Map("c1" -> CIdle, "c2" -> CSent("w1")),1997 schedNoFence::scheduler::crashes: 2,1998 schedNoFence::scheduler::entry: [],1999 schedNoFence::scheduler::free: Map("w1" -> 1, "w2" -> 1),2000 schedNoFence::scheduler::mAssigned: Set(),2001 schedNoFence::scheduler::mBuild: Set(("c2", "w1")),2002 schedNoFence::scheduler::mDone: Set(),2003 schedNoFence::scheduler::mExpect: Set(),2004 schedNoFence::scheduler::mResult: Set(),2005 schedNoFence::scheduler::mRetry: Set(),2006 schedNoFence::scheduler::mRevoke: Set(),2007 schedNoFence::scheduler::mSchedule: Set(),2008 schedNoFence::scheduler::published: 0,2009 schedNoFence::scheduler::publishedBy: Set(),2010 schedNoFence::scheduler::ws:2011 Map(2012 "w1" ->2013 {2014 attached: Set(),2015 built: false,2016 expecting: true,2017 running: true,2018 session: false,2019 up: true2020 },2021 "w2" ->2022 {2023 attached: Set(),2024 built: false,2025 expecting: false,2026 running: false,2027 session: true,2028 up: true2029 }2030 )2031}20322033[State 8]2034{2035 schedNoFence::scheduler::cl: Map("c1" -> CQueued, "c2" -> CSent("w1")),2036 schedNoFence::scheduler::crashes: 2,2037 schedNoFence::scheduler::entry: [],2038 schedNoFence::scheduler::free: Map("w1" -> 1, "w2" -> 1),2039 schedNoFence::scheduler::mAssigned: Set(),2040 schedNoFence::scheduler::mBuild: Set(("c2", "w1")),2041 schedNoFence::scheduler::mDone: Set(),2042 schedNoFence::scheduler::mExpect: Set(),2043 schedNoFence::scheduler::mResult: Set(),2044 schedNoFence::scheduler::mRetry: Set(),2045 schedNoFence::scheduler::mRevoke: Set(),2046 schedNoFence::scheduler::mSchedule: Set("c1"),2047 schedNoFence::scheduler::published: 0,2048 schedNoFence::scheduler::publishedBy: Set(),2049 schedNoFence::scheduler::ws:2050 Map(2051 "w1" ->2052 {2053 attached: Set(),2054 built: false,2055 expecting: true,2056 running: true,2057 session: false,2058 up: true2059 },2060 "w2" ->2061 {2062 attached: Set(),2063 built: false,2064 expecting: false,2065 running: false,2066 session: true,2067 up: true2068 }2069 )2070}20712072[State 9]2073{2074 schedNoFence::scheduler::cl: Map("c1" -> CQueued, "c2" -> CSent("w1")),2075 schedNoFence::scheduler::crashes: 2,2076 schedNoFence::scheduler::entry:2077 [{ followers: Set("c1"), leased: true, worker: "w2" }],2078 schedNoFence::scheduler::free: Map("w1" -> 1, "w2" -> 0),2079 schedNoFence::scheduler::mAssigned: Set(("c1", "w2")),2080 schedNoFence::scheduler::mBuild: Set(("c2", "w1")),2081 schedNoFence::scheduler::mDone: Set(),2082 schedNoFence::scheduler::mExpect: Set("w2"),2083 schedNoFence::scheduler::mResult: Set(),2084 schedNoFence::scheduler::mRetry: Set(),2085 schedNoFence::scheduler::mRevoke: Set(),2086 schedNoFence::scheduler::mSchedule: Set(),2087 schedNoFence::scheduler::published: 0,2088 schedNoFence::scheduler::publishedBy: Set(),2089 schedNoFence::scheduler::ws:2090 Map(2091 "w1" ->2092 {2093 attached: Set(),2094 built: false,2095 expecting: true,2096 running: true,2097 session: false,2098 up: true2099 },2100 "w2" ->2101 {2102 attached: Set(),2103 built: false,2104 expecting: false,2105 running: false,2106 session: true,2107 up: true2108 }2109 )2110}21112112[State 10]2113{2114 schedNoFence::scheduler::cl: Map("c1" -> CQueued, "c2" -> CSent("w1")),2115 schedNoFence::scheduler::crashes: 2,2116 schedNoFence::scheduler::entry:2117 [{ followers: Set("c1"), leased: true, worker: "w2" }],2118 schedNoFence::scheduler::free: Map("w1" -> 1, "w2" -> 0),2119 schedNoFence::scheduler::mAssigned: Set(("c1", "w2")),2120 schedNoFence::scheduler::mBuild: Set(("c2", "w1")),2121 schedNoFence::scheduler::mDone: Set(),2122 schedNoFence::scheduler::mExpect: Set(),2123 schedNoFence::scheduler::mResult: Set(),2124 schedNoFence::scheduler::mRetry: Set(),2125 schedNoFence::scheduler::mRevoke: Set(),2126 schedNoFence::scheduler::mSchedule: Set(),2127 schedNoFence::scheduler::published: 0,2128 schedNoFence::scheduler::publishedBy: Set(),2129 schedNoFence::scheduler::ws:2130 Map(2131 "w1" ->2132 {2133 attached: Set(),2134 built: false,2135 expecting: true,2136 running: true,2137 session: false,2138 up: true2139 },2140 "w2" ->2141 {2142 attached: Set(),2143 built: false,2144 expecting: true,2145 running: true,2146 session: true,2147 up: true2148 }2149 )2150}21512152[State 11]2153{2154 schedNoFence::scheduler::cl: Map("c1" -> CQueued, "c2" -> CSent("w1")),2155 schedNoFence::scheduler::crashes: 2,2156 schedNoFence::scheduler::entry:2157 [{ followers: Set("c1"), leased: true, worker: "w2" }],2158 schedNoFence::scheduler::free: Map("w1" -> 1, "w2" -> 0),2159 schedNoFence::scheduler::mAssigned: Set(("c1", "w2")),2160 schedNoFence::scheduler::mBuild: Set(("c2", "w1")),2161 schedNoFence::scheduler::mDone: Set(),2162 schedNoFence::scheduler::mExpect: Set(),2163 schedNoFence::scheduler::mResult: Set(),2164 schedNoFence::scheduler::mRetry: Set(),2165 schedNoFence::scheduler::mRevoke: Set(),2166 schedNoFence::scheduler::mSchedule: Set(),2167 schedNoFence::scheduler::published: 1,2168 schedNoFence::scheduler::publishedBy: Set("w1"),2169 schedNoFence::scheduler::ws:2170 Map(2171 "w1" ->2172 {2173 attached: Set(),2174 built: true,2175 expecting: false,2176 running: false,2177 session: false,2178 up: true2179 },2180 "w2" ->2181 {2182 attached: Set(),2183 built: false,2184 expecting: true,2185 running: true,2186 session: true,2187 up: true2188 }2189 )2190}21912192[State 12]2193{2194 schedNoFence::scheduler::cl: Map("c1" -> CQueued, "c2" -> CSent("w1")),2195 schedNoFence::scheduler::crashes: 2,2196 schedNoFence::scheduler::entry:2197 [{ followers: Set("c1"), leased: true, worker: "w2" }],2198 schedNoFence::scheduler::free: Map("w1" -> 1, "w2" -> 0),2199 schedNoFence::scheduler::mAssigned: Set(("c1", "w2")),2200 schedNoFence::scheduler::mBuild: Set(("c2", "w1")),2201 schedNoFence::scheduler::mDone: Set("w2"),2202 schedNoFence::scheduler::mExpect: Set(),2203 schedNoFence::scheduler::mResult: Set(),2204 schedNoFence::scheduler::mRetry: Set(),2205 schedNoFence::scheduler::mRevoke: Set(),2206 schedNoFence::scheduler::mSchedule: Set(),2207 schedNoFence::scheduler::published: 2,2208 schedNoFence::scheduler::publishedBy: Set("w1", "w2"),2209 schedNoFence::scheduler::ws:2210 Map(2211 "w1" ->2212 {2213 attached: Set(),2214 built: true,2215 expecting: false,2216 running: false,2217 session: false,2218 up: true2219 },2220 "w2" ->2221 {2222 attached: Set(),2223 built: true,2224 expecting: false,2225 running: false,2226 session: true,2227 up: true2228 }2229 )2230}22312232[violation] Found an issue (482ms at 55786 traces/second).2233Use --verbosity=3 to show executions.2234Use --seed=0x87e6b69e8690be61 --backend=rust to reproduce.2235error: Invariant violated2236An example execution:22372238[State 0]2239{2240 schedNoPush::scheduler::cl: Map("c1" -> CIdle, "c2" -> CIdle),2241 schedNoPush::scheduler::crashes: 0,2242 schedNoPush::scheduler::entry: [],2243 schedNoPush::scheduler::free: Map("w1" -> 1, "w2" -> 1),2244 schedNoPush::scheduler::mAssigned: Set(),2245 schedNoPush::scheduler::mBuild: Set(),2246 schedNoPush::scheduler::mDone: Set(),2247 schedNoPush::scheduler::mExpect: Set(),2248 schedNoPush::scheduler::mResult: Set(),2249 schedNoPush::scheduler::mRetry: Set(),2250 schedNoPush::scheduler::mRevoke: Set(),2251 schedNoPush::scheduler::mSchedule: Set(),2252 schedNoPush::scheduler::published: 0,2253 schedNoPush::scheduler::publishedBy: Set(),2254 schedNoPush::scheduler::ws:2255 Map(2256 "w1" ->2257 {2258 attached: Set(),2259 built: false,2260 expecting: false,2261 running: false,2262 session: true,2263 up: true2264 },2265 "w2" ->2266 {2267 attached: Set(),2268 built: false,2269 expecting: false,2270 running: false,2271 session: true,2272 up: true2273 }2274 )2275}22762277[State 1]2278{2279 schedNoPush::scheduler::cl: Map("c1" -> CIdle, "c2" -> CQueued),2280 schedNoPush::scheduler::crashes: 0,2281 schedNoPush::scheduler::entry: [],2282 schedNoPush::scheduler::free: Map("w1" -> 1, "w2" -> 1),2283 schedNoPush::scheduler::mAssigned: Set(),2284 schedNoPush::scheduler::mBuild: Set(),2285 schedNoPush::scheduler::mDone: Set(),2286 schedNoPush::scheduler::mExpect: Set(),2287 schedNoPush::scheduler::mResult: Set(),2288 schedNoPush::scheduler::mRetry: Set(),2289 schedNoPush::scheduler::mRevoke: Set(),2290 schedNoPush::scheduler::mSchedule: Set("c2"),2291 schedNoPush::scheduler::published: 0,2292 schedNoPush::scheduler::publishedBy: Set(),2293 schedNoPush::scheduler::ws:2294 Map(2295 "w1" ->2296 {2297 attached: Set(),2298 built: false,2299 expecting: false,2300 running: false,2301 session: true,2302 up: true2303 },2304 "w2" ->2305 {2306 attached: Set(),2307 built: false,2308 expecting: false,2309 running: false,2310 session: true,2311 up: true2312 }2313 )2314}23152316[State 2]2317{2318 schedNoPush::scheduler::cl: Map("c1" -> CIdle, "c2" -> CQueued),2319 schedNoPush::scheduler::crashes: 0,2320 schedNoPush::scheduler::entry:2321 [{ followers: Set("c2"), leased: true, worker: "w2" }],2322 schedNoPush::scheduler::free: Map("w1" -> 1, "w2" -> 0),2323 schedNoPush::scheduler::mAssigned: Set(("c2", "w2")),2324 schedNoPush::scheduler::mBuild: Set(),2325 schedNoPush::scheduler::mDone: Set(),2326 schedNoPush::scheduler::mExpect: Set(),2327 schedNoPush::scheduler::mResult: Set(),2328 schedNoPush::scheduler::mRetry: Set(),2329 schedNoPush::scheduler::mRevoke: Set(),2330 schedNoPush::scheduler::mSchedule: Set(),2331 schedNoPush::scheduler::published: 0,2332 schedNoPush::scheduler::publishedBy: Set(),2333 schedNoPush::scheduler::ws:2334 Map(2335 "w1" ->2336 {2337 attached: Set(),2338 built: false,2339 expecting: false,2340 running: false,2341 session: true,2342 up: true2343 },2344 "w2" ->2345 {2346 attached: Set(),2347 built: false,2348 expecting: false,2349 running: false,2350 session: true,2351 up: true2352 }2353 )2354}23552356[State 3]2357{2358 schedNoPush::scheduler::cl: Map("c1" -> CIdle, "c2" -> CSent("w2")),2359 schedNoPush::scheduler::crashes: 0,2360 schedNoPush::scheduler::entry:2361 [{ followers: Set("c2"), leased: true, worker: "w2" }],2362 schedNoPush::scheduler::free: Map("w1" -> 1, "w2" -> 0),2363 schedNoPush::scheduler::mAssigned: Set(),2364 schedNoPush::scheduler::mBuild: Set(("c2", "w2")),2365 schedNoPush::scheduler::mDone: Set(),2366 schedNoPush::scheduler::mExpect: Set(),2367 schedNoPush::scheduler::mResult: Set(),2368 schedNoPush::scheduler::mRetry: Set(),2369 schedNoPush::scheduler::mRevoke: Set(),2370 schedNoPush::scheduler::mSchedule: Set(),2371 schedNoPush::scheduler::published: 0,2372 schedNoPush::scheduler::publishedBy: Set(),2373 schedNoPush::scheduler::ws:2374 Map(2375 "w1" ->2376 {2377 attached: Set(),2378 built: false,2379 expecting: false,2380 running: false,2381 session: true,2382 up: true2383 },2384 "w2" ->2385 {2386 attached: Set(),2387 built: false,2388 expecting: false,2389 running: false,2390 session: true,2391 up: true2392 }2393 )2394}23952396[State 4]2397{2398 schedNoPush::scheduler::cl: Map("c1" -> CIdle, "c2" -> CSent("w2")),2399 schedNoPush::scheduler::crashes: 1,2400 schedNoPush::scheduler::entry:2401 [{ followers: Set("c2"), leased: true, worker: "w2" }],2402 schedNoPush::scheduler::free: Map("w1" -> 1, "w2" -> 0),2403 schedNoPush::scheduler::mAssigned: Set(),2404 schedNoPush::scheduler::mBuild: Set(("c2", "w2")),2405 schedNoPush::scheduler::mDone: Set(),2406 schedNoPush::scheduler::mExpect: Set(),2407 schedNoPush::scheduler::mResult: Set(),2408 schedNoPush::scheduler::mRetry: Set(),2409 schedNoPush::scheduler::mRevoke: Set(),2410 schedNoPush::scheduler::mSchedule: Set(),2411 schedNoPush::scheduler::published: 0,2412 schedNoPush::scheduler::publishedBy: Set(),2413 schedNoPush::scheduler::ws:2414 Map(2415 "w1" ->2416 {2417 attached: Set(),2418 built: false,2419 expecting: false,2420 running: false,2421 session: true,2422 up: true2423 },2424 "w2" ->2425 {2426 attached: Set(),2427 built: false,2428 expecting: false,2429 running: false,2430 session: false,2431 up: false2432 }2433 )2434}24352436[State 5]2437{2438 schedNoPush::scheduler::cl: Map("c1" -> CIdle, "c2" -> CSent("w2")),2439 schedNoPush::scheduler::crashes: 1,2440 schedNoPush::scheduler::entry: [],2441 schedNoPush::scheduler::free: Map("w1" -> 1, "w2" -> 1),2442 schedNoPush::scheduler::mAssigned: Set(),2443 schedNoPush::scheduler::mBuild: Set(("c2", "w2")),2444 schedNoPush::scheduler::mDone: Set(),2445 schedNoPush::scheduler::mExpect: Set(),2446 schedNoPush::scheduler::mResult: Set(),2447 schedNoPush::scheduler::mRetry: Set("c2"),2448 schedNoPush::scheduler::mRevoke: Set(),2449 schedNoPush::scheduler::mSchedule: Set(),2450 schedNoPush::scheduler::published: 0,2451 schedNoPush::scheduler::publishedBy: Set(),2452 schedNoPush::scheduler::ws:2453 Map(2454 "w1" ->2455 {2456 attached: Set(),2457 built: false,2458 expecting: false,2459 running: false,2460 session: true,2461 up: true2462 },2463 "w2" ->2464 {2465 attached: Set(),2466 built: false,2467 expecting: false,2468 running: false,2469 session: true,2470 up: true2471 }2472 )2473}24742475[State 6]2476{2477 schedNoPush::scheduler::cl: Map("c1" -> CIdle, "c2" -> CSent("w2")),2478 schedNoPush::scheduler::crashes: 1,2479 schedNoPush::scheduler::entry: [],2480 schedNoPush::scheduler::free: Map("w1" -> 1, "w2" -> 1),2481 schedNoPush::scheduler::mAssigned: Set(),2482 schedNoPush::scheduler::mBuild: Set(),2483 schedNoPush::scheduler::mDone: Set(),2484 schedNoPush::scheduler::mExpect: Set(),2485 schedNoPush::scheduler::mResult: Set(),2486 schedNoPush::scheduler::mRetry: Set("c2"),2487 schedNoPush::scheduler::mRevoke: Set(),2488 schedNoPush::scheduler::mSchedule: Set(),2489 schedNoPush::scheduler::published: 0,2490 schedNoPush::scheduler::publishedBy: Set(),2491 schedNoPush::scheduler::ws:2492 Map(2493 "w1" ->2494 {2495 attached: Set(),2496 built: false,2497 expecting: false,2498 running: false,2499 session: true,2500 up: true2501 },2502 "w2" ->2503 {2504 attached: Set("c2"),2505 built: false,2506 expecting: true,2507 running: true,2508 session: true,2509 up: true2510 }2511 )2512}25132514[violation] Found an issue (447ms at 40038 traces/second).2515Use --verbosity=3 to show executions.2516Use --seed=0xe4532a84a8f30f2c --backend=rust to reproduce.2517error: Invariant violated2518An example execution:25192520[State 0]2521{2522 schedNoReport::scheduler::cl: Map("c1" -> CIdle, "c2" -> CIdle),2523 schedNoReport::scheduler::crashes: 0,2524 schedNoReport::scheduler::entry: [],2525 schedNoReport::scheduler::free: Map("w1" -> 1, "w2" -> 1),2526 schedNoReport::scheduler::mAssigned: Set(),2527 schedNoReport::scheduler::mBuild: Set(),2528 schedNoReport::scheduler::mDone: Set(),2529 schedNoReport::scheduler::mExpect: Set(),2530 schedNoReport::scheduler::mResult: Set(),2531 schedNoReport::scheduler::mRetry: Set(),2532 schedNoReport::scheduler::mRevoke: Set(),2533 schedNoReport::scheduler::mSchedule: Set(),2534 schedNoReport::scheduler::published: 0,2535 schedNoReport::scheduler::publishedBy: Set(),2536 schedNoReport::scheduler::ws:2537 Map(2538 "w1" ->2539 {2540 attached: Set(),2541 built: false,2542 expecting: false,2543 running: false,2544 session: true,2545 up: true2546 },2547 "w2" ->2548 {2549 attached: Set(),2550 built: false,2551 expecting: false,2552 running: false,2553 session: true,2554 up: true2555 }2556 )2557}25582559[State 1]2560{2561 schedNoReport::scheduler::cl: Map("c1" -> CQueued, "c2" -> CIdle),2562 schedNoReport::scheduler::crashes: 0,2563 schedNoReport::scheduler::entry: [],2564 schedNoReport::scheduler::free: Map("w1" -> 1, "w2" -> 1),2565 schedNoReport::scheduler::mAssigned: Set(),2566 schedNoReport::scheduler::mBuild: Set(),2567 schedNoReport::scheduler::mDone: Set(),2568 schedNoReport::scheduler::mExpect: Set(),2569 schedNoReport::scheduler::mResult: Set(),2570 schedNoReport::scheduler::mRetry: Set(),2571 schedNoReport::scheduler::mRevoke: Set(),2572 schedNoReport::scheduler::mSchedule: Set("c1"),2573 schedNoReport::scheduler::published: 0,2574 schedNoReport::scheduler::publishedBy: Set(),2575 schedNoReport::scheduler::ws:2576 Map(2577 "w1" ->2578 {2579 attached: Set(),2580 built: false,2581 expecting: false,2582 running: false,2583 session: true,2584 up: true2585 },2586 "w2" ->2587 {2588 attached: Set(),2589 built: false,2590 expecting: false,2591 running: false,2592 session: true,2593 up: true2594 }2595 )2596}25972598[State 2]2599{2600 schedNoReport::scheduler::cl: Map("c1" -> CQueued, "c2" -> CIdle),2601 schedNoReport::scheduler::crashes: 1,2602 schedNoReport::scheduler::entry: [],2603 schedNoReport::scheduler::free: Map("w1" -> 1, "w2" -> 1),2604 schedNoReport::scheduler::mAssigned: Set(),2605 schedNoReport::scheduler::mBuild: Set(),2606 schedNoReport::scheduler::mDone: Set(),2607 schedNoReport::scheduler::mExpect: Set(),2608 schedNoReport::scheduler::mResult: Set(),2609 schedNoReport::scheduler::mRetry: Set(),2610 schedNoReport::scheduler::mRevoke: Set(),2611 schedNoReport::scheduler::mSchedule: Set("c1"),2612 schedNoReport::scheduler::published: 0,2613 schedNoReport::scheduler::publishedBy: Set(),2614 schedNoReport::scheduler::ws:2615 Map(2616 "w1" ->2617 {2618 attached: Set(),2619 built: false,2620 expecting: false,2621 running: false,2622 session: false,2623 up: false2624 },2625 "w2" ->2626 {2627 attached: Set(),2628 built: false,2629 expecting: false,2630 running: false,2631 session: true,2632 up: true2633 }2634 )2635}26362637[State 3]2638{2639 schedNoReport::scheduler::cl: Map("c1" -> CQueued, "c2" -> CIdle),2640 schedNoReport::scheduler::crashes: 1,2641 schedNoReport::scheduler::entry:2642 [{ followers: Set("c1"), leased: true, worker: "w2" }],2643 schedNoReport::scheduler::free: Map("w1" -> 1, "w2" -> 0),2644 schedNoReport::scheduler::mAssigned: Set(("c1", "w2")),2645 schedNoReport::scheduler::mBuild: Set(),2646 schedNoReport::scheduler::mDone: Set(),2647 schedNoReport::scheduler::mExpect: Set("w2"),2648 schedNoReport::scheduler::mResult: Set(),2649 schedNoReport::scheduler::mRetry: Set(),2650 schedNoReport::scheduler::mRevoke: Set(),2651 schedNoReport::scheduler::mSchedule: Set(),2652 schedNoReport::scheduler::published: 0,2653 schedNoReport::scheduler::publishedBy: Set(),2654 schedNoReport::scheduler::ws:2655 Map(2656 "w1" ->2657 {2658 attached: Set(),2659 built: false,2660 expecting: false,2661 running: false,2662 session: false,2663 up: false2664 },2665 "w2" ->2666 {2667 attached: Set(),2668 built: false,2669 expecting: false,2670 running: false,2671 session: true,2672 up: true2673 }2674 )2675}26762677[State 4]2678{2679 schedNoReport::scheduler::cl: Map("c1" -> CQueued, "c2" -> CIdle),2680 schedNoReport::scheduler::crashes: 1,2681 schedNoReport::scheduler::entry:2682 [{ followers: Set("c1"), leased: true, worker: "w2" }],2683 schedNoReport::scheduler::free: Map("w1" -> 1, "w2" -> 0),2684 schedNoReport::scheduler::mAssigned: Set(("c1", "w2")),2685 schedNoReport::scheduler::mBuild: Set(),2686 schedNoReport::scheduler::mDone: Set(),2687 schedNoReport::scheduler::mExpect: Set(),2688 schedNoReport::scheduler::mResult: Set(),2689 schedNoReport::scheduler::mRetry: Set(),2690 schedNoReport::scheduler::mRevoke: Set(),2691 schedNoReport::scheduler::mSchedule: Set(),2692 schedNoReport::scheduler::published: 0,2693 schedNoReport::scheduler::publishedBy: Set(),2694 schedNoReport::scheduler::ws:2695 Map(2696 "w1" ->2697 {2698 attached: Set(),2699 built: false,2700 expecting: false,2701 running: false,2702 session: false,2703 up: false2704 },2705 "w2" ->2706 {2707 attached: Set(),2708 built: false,2709 expecting: true,2710 running: true,2711 session: true,2712 up: true2713 }2714 )2715}27162717[State 5]2718{2719 schedNoReport::scheduler::cl: Map("c1" -> CQueued, "c2" -> CIdle),2720 schedNoReport::scheduler::crashes: 2,2721 schedNoReport::scheduler::entry: [],2722 schedNoReport::scheduler::free: Map("w1" -> 1, "w2" -> 1),2723 schedNoReport::scheduler::mAssigned: Set(),2724 schedNoReport::scheduler::mBuild: Set(),2725 schedNoReport::scheduler::mDone: Set(),2726 schedNoReport::scheduler::mExpect: Set(),2727 schedNoReport::scheduler::mResult: Set(),2728 schedNoReport::scheduler::mRetry: Set("c1"),2729 schedNoReport::scheduler::mRevoke: Set(),2730 schedNoReport::scheduler::mSchedule: Set(),2731 schedNoReport::scheduler::published: 0,2732 schedNoReport::scheduler::publishedBy: Set(),2733 schedNoReport::scheduler::ws:2734 Map(2735 "w1" ->2736 {2737 attached: Set(),2738 built: false,2739 expecting: false,2740 running: false,2741 session: false,2742 up: false2743 },2744 "w2" ->2745 {2746 attached: Set(),2747 built: false,2748 expecting: true,2749 running: true,2750 session: false,2751 up: true2752 }2753 )2754}27552756[State 6]2757{2758 schedNoReport::scheduler::cl: Map("c1" -> CQueued, "c2" -> CIdle),2759 schedNoReport::scheduler::crashes: 2,2760 schedNoReport::scheduler::entry: [],2761 schedNoReport::scheduler::free: Map("w1" -> 1, "w2" -> 1),2762 schedNoReport::scheduler::mAssigned: Set(),2763 schedNoReport::scheduler::mBuild: Set(),2764 schedNoReport::scheduler::mDone: Set(),2765 schedNoReport::scheduler::mExpect: Set(),2766 schedNoReport::scheduler::mResult: Set(),2767 schedNoReport::scheduler::mRetry: Set("c1"),2768 schedNoReport::scheduler::mRevoke: Set(),2769 schedNoReport::scheduler::mSchedule: Set(),2770 schedNoReport::scheduler::published: 0,2771 schedNoReport::scheduler::publishedBy: Set(),2772 schedNoReport::scheduler::ws:2773 Map(2774 "w1" ->2775 {2776 attached: Set(),2777 built: false,2778 expecting: false,2779 running: false,2780 session: true,2781 up: true2782 },2783 "w2" ->2784 {2785 attached: Set(),2786 built: false,2787 expecting: true,2788 running: true,2789 session: false,2790 up: true2791 }2792 )2793}27942795[State 7]2796{2797 schedNoReport::scheduler::cl: Map("c1" -> CQueued, "c2" -> CIdle),2798 schedNoReport::scheduler::crashes: 2,2799 schedNoReport::scheduler::entry: [],2800 schedNoReport::scheduler::free: Map("w1" -> 1, "w2" -> 1),2801 schedNoReport::scheduler::mAssigned: Set(),2802 schedNoReport::scheduler::mBuild: Set(),2803 schedNoReport::scheduler::mDone: Set(),2804 schedNoReport::scheduler::mExpect: Set(),2805 schedNoReport::scheduler::mResult: Set(),2806 schedNoReport::scheduler::mRetry: Set(),2807 schedNoReport::scheduler::mRevoke: Set(),2808 schedNoReport::scheduler::mSchedule: Set("c1"),2809 schedNoReport::scheduler::published: 0,2810 schedNoReport::scheduler::publishedBy: Set(),2811 schedNoReport::scheduler::ws:2812 Map(2813 "w1" ->2814 {2815 attached: Set(),2816 built: false,2817 expecting: false,2818 running: false,2819 session: true,2820 up: true2821 },2822 "w2" ->2823 {2824 attached: Set(),2825 built: false,2826 expecting: true,2827 running: true,2828 session: false,2829 up: true2830 }2831 )2832}28332834[State 8]2835{2836 schedNoReport::scheduler::cl: Map("c1" -> CQueued, "c2" -> CIdle),2837 schedNoReport::scheduler::crashes: 2,2838 schedNoReport::scheduler::entry: [],2839 schedNoReport::scheduler::free: Map("w1" -> 1, "w2" -> 1),2840 schedNoReport::scheduler::mAssigned: Set(),2841 schedNoReport::scheduler::mBuild: Set(),2842 schedNoReport::scheduler::mDone: Set(),2843 schedNoReport::scheduler::mExpect: Set(),2844 schedNoReport::scheduler::mResult: Set(),2845 schedNoReport::scheduler::mRetry: Set(),2846 schedNoReport::scheduler::mRevoke: Set(),2847 schedNoReport::scheduler::mSchedule: Set("c1"),2848 schedNoReport::scheduler::published: 0,2849 schedNoReport::scheduler::publishedBy: Set(),2850 schedNoReport::scheduler::ws:2851 Map(2852 "w1" ->2853 {2854 attached: Set(),2855 built: false,2856 expecting: false,2857 running: false,2858 session: true,2859 up: true2860 },2861 "w2" ->2862 {2863 attached: Set(),2864 built: false,2865 expecting: true,2866 running: true,2867 session: true,2868 up: true2869 }2870 )2871}28722873[State 9]2874{2875 schedNoReport::scheduler::cl: Map("c1" -> CQueued, "c2" -> CIdle),2876 schedNoReport::scheduler::crashes: 2,2877 schedNoReport::scheduler::entry:2878 [{ followers: Set("c1"), leased: true, worker: "w1" }],2879 schedNoReport::scheduler::free: Map("w1" -> 0, "w2" -> 1),2880 schedNoReport::scheduler::mAssigned: Set(("c1", "w1")),2881 schedNoReport::scheduler::mBuild: Set(),2882 schedNoReport::scheduler::mDone: Set(),2883 schedNoReport::scheduler::mExpect: Set("w1"),2884 schedNoReport::scheduler::mResult: Set(),2885 schedNoReport::scheduler::mRetry: Set(),2886 schedNoReport::scheduler::mRevoke: Set(),2887 schedNoReport::scheduler::mSchedule: Set(),2888 schedNoReport::scheduler::published: 0,2889 schedNoReport::scheduler::publishedBy: Set(),2890 schedNoReport::scheduler::ws:2891 Map(2892 "w1" ->2893 {2894 attached: Set(),2895 built: false,2896 expecting: false,2897 running: false,2898 session: true,2899 up: true2900 },2901 "w2" ->2902 {2903 attached: Set(),2904 built: false,2905 expecting: true,2906 running: true,2907 session: true,2908 up: true2909 }2910 )2911}29122913[State 10]2914{2915 schedNoReport::scheduler::cl: Map("c1" -> CQueued, "c2" -> CIdle),2916 schedNoReport::scheduler::crashes: 2,2917 schedNoReport::scheduler::entry:2918 [{ followers: Set("c1"), leased: true, worker: "w1" }],2919 schedNoReport::scheduler::free: Map("w1" -> 0, "w2" -> 1),2920 schedNoReport::scheduler::mAssigned: Set(("c1", "w1")),2921 schedNoReport::scheduler::mBuild: Set(),2922 schedNoReport::scheduler::mDone: Set(),2923 schedNoReport::scheduler::mExpect: Set(),2924 schedNoReport::scheduler::mResult: Set(),2925 schedNoReport::scheduler::mRetry: Set(),2926 schedNoReport::scheduler::mRevoke: Set(),2927 schedNoReport::scheduler::mSchedule: Set(),2928 schedNoReport::scheduler::published: 0,2929 schedNoReport::scheduler::publishedBy: Set(),2930 schedNoReport::scheduler::ws:2931 Map(2932 "w1" ->2933 {2934 attached: Set(),2935 built: false,2936 expecting: true,2937 running: true,2938 session: true,2939 up: true2940 },2941 "w2" ->2942 {2943 attached: Set(),2944 built: false,2945 expecting: true,2946 running: true,2947 session: true,2948 up: true2949 }2950 )2951}29522953[violation] Found an issue (505ms at 50964 traces/second).2954Use --verbosity=3 to show executions.2955Use --seed=0xab56cd1d6fd62f4 --backend=rust to reproduce.2956error: Invariant violated2957An example execution:29582959[State 0]2960{2961 schedTerminal::scheduler::cl: Map("c1" -> CIdle, "c2" -> CIdle),2962 schedTerminal::scheduler::crashes: 0,2963 schedTerminal::scheduler::entry: [],2964 schedTerminal::scheduler::free: Map("w1" -> 1, "w2" -> 1),2965 schedTerminal::scheduler::mAssigned: Set(),2966 schedTerminal::scheduler::mBuild: Set(),2967 schedTerminal::scheduler::mDone: Set(),2968 schedTerminal::scheduler::mExpect: Set(),2969 schedTerminal::scheduler::mResult: Set(),2970 schedTerminal::scheduler::mRetry: Set(),2971 schedTerminal::scheduler::mRevoke: Set(),2972 schedTerminal::scheduler::mSchedule: Set(),2973 schedTerminal::scheduler::published: 0,2974 schedTerminal::scheduler::publishedBy: Set(),2975 schedTerminal::scheduler::ws:2976 Map(2977 "w1" ->2978 {2979 attached: Set(),2980 built: false,2981 expecting: false,2982 running: false,2983 session: true,2984 up: true2985 },2986 "w2" ->2987 {2988 attached: Set(),2989 built: false,2990 expecting: false,2991 running: false,2992 session: true,2993 up: true2994 }2995 )2996}29972998[State 1]2999{3000 schedTerminal::scheduler::cl: Map("c1" -> CIdle, "c2" -> CIdle),3001 schedTerminal::scheduler::crashes: 1,3002 schedTerminal::scheduler::entry: [],3003 schedTerminal::scheduler::free: Map("w1" -> 1, "w2" -> 1),3004 schedTerminal::scheduler::mAssigned: Set(),3005 schedTerminal::scheduler::mBuild: Set(),3006 schedTerminal::scheduler::mDone: Set(),3007 schedTerminal::scheduler::mExpect: Set(),3008 schedTerminal::scheduler::mResult: Set(),3009 schedTerminal::scheduler::mRetry: Set(),3010 schedTerminal::scheduler::mRevoke: Set(),3011 schedTerminal::scheduler::mSchedule: Set(),3012 schedTerminal::scheduler::published: 0,3013 schedTerminal::scheduler::publishedBy: Set(),3014 schedTerminal::scheduler::ws:3015 Map(3016 "w1" ->3017 {3018 attached: Set(),3019 built: false,3020 expecting: false,3021 running: false,3022 session: false,3023 up: true3024 },3025 "w2" ->3026 {3027 attached: Set(),3028 built: false,3029 expecting: false,3030 running: false,3031 session: false,3032 up: true3033 }3034 )3035}30363037[State 2]3038{3039 schedTerminal::scheduler::cl: Map("c1" -> CQueued, "c2" -> CIdle),3040 schedTerminal::scheduler::crashes: 1,3041 schedTerminal::scheduler::entry: [],3042 schedTerminal::scheduler::free: Map("w1" -> 1, "w2" -> 1),3043 schedTerminal::scheduler::mAssigned: Set(),3044 schedTerminal::scheduler::mBuild: Set(),3045 schedTerminal::scheduler::mDone: Set(),3046 schedTerminal::scheduler::mExpect: Set(),3047 schedTerminal::scheduler::mResult: Set(),3048 schedTerminal::scheduler::mRetry: Set(),3049 schedTerminal::scheduler::mRevoke: Set(),3050 schedTerminal::scheduler::mSchedule: Set("c1"),3051 schedTerminal::scheduler::published: 0,3052 schedTerminal::scheduler::publishedBy: Set(),3053 schedTerminal::scheduler::ws:3054 Map(3055 "w1" ->3056 {3057 attached: Set(),3058 built: false,3059 expecting: false,3060 running: false,3061 session: false,3062 up: true3063 },3064 "w2" ->3065 {3066 attached: Set(),3067 built: false,3068 expecting: false,3069 running: false,3070 session: false,3071 up: true3072 }3073 )3074}30753076[State 3]3077{3078 schedTerminal::scheduler::cl: Map("c1" -> CFailed, "c2" -> CIdle),3079 schedTerminal::scheduler::crashes: 1,3080 schedTerminal::scheduler::entry: [],3081 schedTerminal::scheduler::free: Map("w1" -> 1, "w2" -> 1),3082 schedTerminal::scheduler::mAssigned: Set(),3083 schedTerminal::scheduler::mBuild: Set(),3084 schedTerminal::scheduler::mDone: Set(),3085 schedTerminal::scheduler::mExpect: Set(),3086 schedTerminal::scheduler::mResult: Set(),3087 schedTerminal::scheduler::mRetry: Set(),3088 schedTerminal::scheduler::mRevoke: Set(),3089 schedTerminal::scheduler::mSchedule: Set(),3090 schedTerminal::scheduler::published: 0,3091 schedTerminal::scheduler::publishedBy: Set(),3092 schedTerminal::scheduler::ws:3093 Map(3094 "w1" ->3095 {3096 attached: Set(),3097 built: false,3098 expecting: false,3099 running: false,3100 session: false,3101 up: true3102 },3103 "w2" ->3104 {3105 attached: Set(),3106 built: false,3107 expecting: false,3108 running: false,3109 session: false,3110 up: true3111 }3112 )3113}31143115[violation] Found an issue (354ms at 5605 traces/second).3116Use --verbosity=3 to show executions.3117Use --seed=0xad5d4232a03d691a --backend=rust to reproduce.3118error: Invariant violated3119An example execution:31203121[State 0]3122{3123 pushFixed::push::byPath: Map(),3124 pushFixed::push::inflight: Set(),3125 pushFixed::push::left: Map(),3126 pushFixed::push::sent: Map()3127}31283129[State 1]3130{3131 pushFixed::push::byPath: Map("a" -> 3, "b" -> 3),3132 pushFixed::push::inflight: Set((3, "a"), (3, "b")),3133 pushFixed::push::left: Map(3 -> 2),3134 pushFixed::push::sent: Map(3 -> Set("a", "b"))3135}31363137[State 2]3138{3139 pushFixed::push::byPath: Map("a" -> 3, "b" -> 3),3140 pushFixed::push::inflight: Set((3, "a")),3141 pushFixed::push::left: Map(3 -> 1),3142 pushFixed::push::sent: Map(3 -> Set("a", "b"))3143}31443145[State 3]3146{3147 pushFixed::push::byPath: Map("a" -> 3, "b" -> 3),3148 pushFixed::push::inflight: Set(),3149 pushFixed::push::left: Map(3 -> 0),3150 pushFixed::push::sent: Map(3 -> Set("a", "b"))3151}31523153[State 4]3154{3155 pushFixed::push::byPath: Map("a" -> 2, "b" -> 2),3156 pushFixed::push::inflight: Set((2, "a"), (2, "b")),3157 pushFixed::push::left: Map(2 -> 2, 3 -> 0),3158 pushFixed::push::sent: Map(2 -> Set("a", "b"), 3 -> Set("a", "b"))3159}31603161[State 5]3162{3163 pushFixed::push::byPath: Map("a" -> 1, "b" -> 1),3164 pushFixed::push::inflight: Set((1, "a"), (1, "b"), (2, "a"), (2, "b")),3165 pushFixed::push::left: Map(1 -> 2, 2 -> 2, 3 -> 0),3166 pushFixed::push::sent:3167 Map(1 -> Set("a", "b"), 2 -> Set("a", "b"), 3 -> Set("a", "b"))3168}31693170[State 6]3171{3172 pushFixed::push::byPath: Map("a" -> 1, "b" -> 1),3173 pushFixed::push::inflight: Set((1, "b"), (2, "a"), (2, "b")),3174 pushFixed::push::left: Map(1 -> 1, 2 -> 2, 3 -> 0),3175 pushFixed::push::sent:3176 Map(1 -> Set("a", "b"), 2 -> Set("a", "b"), 3 -> Set("a", "b"))3177}31783179[State 7]3180{3181 pushFixed::push::byPath: Map("a" -> 1, "b" -> 1),3182 pushFixed::push::inflight: Set((1, "b"), (2, "a")),3183 pushFixed::push::left: Map(1 -> 1, 2 -> 1, 3 -> 0),3184 pushFixed::push::sent:3185 Map(1 -> Set("a", "b"), 2 -> Set("a", "b"), 3 -> Set("a", "b"))3186}31873188[State 8]3189{3190 pushFixed::push::byPath: Map("a" -> 1, "b" -> 1),3191 pushFixed::push::inflight: Set((1, "b")),3192 pushFixed::push::left: Map(1 -> 1, 2 -> 0, 3 -> 0),3193 pushFixed::push::sent:3194 Map(1 -> Set("a", "b"), 2 -> Set("a", "b"), 3 -> Set("a", "b"))3195}31963197[State 9]3198{3199 pushFixed::push::byPath: Map("a" -> 1, "b" -> 1),3200 pushFixed::push::inflight: Set(),3201 pushFixed::push::left: Map(1 -> 0, 2 -> 0, 3 -> 0),3202 pushFixed::push::sent:3203 Map(1 -> Set("a", "b"), 2 -> Set("a", "b"), 3 -> Set("a", "b"))3204}32053206[ok] No violation found (139ms at 143885 traces/second).3207Trace length statistics: max=10, min=7, average=7.963208You may increase --max-samples and --max-steps.3209Use --verbosity to produce more (or less) output.3210Use --seed=0x840b38e3ca6ab341 --backend=rust to reproduce.