Require Export PBFTsim.


Definition PBFTsimul : MonoSimulationState :=
  let num_requests     := 2  in
  let starting_seq_num := 0  in
  let req_operation    := 17 in
  let rounds   := [MkRound 0(*pos*) 5(*num steps*), MkRound 3 25, MkRound 0 36] in
  let switches := [MkSwitch 1 0] in
  PBFTsimul_n
    (MkInitRequests num_requests starting_seq_num req_operation)
    rounds
    switches.

Definition PBFTsimul_pp : unit :=
  print_endline (MonoSimulationState2string PBFTsimul).

Extraction "pbft_simul.ml" PBFTsimul_pp.



(* =================================================*)



Goal False.

  assert (PBFTsimul_list [0,0] = (0,PBFTinit,[]));
    simpl; unfold PBFTsimul_list, PBFTsimul, PBFTinit, run_mono_simulator_at; simpl.

3
  (* Too slow!  Could we force the evaluation of expressions? *)


(*    let init := constr:(MkInitSimState PBFTsys [MkDMsg dst req]) in
    assert (run_n_steps init [0,0,0] = (0,init,[]));
      simpl; unfold run_simulator_at; simpl.*)

(*
    unfold lrun_sm; simpl.
    unfold sm_halted; simpl.
    unfold eq_rect; simpl.
    unfold eq_ind_r; simpl.
    unfold eq_ind; simpl.
    unfold eq_rect; simpl.
    unfold eq_sym; simpl.
    unfold eq_trans; simpl.
    unfold f_equal; simpl.
 *)

Qed.
