diff --git a/coloring/dice5_oracle.lus b/coloring/dice5_oracle.lus index 356cc51b30fa41e37c641636e1eea959d42807ff..f19130874a2e9821829b21c5a25a12d607da0e2d 100644 --- a/coloring/dice5_oracle.lus +++ b/coloring/dice5_oracle.lus @@ -3,8 +3,8 @@ include "../../test/lustre/oracle_utils.lus" node oracle( p0_color:int;p1_color:int;p2_color:int;p3_color:int;p4_color:int; - Enab_p0_recolor,Enab_p1_recolor,Enab_p2_recolor,Enab_p3_recolor,Enab_p4_recolor:bool; - p0_recolor,p1_recolor,p2_recolor,p3_recolor,p4_recolor:bool) + Enab_p0_recolor,Enab_p0_noop,Enab_p1_recolor,Enab_p1_noop,Enab_p2_recolor,Enab_p2_noop,Enab_p3_recolor,Enab_p3_noop,Enab_p4_recolor,Enab_p4_noop:bool; + p0_recolor,p0_noop,p1_recolor,p1_noop,p2_recolor,p2_noop,p3_recolor,p3_noop,p4_recolor,p4_noop:bool) returns (ok:bool); var Acti:bool^actions_number^card; @@ -13,8 +13,8 @@ var nodes : state^card; enables : bool^actions_number^card; let - Acti = [[p0_recolor],[p1_recolor],[p2_recolor],[p3_recolor],[p4_recolor]]; - Enab = [[Enab_p0_recolor],[Enab_p1_recolor],[Enab_p2_recolor],[Enab_p3_recolor],[Enab_p4_recolor]]; + Acti = [[p0_recolor,p0_noop],[p1_recolor,p1_noop],[p2_recolor,p2_noop],[p3_recolor,p3_noop],[p4_recolor,p4_noop]]; + Enab = [[Enab_p0_recolor,Enab_p0_noop],[Enab_p1_recolor,Enab_p1_noop],[Enab_p2_recolor,Enab_p2_noop],[Enab_p3_recolor,Enab_p3_noop],[Enab_p4_recolor,Enab_p4_noop]]; Stat = [ p0_color, p1_color, p2_color, p3_color, p4_color ]; nodes, enables = dice5(pre(Acti), Stat); diff --git a/coloring/p.lus b/coloring/p.lus index 04c27553aa2921445aa4186ad6e0973749250be2..7b69e1d2b728e5e64730029c81dab31bd85e718c 100644 --- a/coloring/p.lus +++ b/coloring/p.lus @@ -2,13 +2,13 @@ include "bitset.lus" type state = int; -type action = enum { recolor }; -const actions_number = 1; +type action = enum { recolor, noop }; +const actions_number = 2; function action_of_int(i : int) returns (a : action); let assert(i >= 0); - a = recolor; + a = if i = 0 then recolor else noop; tel; const K = max_degree + 1; @@ -18,12 +18,13 @@ returns (enabled : bool^actions_number); var conflict : bool; let conflict = subset<<K>>(one_hot<<K>>(this), bitset_of_list<<K,degree>>(neighbors)); - enabled = [ conflict ]; + enabled = [ conflict, not conflict ]; tel; function p_step<<const degree:int>>(this : state; neighbors : state^degree; action : action) returns (new : state); let - new = first_set<<K>>(diff<<K>>(true^K, bitset_of_list<<K,degree>>(neighbors))); + new = if action = noop then this + else first_set<<K>>(diff<<K>>(true^K, bitset_of_list<<K,degree>>(neighbors))); assert(new >= 0); tel; diff --git a/coloring/p.ml b/coloring/p.ml index 899115bef6605589dd490a64ee441d8b31dac051..869d9bf302851b08242b9ce702a04c298eec13a9 100644 --- a/coloring/p.ml +++ b/coloring/p.ml @@ -15,9 +15,10 @@ let init_state : State.t Algo.state_init_fun = fun n _ -> Random.int n let enable_f : State.t Algo.enable_fun = fun state neighbors -> if conflict { color = state; neighbors = List.map Algo.state neighbors } then [ "recolor" ] - else [ ] + else [ "noop" ] let step_f : State.t Algo.step_fun = fun state neighbors action -> match action with | "recolor" -> color { color = state; neighbors = List.map Algo.state neighbors } + | "noop" -> state | _ -> failwith "Invalid action" diff --git a/coloring/state.ml b/coloring/state.ml index df321ce1563da4cb5510ce4cbb81d150acc950c9..42413aa1133a07b72e54a2ce59abfd2ff7fcb74a 100644 --- a/coloring/state.ml +++ b/coloring/state.ml @@ -2,4 +2,4 @@ type t = int let to_string = Printf.sprintf "color=%i" let of_string = None let copy x = x -let actions = [ "recolor" ] +let actions = [ "recolor"; "noop" ]