@@ -18,80 +18,50 @@ pub enum SolverOutput {
1818}
1919
2020pub fn solve ( nfa : & nfa:: Nfa , output : & SolverOutput ) -> Solution {
21- match output {
22- SolverOutput :: Strategy => compute_maximal_winning_strategy ( nfa) ,
23- SolverOutput :: YesNo => compute_control_problem_solution ( nfa) ,
24- }
25- }
26-
27- fn compute_control_problem_solution ( nfa : & nfa:: Nfa ) -> Solution {
2821 let dim = nfa. nb_states ( ) ;
2922 let source = get_omega_sheep (
3023 dim,
3124 & nfa. initial_states ( ) . iter ( ) . cloned ( ) . collect :: < Vec < _ > > ( ) ,
3225 ) ;
3326 let final_states = nfa. final_states ( ) ;
34-
3527 let edges = nfa. get_edges ( ) ;
36- let mut strategy = Strategy :: get_maximal_strategy ( dim, & nfa. get_alphabet ( ) ) ;
37-
38- for maximal_finite_value in 1 ..dim as coef {
39- let mut step = 1 ;
40- loop {
41- //convert strategy to flows
42- info ! (
43- "Looking for a winning strategy using maximal finite_value {} step {}" ,
44- maximal_finite_value, step
45- ) ;
46- step += 1 ;
47-
48- let changed = update_strategy (
49- dim,
50- & mut strategy,
51- & final_states,
52- & edges,
53- maximal_finite_value,
54- ) ;
55- let result = strategy. is_defined_on ( & source) ;
56-
57- if !changed || !result {
58- break ;
59- }
28+ let letters = nfa. get_alphabet ( ) ;
29+ let strategy = match output {
30+ SolverOutput :: Strategy => {
31+ compute_maximal_winning_strategy ( dim, & final_states, edges, & letters)
6032 }
61- if strategy . is_defined_on ( & source ) {
62- break ;
33+ SolverOutput :: YesNo => {
34+ compute_control_problem_solution ( dim , & source , & final_states , edges , & letters )
6335 }
64- }
36+ } ;
37+ let is_controllable = strategy. is_defined_on ( & source) ;
6538 Solution {
6639 nfa : nfa. clone ( ) ,
67- result : Some ( strategy . is_defined_on ( & source ) ) ,
40+ is_controllable ,
6841 winning_strategy : strategy,
6942 }
7043}
7144
72- fn compute_maximal_winning_strategy ( nfa : & nfa:: Nfa ) -> Solution {
73- let dim = nfa. nb_states ( ) ;
45+ fn compute_maximal_winning_strategy (
46+ dim : usize ,
47+ final_states : & [ usize ] ,
48+ edges : HashMap < String , Graph > ,
49+ letters : & [ & str ] ,
50+ ) -> Strategy {
7451 let maximal_finite_value = dim as coef ;
75- let final_states = nfa. final_states ( ) ;
7652
77- let edges = nfa. get_edges ( ) ;
78- let mut strategy = Strategy :: get_maximal_strategy ( dim, & nfa. get_alphabet ( ) ) ;
53+ let mut strategy = Strategy :: get_maximal_strategy ( dim, letters) ;
7954
8055 let mut step = 1 ;
8156 loop {
8257 //convert strategy to flows
83- info ! (
84- "Computing the maximal winning strategy step {} states\n {}\n current strategy\n {}" ,
85- step,
86- nfa. states_str( ) ,
87- strategy
88- ) ;
58+ info ! ( "Computing the maximal winning strategy step {}" , step) ;
8959 step += 1 ;
9060
9161 let changed = update_strategy (
9262 dim,
9363 & mut strategy,
94- & final_states,
64+ final_states,
9565 & edges,
9666 maximal_finite_value,
9767 ) ;
@@ -100,11 +70,46 @@ fn compute_maximal_winning_strategy(nfa: &nfa::Nfa) -> Solution {
10070 break ;
10171 }
10272 }
103- Solution {
104- nfa : nfa. clone ( ) ,
105- result : None ,
106- winning_strategy : strategy,
73+ strategy
74+ }
75+
76+ fn compute_control_problem_solution (
77+ dim : usize ,
78+ source : & Sheep ,
79+ final_states : & [ usize ] ,
80+ edges : HashMap < String , Graph > ,
81+ letters : & [ & str ] ,
82+ ) -> Strategy {
83+ let mut strategy = Strategy :: get_maximal_strategy ( dim, letters) ;
84+
85+ for maximal_finite_value in 1 ..dim as coef {
86+ let mut step = 1 ;
87+ loop {
88+ //convert strategy to flows
89+ info ! (
90+ "Looking for a winning strategy using maximal finite_value {} step {}" ,
91+ maximal_finite_value, step
92+ ) ;
93+ step += 1 ;
94+
95+ let changed = update_strategy (
96+ dim,
97+ & mut strategy,
98+ final_states,
99+ & edges,
100+ maximal_finite_value,
101+ ) ;
102+ let result = strategy. is_defined_on ( source) ;
103+
104+ if !changed || !result {
105+ break ;
106+ }
107+ }
108+ if strategy. is_defined_on ( source) {
109+ break ;
110+ }
107111 }
112+ strategy
108113}
109114
110115fn update_strategy (
@@ -126,18 +131,7 @@ fn update_strategy(
126131 debug ! ( "Computing winning ideal" ) ;
127132 let mut winning_ideal = semigroup. get_path_problem_solution ( final_states) ;
128133 winning_ideal. insert ( & final_ideal) ;
129- //non-omega stay below dim
130- /*
131- debug!(
132- "Winning ideal for the path problem before rounding down\n{}",
133- winning_ideal
134- );*/
135- winning_ideal. round_down ( maximal_finite_value, dim) ; //backed by the small constants theorem
136- /*
137- debug!(
138- "Winning ideal for the path problem before minimize\n{}",
139- winning_ideal
140- );*/
134+ winning_ideal. round_down ( maximal_finite_value, dim) ;
141135 winning_ideal. minimize ( ) ;
142136 debug ! ( "Winning ideal for the path problem:\n {}" , winning_ideal) ;
143137 debug ! ( "Restricting strategy" ) ;
@@ -279,7 +273,7 @@ mod tests {
279273 nfa. add_transition_by_index1 ( 0 , 2 , 'a' ) ;
280274 nfa. add_transition_by_index1 ( 1 , 2 , 'a' ) ;
281275 let solution = solve ( & nfa, & SolverOutput :: Strategy ) ;
282- assert ! ( !solution. result . unwrap_or ( false ) ) ;
276+ assert ! ( !solution. is_controllable ) ;
283277 }
284278
285279 #[ test]
@@ -293,7 +287,7 @@ mod tests {
293287 nfa. add_transition_by_index1 ( 2 , 2 , 'a' ) ;
294288 let solution = solve ( & nfa, & SolverOutput :: Strategy ) ;
295289 print ! ( "{}" , solution) ;
296- assert ! ( !solution. result . unwrap_or ( false ) ) ;
290+ assert ! ( !solution. is_controllable ) ;
297291 }
298292
299293 #[ test]
@@ -324,6 +318,6 @@ mod tests {
324318
325319 let solution = solve ( & nfa, & SolverOutput :: YesNo ) ;
326320 print ! ( "{}" , solution) ;
327- assert ! ( solution. result . unwrap_or ( false ) ) ;
321+ assert ! ( solution. is_controllable ) ;
328322 }
329323}
0 commit comments