model: AgentCallAdapter.tla sha256=8aad397e395b92d62a94f0333993e3cfd8230f63a508c66fa4ea344cd18a8fee
tla2tools: sha256=0f56d6a813368c48008dfbecb23a73ab43a4a5e1bf09f026782a674aa9d4b3c9
AgentCallAdapter_design cfg_sha256=fd519c9a1022967359f759267ddcc906468ee750f3c205a22b29150bbc124f0e out_sha256=0cf0f3c692005053817fc3152820b9df960a3e76bb116d4935fb0e282d7f769e result=PASS
M1_no_fencing cfg_sha256=af8f3a2cdc30fb81ce48d438ad7ec23b002e896717a7cf602354cd24fc8f32df out_sha256=767bcf0ad714377501d2908ad0c8cec34739cc6452e54c67cbc358c29cc3eda5 result=VIOLATED AtMostOneDispatchPerClientCall
M2_dispatch_before_intent cfg_sha256=5c3b9e212d102d10fa7bd5ea74afaccd1baafa4046b980a958b6eb42e50a9fbd out_sha256=b21c371c2c120fb777aa7b15e3070d86043ac0d56aa8602191ffcbcb64c084ee result=VIOLATED AtMostOneDispatchPerClientCall
M3_blind_upsert cfg_sha256=f65975a522b589aefc9660cfb8966ad997f3297c8ecaec21e1f3dfb830551f21 out_sha256=4a94b93bbc65eddb4fa698bf972de91f74c532dd1dc4a3928934108efa0cccb7 result=VIOLATED AtMostOneDispatchPerClientCall
M4_reconcile_redispatch cfg_sha256=122d9580adf1a70ef9c7be2b5b032597cee7f26cc1ddfeb125f3e807010db10b out_sha256=a3c6da6e557ebfd9731dfc808fa32e6b9d41515bc6332fd411812be4654b8f22 result=VIOLATED AtMostOneDispatchPerClientCall
M5_corr_from_key cfg_sha256=e92e44322d8bb70f671b565eae6cd677a3b26b3eae0040e513817c083e1e6490 out_sha256=af89bcd164a2cc710a9dea1d4491801dc723332cdbab7fad2cb008f9fb64ea97 result=VIOLATED ConflictNeverReachesOriginal
M6_echo_before_commit cfg_sha256=0cc6e6001d4903b5c40e06924dfc48fdcda9c66c85a16a4e9a808e8998e8303b out_sha256=811348747c628ed59c6620af80db8ece14bd86be7f44fd3e1a805a0218130533 result=VIOLATED NativeOnlyWhenConfirmedNotDispatched
M7_server_mode_wins cfg_sha256=94cea40e41cb5d86bc2844ec099ee5f45d3f6e20d681afb622b031ce41e6f427 out_sha256=5cc7ef54594b6ecb9391e3e1ba7de2f2322fff6fe062b3d74c76b7bf485d0df6 result=VIOLATED ObserveNeverDispatches
M8_native_on_unknown cfg_sha256=fd1840c5c43e171bf7e0f9ae46d828cd89e300dbce7dd9ad3dab90f358d61417 out_sha256=e4af1f1ebc9485a7013e07211785aadb18de302b812aaf70790e1be0079cf0c0 result=VIOLATED NativeOnlyWhenConfirmedNotDispatched
M9_binding_fail_open cfg_sha256=402a5046fce364de56afcd896d0ad2a1554c87566be00dcc999a13e7d1047f1d out_sha256=f8065501b5f7ea4d63340f1af8a58c77d3b78b5ed3d4345a0fe87fb07523559f result=VIOLATED RequiredAllowlistedNeverNative
M10_answer_any_terminal cfg_sha256=6fd7f0f57ee1ada3e5fd64bb1726735c7752efb610fcccc4ee281c0178aa5d3b out_sha256=973bb35dbe3a515876a3c41b236e644197049fa65a7e4dea83f6565d7ed4af70 result=VIOLATED AnswerOnlyOnAcceptedResult
