Commit a3874283 authored by Maximilien Colange's avatar Maximilien Colange

Make more exploration strategies available in regular reachability.

Update documentation.
parent 934bb0d3
......@@ -96,7 +96,8 @@ struct
(Pwo : PARTIAL_WO)
= Pwo(TA.DS)(TA.MDbm)(COMP)(Best(TA)(COMP))
let bestcompare = ref (module BestCost : BEST)
let walk_order = ref (module Waiting.Walk_BFS : PARTIAL_WO)
let bestcompare = ref (module HighPrio : BEST)
type res_t = M.res_t
......@@ -142,6 +143,26 @@ struct
Arg.Unit (function () -> do_bound := true),
" Use the (global M)-bounded version of the input automaton.
\tThis induces a performance hit, but guarantees termination of algorithms when you are not sure whether the input automaton is bounded or not.");
( "-order",
Arg.String (function
| "BFS" -> walk_order := (module Waiting.Walk_BFS : PARTIAL_WO)
| "DFS" -> walk_order := (module Waiting.Walk_DFS : PARTIAL_WO)
| "BBFS" -> walk_order := (module Waiting.BBFS : PARTIAL_WO)
| "BDFS" -> walk_order := (module Waiting.BDFS : PARTIAL_WO)
| "BBFST" -> walk_order := (module Waiting.BBFST : PARTIAL_WO)
| "BDFST" -> walk_order := (module Waiting.BDFST : PARTIAL_WO)
| "SBFS" -> walk_order := (module Best_wait.WSTS_WO : PARTIAL_WO)
| _ -> raise (Arg.Bad "Invalid argument for option -order")),
" Sets the order in which the RG is explored:
\tBFS [default] Bread-First Search
\tDFS Depth-First Search
\tBBFS Best first (i.e. higher preference, see state variable \"preference\"), BFS on equivalent ones
\t With optimality analysis (tiamo optimal), also see -best option.
\tBDFS Best first (i.e. higher preference, see state variable \"preference\"), DFS on equivalent ones
\t With optimality analysis (tiamo optimal), also see -best option.
\tSBFS Smart BFS");
]
end
......@@ -151,7 +172,6 @@ struct
include Option_common(struct module Dbm = UDbm type res_t = bool end)
let walk_order = ref (module Waiting.Walk_BFS : PARTIAL_WO)
let abstraction = ref (module Extra_LU : ITA_ABSTRACTION)
let inclusion = ref (module Inclusion : ITA_INCLUSION)
let initial_value = ref false
......@@ -160,24 +180,13 @@ struct
let arguments = Arg.align (common_args @
[
( "-order",
Arg.String (function
| "DFS" -> walk_order := (module Waiting.Walk_DFS : PARTIAL_WO)
| "BFS" -> walk_order := (module Waiting.Walk_BFS : PARTIAL_WO)
| "SBFS" -> walk_order := (module Best_wait.WSTS_WO : PARTIAL_WO)
| _ -> raise (Arg.Bad "Invalid argument for option -order")),
" Sets the order in which the RG is explored
\tBFS [default] Bread-First Search
\tSBFS Smart BFS
\tDFS Depth-First Search");
( "-abstr",
Arg.String (function
| "LU" -> abstraction := (module Extra_LU : ITA_ABSTRACTION)
| "M" -> raise (Arg.Bad "M abstraction is currently not implemented")
| "ID" -> abstraction := (module ID_abstraction : ITA_ABSTRACTION)
| _ -> raise (Arg.Bad "Invalid argument for option -abstr")),
" Sets the abstraction to use.
" Sets the abstraction to use:
\tLU [default] LU (per discrete state) abstraction
\tM M abstraction (unimplemented)
\tID No abstraction (use with bounded automata, otherwise
......@@ -188,7 +197,7 @@ struct
| "simple" -> inclusion := (module Inclusion : ITA_INCLUSION)
| "sri" -> inclusion := (module Sri : ITA_INCLUSION)
| _ -> raise (Arg.Bad "Invalid argument for option -incl")),
" Sets the inclusion to use
" Sets the inclusion to use:
\tsimple [default] regular set inclusion
\tsri abstract inclusion (Z subset of abs_LU(Z'))");
......@@ -201,7 +210,6 @@ struct
include Option_common(struct module Dbm = PDbm type res_t = int end)
let walk_order = ref (module Waiting.Walk_BFS : PARTIAL_WO)
let abstraction = ref (module ID_abstraction : ITA_ABSTRACTION)
let inclusion = ref (module Inclusion : ITA_INCLUSION)
let initial_value = ref Dbm.PDbm.Dbm.infty
......@@ -210,31 +218,14 @@ struct
let arguments = Arg.align (common_args @
[
( "-order",
Arg.String (function
| "BFS" -> walk_order := (module Waiting.Walk_BFS : PARTIAL_WO)
| "DFS" -> walk_order := (module Waiting.Walk_DFS : PARTIAL_WO)
| "BBFS" -> walk_order := (module Waiting.BBFS : PARTIAL_WO)
| "BDFS" -> walk_order := (module Waiting.BDFS : PARTIAL_WO)
| "BBFST" -> walk_order := (module Waiting.BBFST : PARTIAL_WO)
| "BDFST" -> walk_order := (module Waiting.BDFST : PARTIAL_WO)
| "SBFS" -> walk_order := (module Best_wait.WSTS_WO : PARTIAL_WO)
| _ -> raise (Arg.Bad "Invalid argument for option -order")),
" Sets the order in which the RG is explored
\tBFS [default] Bread-First Search
\tDFS Depth-First Search
\tBBFS Best first (see option -best), BFS on equivalent ones
\tBDFS Best first (see option -best), DFS on equivalent ones
\tSBFS Smart BFS");
( "-best",
Arg.String (function
| "cost" -> bestcompare := (module BestCost : BEST)
| "pref" -> bestcompare := (module HighPrio : BEST)
| _ -> raise (Arg.Bad "Invalid argument for option -best")),
" Sets the way to chose the best candidate in waiting list (see 'BBSF' and 'BDFS' arguments of option -order)
\tcost [default] Choose the symbolic state with the smallest minimal cost (i.e. the most promising one cost-wise)
\tpref Choose the symbolic state with the highest priority, encoded in the variable \"preference\" of the model");
" Sets the way to chose the best candidate in waiting list (see 'BBSF' and 'BDFS' arguments of option -order):
\tpref [default] Choose the symbolic state with the highest preference, encoded in the variable \"preference\" of the model
\tcost Choose the symbolic state with the smallest minimal cost (i.e. the most promising one cost-wise)");
( "-incl",
Arg.String (function
......
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