fact: Fixpoint gen_by_exec (t : table) (fuel : nat) (st : State) := let '(St im m stk (Atm addr pcl)) := st in match fuel with | O => returnGen st | S fuel' => match nth im addr with | Some Nop => bindGen (ainstr st) (fun i => match upd im addr i with | Some im' => let st' := St im' m stk (Atm addr pcl) in gen_by_exec t fuel' st' | None => returnGen st end) | Some _ => match exec t st with | Some st' => gen_by_exec t fuel' st' | None => returnGen st end | None => returnGen st end end.
imports: QuickChick(QuickChick) ZArith List QuickChick.ifcbasic(Machine)