Skip to content

Commit

Permalink
PTG: Disable controller gen and add new strategy generation
Browse files Browse the repository at this point in the history
  • Loading branch information
@mikaelbdj
mikaelbdj committed May 23, 2024
1 parent 35722e0 commit fe0780c
Show file tree
Hide file tree
Showing 4 changed files with 188 additions and 64 deletions.
152 changes: 91 additions & 61 deletions src/lib/AlgoPTG.ml
View file
Original file line number Diff line number Diff line change
Expand Up @@ -45,6 +45,7 @@ let print_exp = print_message Verbose_experiments
type edge = {state: state_index; action: Automaton.action_index; transition: StateSpace.combined_transition; state': state_index}

type edge_status = BackpropLosing | BackpropWinning | Unexplored
type backtrack_type = Winning | Losing
module type Default = sig
type elem
type key
Expand All @@ -59,10 +60,10 @@ module DefaultHashtbl (D : Default) = struct
let model = D.model
(* let to_seq () = Hashtbl.to_seq D.tbl *)
let tbl = D.tbl
let replace = Hashtbl.replace tbl
let find key =
try Hashtbl.find tbl key with
Not_found -> D.default key
let replace = Hashtbl.replace tbl
Not_found -> let d = D.default key in replace key d; d
let to_str () = "[" ^
Seq.fold_left
(fun acc (key, elem) -> Printf.sprintf "%s, %s -> %s\n" acc (D.str_of_key key) (D.str_of_elem elem))
Expand Down Expand Up @@ -96,10 +97,10 @@ let edge_list_to_str seq model state_space = "[" ^

module WinningZone = DefaultHashtbl (struct
let model = ref None
type elem = LinearConstraint.px_nnconvex_constraint * AlgoPTGStrategyGenerator.winningMovesPerState
type elem = LinearConstraint.px_nnconvex_constraint * AlgoPTGStrategyGenerator.state_strategy ref
type key = state_index
let tbl = Hashtbl.create 100
let default = fun _ -> LinearConstraint.false_px_nnconvex_constraint(), new AlgoPTGStrategyGenerator.winningMovesPerState
let default = fun _ -> LinearConstraint.false_px_nnconvex_constraint(), ref []
let str_of_elem (zone, _) = match !model with
| Some model -> LinearConstraint.string_of_px_nnconvex_constraint model.variable_names zone
| None -> "No model provided"
Expand Down Expand Up @@ -133,14 +134,15 @@ module Depends = DefaultHashtbl (struct
type elem = edgeSet
type key = state_index
let tbl = Hashtbl.create 100
let default = fun idx -> let s = new edgeSet in Hashtbl.add tbl idx s; s
let default = fun _ -> new edgeSet
let str_of_elem _ = match !model with
| Some _ -> "TODO"
| None -> "No model provided"
let str_of_key = string_of_int
end)



class virtual stateSpacePTG = object(self)
val mutable state_space : StateSpace.stateSpace = new StateSpace.stateSpace 0
method state_space = state_space
Expand Down Expand Up @@ -430,7 +432,7 @@ class algoPTG (model : AbstractModel.abstract_model) (property : AbstractPropert
let coverage_pruning = ref false in
if self#matches_state_predicate state' then
begin
WinningZone.replace state' @@ ((self#constr_of_state_index >> nn) state', new AlgoPTGStrategyGenerator.winningMovesPerState);
WinningZone.replace state' @@ ((self#constr_of_state_index >> nn) state', ref []);
waiting #<- (e, BackpropWinning);
coverage_pruning := true
end;
Expand Down Expand Up @@ -459,63 +461,84 @@ class algoPTG (model : AbstractModel.abstract_model) (property : AbstractPropert
method private edge_set_to_queue_with_status edge_set status =
new normalQueue @@ List.map (fun e -> (e, status)) (edge_set#to_list)

(* Handle backtracking for a single edge, updating the winning zone and the associated strategy
return true if winning zone was changed otherwise false
*)
method private backtrack_single_controllable_edge edge bad_zone zone_map =
let {state; state'; action;_} = edge in
let winning_move = self#predecessor_nnconvex edge (zone_map state') in

let safe_timed_pred = self#safe_timed_pred winning_move bad_zone state in
let current_winning_zone = WinningZone.find state |> fst in


(* Intersect winning move with safe timed predecessors to remove unsafe parts *)
LinearConstraint.px_nnconvex_intersection_assign winning_move safe_timed_pred;

(* Make safe_timed_pred a partition *)
LinearConstraint.px_nnconvex_difference_assign safe_timed_pred current_winning_zone;

if not @@ LinearConstraint.px_nnconvex_constraint_is_false safe_timed_pred then
begin
(* Extend the winning zone with new partition *)
LinearConstraint.px_nnconvex_union_assign current_winning_zone safe_timed_pred;

(* Extend strategy with new partition *)
let new_strategy_entry : AlgoPTGStrategyGenerator.strategy_entry = {
action = action;
winning_move;
prioritized_winning_zone = safe_timed_pred
}
in
let strategy = WinningZone.find state |> snd in
strategy := new_strategy_entry :: !strategy;
true
end
else
false


(* General method for backpropagation of winning/losing zones *)
method private backtrack_gen e find replace to_str good_edge bad_edge precedence callback winning_moves_opt =
method private backtrack e waiting backtrack_type =
let {state; state';_} = e in
let get_pred_from_edges default edges zone save =
let get_pred_from_edges default edges zone =
List.fold_left (|||) default @@
List.map (fun edge ->
let pred = self#predecessor_nnconvex edge (zone edge.state') in
if save then
(match winning_moves_opt with
| Some winning_moves ->
(winning_moves#find edge.state')#replace (edge.action) pred
| None -> ());
pred
self#predecessor_nnconvex edge (zone edge.state')
)
edges
in
let g_init = LinearConstraint.px_nnconvex_copy @@ find state in
let g = get_pred_from_edges g_init (good_edge state) find true in
let b = get_pred_from_edges (bot ()) (bad_edge state) (fun x -> self#negate_zone (find x) x) false in

if precedence then LinearConstraint.px_nnconvex_difference_assign b g;
let new_zone = self#safe_timed_pred g b state in
print_PTG (Printf.sprintf "\tPred_t(G, B) = %s" @@ LinearConstraint.string_of_px_nnconvex_constraint model.variable_names new_zone);
if (find state) #!= new_zone then
begin
replace state new_zone;
print_PTG "Updating zones to:";
print_PTG (to_str ());
callback state
end;
(Depends.find state')#add e

let good_edges = if backtrack_type = Winning then self#get_controllable_edges state else self#get_uncontrollable_edges state in
let bad_edges = if backtrack_type = Losing then self#get_controllable_edges state else self#get_uncontrollable_edges state in

(* Backtracks in order to update losing zones in the simulation graph *)
method private backtrack_losing e waiting =
print_PTG "\tLOSING ZONE PROPAGATION:";
let callback state =
waiting #<-- (self#edge_set_to_queue_with_status (Depends.find state) BackpropLosing);
if state = state_space#get_initial_state_index then init_losing_zone_changed := true
in
self#backtrack_gen e LosingZone.find LosingZone.replace LosingZone.to_str
self#get_uncontrollable_edges self#get_controllable_edges true
callback None



(* Backtracks in order to update winning zones in the simulation graph *)
method private backtrack_winning e waiting =
print_PTG "\tWINNING ZONE PROPAGATION:";
let winning_moves = WinningZone.find e.state |> snd in
let replace state zone = (WinningZone.replace state (zone, winning_moves)) in
let callback state =
waiting #<-- (self#edge_set_to_queue_with_status (Depends.find state) BackpropWinning);
if state = state_space#get_initial_state_index then init_winning_zone_changed := true in
self#backtrack_gen e (WinningZone.find >> fst) replace WinningZone.to_str
self#get_controllable_edges self#get_uncontrollable_edges false
callback (Some winning_moves)
begin
match backtrack_type with
| Winning ->
print_PTG "\tWINNING ZONE PROPAGATION:";
let bad = get_pred_from_edges (bot ()) bad_edges (fun x -> self#negate_zone (fst @@ WinningZone.find x) x) in
let winning_zone_changed =
List.fold_left (||) false
(List.map(fun edge -> self#backtrack_single_controllable_edge edge bad (WinningZone.find >> fst)) good_edges) in
if winning_zone_changed then
begin
waiting #<-- (self#edge_set_to_queue_with_status (Depends.find state) BackpropWinning);
if state = state_space#get_initial_state_index then init_winning_zone_changed := true
end
| Losing ->
print_PTG "\tLOSING ZONE PROPAGATION:";
let good = get_pred_from_edges (LinearConstraint.px_nnconvex_copy @@ LosingZone.find state) good_edges LosingZone.find in
let bad = get_pred_from_edges (bot ()) bad_edges (fun x -> self#negate_zone (LosingZone.find x) x) in
LinearConstraint.px_nnconvex_difference_assign bad good;
let new_zone = self#safe_timed_pred good bad state in
if (LosingZone.find state) #!= new_zone then
begin
LosingZone.replace state new_zone;
waiting #<-- (self#edge_set_to_queue_with_status (Depends.find state) BackpropLosing);
if state = state_space#get_initial_state_index then init_losing_zone_changed := true
end;
end;
(Depends.find state')#add e

(* Initial state is lost if initial constraint is included in losing zone *)
method private init_is_lost init =
Expand Down Expand Up @@ -577,7 +600,7 @@ class algoPTG (model : AbstractModel.abstract_model) (property : AbstractPropert

(* If goal is init then initial winning zone is it's own constraint*)
if self#matches_state_predicate init then
WinningZone.replace init @@ ((self#constr_of_state_index >> nn) init, new AlgoPTGStrategyGenerator.winningMovesPerState);
WinningZone.replace init @@ ((self#constr_of_state_index >> nn) init, ref []);

(* If init is deadlock then initial losing zone is it's own constraint*)
if self#matches_state_predicate init && propagate_losing_states then
Expand All @@ -595,12 +618,12 @@ class algoPTG (model : AbstractModel.abstract_model) (property : AbstractPropert
else
match edge_status with
| Unexplored ->
self#backtrack_winning e waiting;
if propagate_losing_states then self#backtrack_losing e waiting
self#backtrack e waiting Winning;
if propagate_losing_states then self#backtrack e waiting Losing
| BackpropWinning ->
self#backtrack_winning e waiting
self#backtrack e waiting Winning
| BackpropLosing ->
self#backtrack_losing e waiting
self#backtrack e waiting Losing
done;
print_PTG "After running AlgoPTG I found these winning zones:";
print_PTG (WinningZone.to_str ());
Expand All @@ -620,10 +643,17 @@ class algoPTG (model : AbstractModel.abstract_model) (property : AbstractPropert

(* Compute the parametric timed game *)
self#compute_PTG;


AlgoPTGStrategyGenerator.print_strategy
model
~strategy:(fun state_index -> !(WinningZone.find state_index |> snd))
~state_indices:(List.of_seq @@ Hashtbl.to_seq_keys WinningZone.tbl)
~state_space:state_space;

(* Compute the strategy *)
if options#ptg_controller_mode != AbstractAlgorithm.No_Generation then
AlgoPTGStrategyGenerator.generate_controller model (fun x -> WinningZone.find x |> snd) state_space options;
(* if options#ptg_controller_mode != AbstractAlgorithm.No_Generation then
AlgoPTGStrategyGenerator.generate_controller model (fun x -> WinningZone.find x |> snd) state_space options; *)

(* Return the result *)
self#compute_result;
Expand Down
49 changes: 46 additions & 3 deletions src/lib/AlgoPTGStrategyGenerator.ml
View file
Original file line number Diff line number Diff line change
Expand Up @@ -23,6 +23,49 @@ class ['a] array (ls : 'a list) = object
method get = Array.get internal_array
end

type strategy_entry = {
action : action_index;
prioritized_winning_zone : LinearConstraint.px_nnconvex_constraint;
winning_move : LinearConstraint.px_nnconvex_constraint;
}


type state_strategy = strategy_entry list

type strategy = state_index -> state_strategy

let format_zone_string (string : string) =
let b = Buffer.create 10 in
String.iter (fun c -> if c == '\n' then Buffer.add_char b ' ' else Buffer.add_char b c) string;
Buffer.contents b

let string_of_strategy_entry (model : abstract_model) (strategy_entry : strategy_entry) =
let {action;prioritized_winning_zone;winning_move} = strategy_entry in
Printf.sprintf "\t(Action: %s, Winning Zone: %s, Winning Move: %s)"
(model.action_names action)
(format_zone_string (LinearConstraint.string_of_px_nnconvex_constraint model.variable_names prioritized_winning_zone))
(format_zone_string (LinearConstraint.string_of_px_nnconvex_constraint model.variable_names winning_move))


let string_of_state_strategy (model : abstract_model) (state_strategy : state_strategy) =
let strategy_entry_strings = List.rev @@ List.map (string_of_strategy_entry model) state_strategy in
let state_strategy_string = List.fold_left (fun acc str -> Printf.sprintf "%s%s,\n" acc str) ("") strategy_entry_strings in
String.sub state_strategy_string 0 (String.length state_strategy_string-2)



let print_strategy (model : abstract_model) ~strategy ~state_indices ~state_space =
let relevant_states = List.filter (fun state_index -> List.length @@ strategy state_index != 0) state_indices in
let state_strategy_strings = List.map (fun state_index -> state_index, string_of_state_strategy model (strategy state_index)) relevant_states in

let get_location_index state_index = Array.get (DiscreteState.get_locations ((state_space#get_state state_index).global_location)) 0 in
let get_location_name state_index = model.location_names 0 (get_location_index state_index) in

print_message Verbose_standard "Printing strategy that ensures controller win:";
List.iter (fun (state_index, str) ->
print_message Verbose_standard @@ Printf.sprintf "%s -> \n%s\n" (get_location_name state_index) str
) state_strategy_strings

class winningMovesPerAction = object
inherit([action_index, LinearConstraint.px_nnconvex_constraint] hashTable)
method bot = LinearConstraint.false_px_nnconvex_constraint ()
Expand Down Expand Up @@ -182,9 +225,9 @@ let generate_controller (system_model : AbstractModel.abstract_model) (get_winni
) relevant_uncontrollable_successors;


let winning_moves = get_winning_moves state_index in
let winning_moves = get_winning_moves state_index in ()(* in
winning_moves#iter (
fun state_index' winning_moves_per_action ->
fun state_index' winning_moves_per_action ->
let location_index' = location_manager#get_location state_index' in
winning_moves_per_action#iter (
fun action_index nnconv_constr ->
Expand All @@ -204,7 +247,7 @@ let generate_controller (system_model : AbstractModel.abstract_model) (get_winni
) constituent_constrs
end);
continue_exploring state_index' location_index'
)
) *)
in
explore initial_state_index (location_manager#get_location initial_state_index);

Expand Down
11 changes: 11 additions & 0 deletions src/lib/AlgoPTGStrategyGenerator.mli
View file
Original file line number Diff line number Diff line change
Expand Up @@ -4,6 +4,16 @@ open State
open StateSpace


type strategy_entry = {
action : action_index;
prioritized_winning_zone : LinearConstraint.px_nnconvex_constraint;
winning_move : LinearConstraint.px_nnconvex_constraint;
}

type state_strategy = strategy_entry list

type strategy = state_index -> state_strategy

class winningMovesPerAction : object
val mutable internal_tbl : (action_index, LinearConstraint.px_nnconvex_constraint) Hashtbl.t
method replace : action_index -> LinearConstraint.px_nnconvex_constraint -> unit
Expand All @@ -24,4 +34,5 @@ class winningMovesPerState : object
method bot : winningMovesPerAction
end

val print_strategy : abstract_model -> strategy:strategy -> state_indices:state_index list -> state_space:StateSpace.stateSpace -> unit
val generate_controller : abstract_model -> (state_index -> winningMovesPerState) -> stateSpace -> Options.imitator_options -> unit
40 changes: 40 additions & 0 deletions tests/testcases/parametric_timed_games/strategy_generation/strategy_generation_1.imi
View file
Original file line number Diff line number Diff line change
@@ -0,0 +1,40 @@
(* Mikael & Baptiste, Aarhus, May 14, 2024
Strategy generation example, non-trivial
Expected constraint:
*)

uncontrollable actions: u_1, u_2;

var
x : clock;

automaton ptg

actions: c_1, c_2, c_3, c_4, c_5, u_1, u_2;

loc l1: invariant True
when True sync u_1 goto l2;
when x > 10 sync c_5 goto goal;

loc l2: invariant True
when 2 <= x & x <= 4 do {x:=0} sync u_2 goto l2;
when 1 < x & x < 2 sync c_2 goto temp1;
when x > 9 sync c_1 goto goal;

loc temp1: invariant True
when True sync c_3 goto temp2;

loc temp2: invariant True
when True sync c_4 goto goal;

accepting loc goal: invariant True


end (* ptg *)

init :=
& loc[ptg] = l1
& x = 0
;

end

0 comments on commit fe0780c

Please sign in to comment.