Commit 705d7b54 authored by Adrien KOUTSOS's avatar Adrien KOUTSOS

added pretty printing functions for guarded processes and for if_tree

parent 52de3095
let VoterA sksig v pk =
new r.
let ballot = enc(v,r,pk) in
out(ca, <ballot,sign(ballot, sksig)>);
let VoterB sksig v pk =
new r.
let ballot = enc(v,r,pk) in
out(cb, <ballot,sign(ballot, sksig)>);
let Outcome v1 v2 v3 sk =
if EQ(v1,v2) then
out(cres,replayedBallot())
else if EQ(v1,v3) then
out(cres,replayedBallot())
else if EQ(v2,v3) then
out(cres,replayedBallot())
else
let res1 = dec(v1,sk) in
let res2 = dec(v2,sk) in
let res3 = dec(v3,sk) in
let acount = count(A(),res1,res2,res3) in
let bcount = count(B(),res1,res2,res3) in
out(cres,<acount,bcount>);
let SubTally{i} v1 v2 v3 bv1 bv2 pksig1 pksig2 pksig3 sk =
in(c, x).
if EQ(checksig(pi1(x),pi2(x),pksig1),sigok()) then
(SubTally{i-1}
(pi1(x)) v2 v3
(A()) bv2
pksig1 pksig2 pksig3 sk)
else if EQ(checksig(pi1(x),pi2(x),pksig2),sigok()) then
(SubTally{i-1}
v1 (pi1(x)) v3
bv1 (B())
pksig1 pksig2 pksig3 sk)
else if EQ(checksig(pi1(x),pi2(x),pksig3),sigok()) then
(SubTally{i-1}
v1 v2 (pi1(x))
bv1 bv2
pksig1 pksig2 pksig3 sk)
else
(SubTally{i-1} v1 v2 v3 bv1 bv2 pksig1 pksig2 pksig3 sk);
let SubTally{0} v1 v2 v3 bv1 bv2 pksig1 pksig2 pksig3 sk =
if EQ(bv1,A()) then
(if EQ(bv2,B()) then
(Outcome v1 v2 v3 sk)
else
out(cres,badVotes()))
else
out(cres,badVotes());
let P vc1 vc2 =
new n.
let pk = pk(n) in
let sk = sk(n) in
out(cinit,pk).
new nksig1.
new nksig2.
new nksig3.
let sksig1 = sksig(nksig1) in
let pksig1 = pksig(nksig1) in
out(cinit,pksig1).
let sksig2 = sksig(nksig2) in
let pksig2 = pksig(nksig2) in
out(cinit,pksig2).
let sksig3 = sksig(nksig3) in
let pksig3 = pksig(nksig3) in
out(cinit,pksig3).
out(cinit,sksig3).
((VoterA sksig1 vc1 pk) | (VoterB sksig2 vc2 pk)
| (SubTally{1} (N()) (N()) (N()) (C()) (C()) pksig1 pksig2 pksig3 sk));
goal: P (A()) (B()) ~ P (B()) (A())
......@@ -364,6 +364,34 @@ type guard =
| Conj of boole term * guard
| NConj of boole term * guard
let rec print_guard ppf g =
let open Fmt in
let ident = fun ppf s -> pf ppf "%s" s in
match g with
| NilGuard -> print_term ppf True
| Guard b -> pf ppf "@[%a@]" print_term b
| NGuard b ->
pf ppf "@[%a %a@]"
(styled `Bold ident) "not"
print_term b
| Conj (b,g') ->
Fmt.pf ppf "@[%a(%a,@ %a)@]"
(styled `Bold ident) "and"
print_term b
print_guard g'
| NConj (b,g') ->
Fmt.pf ppf "@[%a(%a %a,@ %a)@]"
(styled `Bold ident) "and"
(styled `Bold ident) "not"
print_term b
print_guard g'
(* (g,p) is should be interpreted as IfThenElse(g,p,Nil) (generalizing the
IfThenElse constructor to guards). *)
type guarded_process = guard * concrete process
......@@ -694,7 +722,6 @@ type action = | AIn of channel
| AOut of channel
let available_actions gp_list =
let actions =
List.fold_left
(fun acc guarded_process -> match guarded_process with
......@@ -738,6 +765,23 @@ type if_tree =
| Node of guard * if_tree * if_tree
| Leave of msg term
let rec print_if_tree ppf tree =
let open Fmt in
let ident ppf s = pf ppf "%s" s in
let kw style = (styled style ident) in
match tree with
| Leave t -> print_term ppf t
| Node (g,t1,t2) ->
pf ppf "@[<hv>%a (@[%a@]) %a@;<1 2>@[%a@]@ %a@ @[%a@]@]"
(kw `Red) "if"
print_guard g
(kw `Red) "then"
print_if_tree t1
(kw `Red) "else"
print_if_tree t2
let rec i_tree_depth = function
| Leave _ -> 1
| Node (_,i,i') -> 1 + max (i_tree_depth i) (i_tree_depth i')
......@@ -836,16 +880,9 @@ let apply_action action configuration env map_fresh side =
let sorted_gp_list = sort_gp_list configuration.gp_list
and frame = configuration.frame in
Printf.eprintf "aa %d %d%!" (List.length frame) (List.length sorted_gp_list);
let cpt3 = ref 0 in
let (new_gp_list, itree, map_fresh') =
List.fold_left
(fun (acc_gp_list, partial_itree, map) g_process ->
Printf.eprintf "aa %d%!" !cpt3;
cpt3 := !cpt3 + 1;
match g_process,action with
| (g, In (Public c, s, p)), AIn cp when Public c = cp ->
let (adv_term,map_fresh') =
......@@ -880,24 +917,20 @@ let apply_action action configuration env map_fresh side =
(acc_gp_list', partial_itree', map_fresh')
| _ -> (g_process :: acc_gp_list, partial_itree, map_fresh))
| (_, In _), _ | (_, Out _), _ ->
(g_process :: acc_gp_list, partial_itree, map_fresh)
| _ -> assert false)
([], Leave (Fun ("silence",[])), map_fresh)
sorted_gp_list in
Printf.eprintf "before term itree %d %d\n %!" (i_tree_size itree)
(i_tree_depth itree);
let outputed_term = term_from_itree itree in
Printf.eprintf "bb\n %!";
(* We weakly normalize the outputed term. *)
let norm_outputed_term =
weak_normalize env outputed_term in
Printf.eprintf "aa wn %!";
(* We define the new frame variable phi', and bind it in the environement. *)
let i = List.length configuration.frame in
let (var_phi', map_fresh'') =
......@@ -908,8 +941,6 @@ let apply_action action configuration env map_fresh side =
Hashtbl.add env.t_bindings var_phi' term_phi';
Hashtbl.add env.hide_bindings var_phi' false;
Printf.eprintf "aa ne %!";
let phi' = Var (var_phi',Msg) in
( { gp_list = new_gp_list;
......@@ -945,32 +976,20 @@ let get_actions_por left_configuration right_configuration =
else
left_actions)
let cpt = ref 0;;
(* Apply one step of the folding algorithm *)
let fold left_configuration right_configuration env map_fresh =
let por_actions = get_actions_por left_configuration right_configuration in
Printf.eprintf "fold %d: %d\n\n%!" !cpt (List.length por_actions);
cpt := !cpt + 1;
let cpt2 = ref 0 in
List.fold_left
(fun acc action ->
(* Environement are updated in place, so we need to make a copy for
each action. *)
let env' = copy_env env in
Printf.eprintf "fold2 %d %!" !cpt2;
cpt2 := !cpt2 + 1;
let (new_left_configuration, map_fresh') =
apply_action action left_configuration env' map_fresh Left in
Printf.eprintf "l %!" ;
let (new_right_configuration, map_fresh'') =
apply_action action right_configuration env' map_fresh' Right in
Printf.eprintf "r %!" ;
( new_left_configuration, new_right_configuration, env', map_fresh'')
:: acc )
[]
......
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment