fact: Example get_set_eg1 : forall tr (net : @network _ PB_multi_params) a b, step_async_star step_async_init net tr -> inputs_m tr = [Put "james" "awesome"; Get "james"] -> outputs_m tr = [a; b] -> outputs_m tr = [Response "james" (Some "awesome") None; Response "james" (Some "awesome") (Some "awesome")].
imports: Verdi(Verdi) Coq(String) Verdi(VarD PrimaryBackup)