From d994ed2e0a72cb695f8b2c6375364e0c7e6e6adf Mon Sep 17 00:00:00 2001 From: Patrick Totzke Date: Tue, 13 May 2025 09:25:23 +0100 Subject: [PATCH 1/9] add new binary target and bare module --- Cargo.toml | 5 +++++ src/iterative.rs | 58 ++++++++++++++++++++++++++++++++++++++++++++++++ 2 files changed, 63 insertions(+) create mode 100644 src/iterative.rs diff --git a/Cargo.toml b/Cargo.toml index fd1b5c0..7e12c97 100644 --- a/Cargo.toml +++ b/Cargo.toml @@ -21,3 +21,8 @@ itertools = "0.14.0" #profile mode #debug = true + +[[bin]] +name = "schaeppert" +path = "src/iterative.rs" + diff --git a/src/iterative.rs b/src/iterative.rs new file mode 100644 index 0000000..6e1b659 --- /dev/null +++ b/src/iterative.rs @@ -0,0 +1,58 @@ +use clap::Parser; +use std::path::PathBuf; +use log::info; + +use shepherd::nfa; +mod logging; + + + +#[derive(Parser, Debug)] +#[command(version, about, long_about = None)] +pub struct Args { + #[arg(value_name = "AUTOMATON_FILE", help = "Path to the input")] + pub filename: String, + + #[arg( + short = 'f', + long = "from", + value_enum, + default_value = "tikz", + help = "The input format" + )] + pub input_format: nfa::InputFormat, + + #[arg( + short = 'v', + long = "verbose", + action = clap::ArgAction::Count, + help = "Increase verbosity level" + )] + pub verbosity: u8, + + #[arg( + long, + short = 'l', + value_name = "LOG_FILE", + help = "Optional path to the log file. Defaults to stdout if not specified." + )] + pub log_output: Option, + +} + +pub fn main() { + // parse CLI arguments + let args = Args::parse(); + + // set up logging + logging::setup_logger(args.verbosity, args.log_output); + + // parse the input file + let nfa = nfa::Nfa::load_from_file(&args.filename, &args.input_format, &nfa::StateOrdering::Input); + + // print the input automaton + info!("{}", nfa); + + // compute the solution + +} From 95f4b74f35c5b2ab257f1d3f762d83f49463b875 Mon Sep 17 00:00:00 2001 From: Patrick Totzke Date: Tue, 13 May 2025 09:38:22 +0100 Subject: [PATCH 2/9] add new method Nfa::add_state --- src/nfa.rs | 13 +++++++++++++ 1 file changed, 13 insertions(+) diff --git a/src/nfa.rs b/src/nfa.rs index 8df8bb4..b46ecb9 100644 --- a/src/nfa.rs +++ b/src/nfa.rs @@ -320,6 +320,19 @@ impl Nfa { }); } + /// add a new state with given label + /// returns the index of the new state or an Error if the state already exists + pub fn add_state(&mut self, label: &str) -> Result{ + let label = String::from(label); + match self.states.contains(&label) { + true => Err("state with label exists"), + false => { + self.states.push(label); + Ok(self.states.len() - 1) + } + } + } + fn check_state(&self, q: State) { assert!(q < self.nb_states(), "State {} is not in the NFA", q) } From 87255c268d4280dd9a84b36970826b5a5f22736f Mon Sep 17 00:00:00 2001 From: Patrick Totzke Date: Tue, 13 May 2025 10:23:15 +0100 Subject: [PATCH 3/9] iterative: complete given automaton if necessary --- src/iterative.rs | 20 +++++++++++++++++++- 1 file changed, 19 insertions(+), 1 deletion(-) diff --git a/src/iterative.rs b/src/iterative.rs index 6e1b659..500b122 100644 --- a/src/iterative.rs +++ b/src/iterative.rs @@ -48,11 +48,29 @@ pub fn main() { logging::setup_logger(args.verbosity, args.log_output); // parse the input file - let nfa = nfa::Nfa::load_from_file(&args.filename, &args.input_format, &nfa::StateOrdering::Input); + let mut nfa = nfa::Nfa::load_from_file(&args.filename, &args.input_format, &nfa::StateOrdering::Input); // print the input automaton info!("{}", nfa); // compute the solution + if !nfa.is_complete() { + info!("The automaton is not complete. Completing it..."); + match nfa.add_state("SINK") { + Ok(sink) => { + info!("Added sink state"); + nfa.complete(Some(sink)); + }, + Err(e) => { + info!("Error adding sink state: {}", e); + return; // TODO: handle this error properly + } + } + } + // print the complete automaton again + info!("{}", nfa); + + // TODO: create prism input file + // TODO: call prism } From e44b26ca0dc42e9eea994983c31f651e0b05d479 Mon Sep 17 00:00:00 2001 From: Patrick Totzke Date: Wed, 14 May 2025 15:09:54 +0100 Subject: [PATCH 4/9] define nfa_to_prism function this turns our Nfa and a number n into a String representation in PRISM lang of the n-fold product MDP. --- src/iterative.rs | 71 ++++++++++++++++++++++++++++++++++++++++++++++++ 1 file changed, 71 insertions(+) diff --git a/src/iterative.rs b/src/iterative.rs index 500b122..12f19c4 100644 --- a/src/iterative.rs +++ b/src/iterative.rs @@ -13,6 +13,11 @@ pub struct Args { #[arg(value_name = "AUTOMATON_FILE", help = "Path to the input")] pub filename: String, + #[arg(value_name = "N", + help = "dimension of the product" + )] + pub dim: usize, + #[arg( short = 'f', long = "from", @@ -72,5 +77,71 @@ pub fn main() { info!("{}", nfa); // TODO: create prism input file + let prism_model = nfa_to_prism(&nfa, args.dim); + print!("{}", prism_model); // TODO: call prism } + +fn nfa_to_prism(nfa: &nfa::Nfa, n: usize) -> String { + let mut prism_input = String::new(); + prism_input.push_str("mdp\n\n"); + + // module M1 will be our NFA. + prism_input.push_str("module M1\n"); + // define states, assume that state 0 is the initial state + prism_input.push_str(&format!("s1 : [0..{}] init 0;\n", nfa.nb_states()-1)); + + // define transitions + for (act,am) in nfa.get_edges().iter() { // for every alphabet letter + for src in 0..am.dim() { // for all states + let succs = am.get_successors(src); // get successors + // prism requires explicit floating point numbers to represent distributions. + // here we represent a uniform dist among successors. + let prob = 1.0/succs.len() as f64; + let update = succs.iter() + .map(|trg| format!("{}:(s1'={})", prob, trg)) + .collect::>() + .join(" + "); + prism_input.push_str(&format!("[{act}] s1={} -> {};\n", src, update)); + } + } + prism_input.push_str("endmodule\n\n"); + + + // Add a copy of the MDP for every power up to n + for i in 2..=n { + prism_input.push_str(&format!("module M{i} = M1 [s1=s{i}, s{i}=s1] endmodule\n")); + } + + + // define a label representing global reachability target: + // every component is in one of its final states. + let mut final_line = String::from("\nlabel \"final\" = "); + + let mut conj = Vec::new(); + for i in 1..=n { + conj.push(nfa.final_states().iter() + .map(|f| format!("s{i}={f}")) + .collect::>() + .join("| ")); + } + final_line.push_str(&conj.iter() + .map(|f| format!("( {f} )")) + .collect::>() + .join(" & ")); + final_line.push_str(";\n"); + prism_input.push_str(&final_line); + + + // define the global system as the product of all n many copies. + // This uses prisms syntax for parallel composition. + prism_input.push_str("\nsystem\n"); + let prod_string = (1..=n) + .map(|i| format!("M{i}")) + .collect::>() + .join(" || "); + prism_input.push_str(&prod_string); + prism_input.push_str("\nendsystem\n"); + + prism_input +} From ee355e241fae6be8aaeda70cdce8546a47c0818d Mon Sep 17 00:00:00 2001 From: Patrick Totzke Date: Thu, 15 May 2025 09:19:49 +0100 Subject: [PATCH 5/9] nfa_to_prism: reorder states alphabetically --- src/iterative.rs | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/iterative.rs b/src/iterative.rs index 12f19c4..71fce96 100644 --- a/src/iterative.rs +++ b/src/iterative.rs @@ -53,7 +53,7 @@ pub fn main() { logging::setup_logger(args.verbosity, args.log_output); // parse the input file - let mut nfa = nfa::Nfa::load_from_file(&args.filename, &args.input_format, &nfa::StateOrdering::Input); + let mut nfa = nfa::Nfa::load_from_file(&args.filename, &args.input_format, &nfa::StateOrdering::Alphabetical); // print the input automaton info!("{}", nfa); From 12cee7eb95cb7e0a321c7372861ff700da81b950 Mon Sep 17 00:00:00 2001 From: Patrick Totzke Date: Thu, 15 May 2025 09:21:45 +0100 Subject: [PATCH 6/9] nfa_to_prism: use right initial state index --- src/iterative.rs | 8 ++++++-- 1 file changed, 6 insertions(+), 2 deletions(-) diff --git a/src/iterative.rs b/src/iterative.rs index 71fce96..30488b4 100644 --- a/src/iterative.rs +++ b/src/iterative.rs @@ -88,8 +88,12 @@ fn nfa_to_prism(nfa: &nfa::Nfa, n: usize) -> String { // module M1 will be our NFA. prism_input.push_str("module M1\n"); - // define states, assume that state 0 is the initial state - prism_input.push_str(&format!("s1 : [0..{}] init 0;\n", nfa.nb_states()-1)); + + // we assume that there is only one initial state; get it. + let initial :nfa::State = nfa.initial_states().iter().cloned().next().unwrap(); + + // define states string for prism + prism_input.push_str(&format!("s1 : [0..{}] init {initial};\n", nfa.nb_states()-1)); // define transitions for (act,am) in nfa.get_edges().iter() { // for every alphabet letter From 5c2604e29923fcec103f672fb013c7f68e68b46d Mon Sep 17 00:00:00 2001 From: Patrick Totzke Date: Thu, 15 May 2025 11:03:25 +0100 Subject: [PATCH 7/9] iterative procedure --- src/iterative.rs | 204 ++++++++++++++++++++++++++++++++++++----------- 1 file changed, 159 insertions(+), 45 deletions(-) diff --git a/src/iterative.rs b/src/iterative.rs index 30488b4..3d4ac82 100644 --- a/src/iterative.rs +++ b/src/iterative.rs @@ -1,23 +1,26 @@ -use clap::Parser; -use std::path::PathBuf; -use log::info; +use clap::{Parser, Subcommand}; +use log::{debug, info}; +use std::path::{PathBuf,Path}; use shepherd::nfa; mod logging; +use regex::Regex; +use std::fs::File; +use std::io; +use std::io::{Read, Write}; +use std::process::{Command, Stdio}; +const PRISM_CMD: &str = "prism"; - -#[derive(Parser, Debug)] +#[derive(Parser)] #[command(version, about, long_about = None)] pub struct Args { + #[command(subcommand)] + command: Commands, + #[arg(value_name = "AUTOMATON_FILE", help = "Path to the input")] pub filename: String, - #[arg(value_name = "N", - help = "dimension of the product" - )] - pub dim: usize, - #[arg( short = 'f', long = "from", @@ -42,18 +45,34 @@ pub struct Args { help = "Optional path to the log file. Defaults to stdout if not specified." )] pub log_output: Option, +} +#[derive(Subcommand)] +enum Commands { + Convert { + /// generate the n-fold product + //#[arg(default_value_t = 2020)] + power : Option, + }, + Iterate { + /// where to write genrated files + tmp_dir: PathBuf, + }, } pub fn main() { // parse CLI arguments - let args = Args::parse(); + let cli = Args::parse(); // set up logging - logging::setup_logger(args.verbosity, args.log_output); + logging::setup_logger(cli.verbosity, cli.log_output); // parse the input file - let mut nfa = nfa::Nfa::load_from_file(&args.filename, &args.input_format, &nfa::StateOrdering::Alphabetical); + let mut nfa = nfa::Nfa::load_from_file( + &cli.filename, + &cli.input_format, + &nfa::StateOrdering::Alphabetical, + ); // print the input automaton info!("{}", nfa); @@ -66,23 +85,77 @@ pub fn main() { Ok(sink) => { info!("Added sink state"); nfa.complete(Some(sink)); - }, + } Err(e) => { info!("Error adding sink state: {}", e); - return; // TODO: handle this error properly + return; // TODO: handle this error properly } } } // print the complete automaton again info!("{}", nfa); - // TODO: create prism input file - let prism_model = nfa_to_prism(&nfa, args.dim); - print!("{}", prism_model); - // TODO: call prism + match &cli.command { + Commands::Iterate { tmp_dir } => { + info!("Iterating prism on the given NFA. Writing files to {tmp_dir:?}."); + let res = iter_prism(&nfa, tmp_dir); + match res { + Ok(stopped_at) =>{ + println!("The {stopped_at}-fold power of this NFA is not controllable."); + } + Err(msg) => { + eprintln!("Error when calling prism:\n {msg}"); + } + } + } + Commands::Convert { power } => { + info!("Converting given NFA to a prism model."); + println!("{}", nfa_to_prism(&nfa, power.unwrap_or(1))) + } + } +} + +fn write_string_to_file(content: &str, file_path: &PathBuf) -> io::Result<()> { + let mut file = File::create(file_path)?; + file.write_all(content.as_bytes())?; + Ok(()) } -fn nfa_to_prism(nfa: &nfa::Nfa, n: usize) -> String { +fn call_prism(args: &[&str]) -> Result { + let mut child = Command::new(PRISM_CMD) + .args(args) + .stdout(Stdio::piped()) + .spawn() + .expect("Failed to call prism"); + + child.wait().expect("failed to wait on child"); + + let stdout = child.stdout.expect("Failed to capture stdout"); + + // Using stdout to read the output from the child process + let mut output = String::new(); + io::BufReader::new(stdout) + .read_to_string(&mut output) + .expect("Failed to read from stdout"); + info!( + "PRISM OUTPUT\n---------------\n{}\n-----------------", + output + ); + + // Compile the regular expression once + let re = Regex::new(r"Value in the initial state: (\d+\.\d+)").unwrap(); + + for line in output.lines() { + if let Some(captures) = re.captures(line) { + if let Some(value) = captures.get(1) { + return value.as_str().parse::().map_err(|_| ()); + } + } + } + Err(()) +} + +fn nfa_to_prism(nfa: &nfa::Nfa, n: u16) -> String { let mut prism_input = String::new(); prism_input.push_str("mdp\n\n"); @@ -90,62 +163,103 @@ fn nfa_to_prism(nfa: &nfa::Nfa, n: usize) -> String { prism_input.push_str("module M1\n"); // we assume that there is only one initial state; get it. - let initial :nfa::State = nfa.initial_states().iter().cloned().next().unwrap(); + let initial: nfa::State = nfa.initial_states().iter().cloned().next().unwrap(); // define states string for prism - prism_input.push_str(&format!("s1 : [0..{}] init {initial};\n", nfa.nb_states()-1)); + prism_input.push_str(&format!( + "s1 : [0..{}] init {initial};\n", + nfa.nb_states() - 1 + )); // define transitions - for (act,am) in nfa.get_edges().iter() { // for every alphabet letter - for src in 0..am.dim() { // for all states + for (act, am) in nfa.get_edges().iter() { + // for every alphabet letter + for src in 0..am.dim() { + // for all states let succs = am.get_successors(src); // get successors - // prism requires explicit floating point numbers to represent distributions. - // here we represent a uniform dist among successors. - let prob = 1.0/succs.len() as f64; - let update = succs.iter() - .map(|trg| format!("{}:(s1'={})", prob, trg)) - .collect::>() - .join(" + "); + // prism requires explicit floating point numbers to represent distributions. + // here we represent a uniform dist among successors. + let prob = 1.0 / succs.len() as f64; + let update = succs + .iter() + .map(|trg| format!("{}:(s1'={})", prob, trg)) + .collect::>() + .join(" + "); prism_input.push_str(&format!("[{act}] s1={} -> {};\n", src, update)); } } prism_input.push_str("endmodule\n\n"); - // Add a copy of the MDP for every power up to n for i in 2..=n { prism_input.push_str(&format!("module M{i} = M1 [s1=s{i}, s{i}=s1] endmodule\n")); } - // define a label representing global reachability target: // every component is in one of its final states. let mut final_line = String::from("\nlabel \"final\" = "); let mut conj = Vec::new(); for i in 1..=n { - conj.push(nfa.final_states().iter() - .map(|f| format!("s{i}={f}")) - .collect::>() - .join("| ")); + conj.push( + nfa.final_states() + .iter() + .map(|f| format!("s{i}={f}")) + .collect::>() + .join("| "), + ); } - final_line.push_str(&conj.iter() - .map(|f| format!("( {f} )")) - .collect::>() - .join(" & ")); + final_line.push_str( + &conj + .iter() + .map(|f| format!("( {f} )")) + .collect::>() + .join(" & "), + ); final_line.push_str(";\n"); prism_input.push_str(&final_line); - // define the global system as the product of all n many copies. // This uses prisms syntax for parallel composition. prism_input.push_str("\nsystem\n"); let prod_string = (1..=n) - .map(|i| format!("M{i}")) - .collect::>() - .join(" || "); + .map(|i| format!("M{i}")) + .collect::>() + .join(" || "); prism_input.push_str(&prod_string); prism_input.push_str("\nendsystem\n"); prism_input } + +fn iter_prism(nfa: &nfa::Nfa, tmp_dir :&Path) -> Result { + let mut i: u16 = 1; + loop { + // create prism input string + let prism_model = nfa_to_prism(nfa, i); + debug!("{}", prism_model); + + // write prism input to file + let prism_input_path = tmp_dir.join(format!("model-{}.pm", i)); + if let Err(e) = write_string_to_file(&prism_model, &prism_input_path) { + return Err(format!("Error writing to file: {}", e)); + } + + info!("Wrote prism input to file: {}", prism_input_path.display()); + + let value = call_prism(&[ + "-pf", + "Pmax=? [ F \"final\" ]", + &prism_input_path.to_string_lossy(), + ]) + .unwrap(); + println!("n={} -> {:.3}", i, value); + + if value < 1.0 { + println!("The value is less than 1.0, stopping the search."); + break; + } + i += 1; + } + Ok(i) +} From 20906614f998b353e9846345a923bb75c15f6e66 Mon Sep 17 00:00:00 2001 From: Patrick Totzke Date: Mon, 26 May 2025 14:20:02 +0100 Subject: [PATCH 8/9] docs --- README.md | 26 +++++++++++ examples/guess-empty-n/README.md | 75 ++++++++++++++++++++++++++++++++ 2 files changed, 101 insertions(+) create mode 100644 examples/guess-empty-n/README.md diff --git a/README.md b/README.md index abe13b6..b47c809 100644 --- a/README.md +++ b/README.md @@ -134,4 +134,30 @@ shepherd -f examples/example1.tikz -o report.tex && pdflatex report.tex The states of the NFA can be automatically reordered in order to make the generated reports more readable. Either topologically (`-s topological`) or alphabetically (`-s alphabetical`). +## Comparison with iterating prism + +The binary `schaeppert` implements an alternative approach for the random population control problem by iteratively constructing an explicit n-fold product MDP, +and stopping once the combined target is not almost-surely reachable. +This is of course only a semi-decision procedure, as it may not terminate on controllable instances. + +MDP solving is done using [prism model checker](https://github.com/prismmodelchecker/prism) and we **assume that the `prism` binary is available in your PATH**. +The product MDPs are represented in the PRISM language using the [parallel composition](https://www.prismmodelchecker.org/manual/ThePRISMLanguage/ProcessAlgebraOperators). +Accordingly, the size of the representation is linear in the number of NFA transitions and $n$. + +The binary includes two subcommands: + +- `schaeppert convert [n]`: This will read an automaton from the given file and print the n-fold product MDP to standard out. The argument `n` is optional and defaults to 1. +- `schaeppert iterate `: This will read an automaton from the given file and iteratively creates prism-models and calls `prism` on them. + + +```console +./target/release/schaeppert -f dot examples/bottleneck-2-free.dot iterate tmp/ +n=1 -> 1.000 +n=2 -> 1.000 +n=3 -> 0.500 +The value is less than 1.0, stopping the search. +The 3-fold power of this NFA is not controllable. +``` + + diff --git a/examples/guess-empty-n/README.md b/examples/guess-empty-n/README.md new file mode 100644 index 0000000..1df9a2b --- /dev/null +++ b/examples/guess-empty-n/README.md @@ -0,0 +1,75 @@ + +# A family of uncontrollable NFAs + +Each automaton in this family is a bottleneck of capacity n, facilitated by n states and actions. +The idea is to let all processes go to one of $n$ distinct nodes; afterwards, one has to play an action $aj$ +identifying a node $j$ that is not occupied. This move wins, any other loses. + +From $n>1$ onwards, all of these models are **not** congrollable for arbitrary number of processes, but the $n$-fold product of the size-$m$ model is controllable. + +## Generate model files + +Starting in shepherd's main directory, run the python script to generate 10 models. + +```console +cd examples/guess-empty-n +./generate_models.py 10 + +ls +bottleneck-10.dot bottleneck-2.dot bottleneck-4.dot bottleneck-6.dot bottleneck-8.dot generate_models.py +bottleneck-1.dot bottleneck-3.dot bottleneck-5.dot bottleneck-7.dot bottleneck-9.dot +``` + +## Solve them using prism + +```console +time ./target/release/schaeppert -f dot examples/guess-empty-n/bottleneck-5.dot iterate tmp/ +n=1 -> 1.000 +n=2 -> 1.000 +n=3 -> 1.000 +n=4 -> 1.000 +n=5 -> 0.962 +The value is less than 1.0, stopping the search. +The 5-fold power of this NFA is not controllable. + +./target/release/schaeppert -f dot examples/guess-empty-n/bottleneck-5.dot 5.82s user 0.33s system 216% cpu 2.847 total +``` + + +## Solve them using shepherd + + +```console + time ./target/release/shepherd -f dot examples/guess-empty-n/bottleneck-5.dot + +Maximal winning strategy; +Answer: + NO (uncontrollable) + +States: ( 3 , 2 , 0 , T , 4 , 1 , 5 ) + Play action 'a' in the downward-closure of + ( _ , _ , 4 , _ , _ , _ , _ ) + + +Play action 'a1' in the downward-closure of + ( ω , ω , _ , _ , ω , _ , ω ) + + +Play action 'a2' in the downward-closure of + ( ω , _ , _ , _ , ω , ω , ω ) + + +Play action 'a3' in the downward-closure of + ( _ , ω , _ , _ , ω , ω , ω ) + + +Play action 'a4' in the downward-closure of + ( ω , ω , _ , _ , _ , ω , ω ) + + +Play action 'a5' in the downward-closure of + ( ω , ω , _ , _ , ω , ω , _ ) + + +./target/release/shepherd -f dot examples/guess-empty-n/bottleneck-5.dot 0.37s user 0.06s system 175% cpu 0.248 total +``` From 3a67c379b878cf1ea3db1318339177ee5aa2c4eb Mon Sep 17 00:00:00 2001 From: Patrick Totzke Date: Mon, 26 May 2025 13:50:54 +0100 Subject: [PATCH 9/9] parameterized example Each automaton in this family is a bottleneck of capacity n, facilitated by $O(n)$ states and actions. The idea is to let all processes go to one of $n+1$ distinct nodes; afterwards, one has to play an action $aj$ identifying a node $j$ that is not occupied. This move wins, any other loses. All of these models are **not** congrollable for arbitrary number of processes, but the $n$-fold product of the size-$m$ model is controllable iff $n\le m$. The two python scripts generate (dot) NFAs and run commands on them, respectively. See `examples/guess-empty-n/README.md` for details. --- examples/guess-empty-n/README.md | 20 +++-- examples/guess-empty-n/generate_models.py | 58 +++++++++++++ examples/guess-empty-n/nfa-2.png | Bin 0 -> 24611 bytes examples/guess-empty-n/run_benchmarks.py | 101 ++++++++++++++++++++++ 4 files changed, 170 insertions(+), 9 deletions(-) create mode 100755 examples/guess-empty-n/generate_models.py create mode 100644 examples/guess-empty-n/nfa-2.png create mode 100755 examples/guess-empty-n/run_benchmarks.py diff --git a/examples/guess-empty-n/README.md b/examples/guess-empty-n/README.md index 1df9a2b..3e4cf29 100644 --- a/examples/guess-empty-n/README.md +++ b/examples/guess-empty-n/README.md @@ -1,11 +1,13 @@ # A family of uncontrollable NFAs -Each automaton in this family is a bottleneck of capacity n, facilitated by n states and actions. -The idea is to let all processes go to one of $n$ distinct nodes; afterwards, one has to play an action $aj$ +Each automaton in this family is a bottleneck of capacity n, facilitated by $O(n)$ states and actions. +The idea is to let all processes go to one of $n+1$ distinct nodes; afterwards, one has to play an action $aj$ identifying a node $j$ that is not occupied. This move wins, any other loses. -From $n>1$ onwards, all of these models are **not** congrollable for arbitrary number of processes, but the $n$-fold product of the size-$m$ model is controllable. +![nfa for N=2](nfa-2.png) + +All of these models are **not** congrollable for arbitrary number of processes, but the $n$-fold product of the size-$m$ model is controllable iff $n\le m$. ## Generate model files @@ -16,14 +18,14 @@ cd examples/guess-empty-n ./generate_models.py 10 ls -bottleneck-10.dot bottleneck-2.dot bottleneck-4.dot bottleneck-6.dot bottleneck-8.dot generate_models.py -bottleneck-1.dot bottleneck-3.dot bottleneck-5.dot bottleneck-7.dot bottleneck-9.dot +nfa-10.dot nfa-2.dot nfa-4.dot nfa-6.dot nfa-8.dot generate_models.py +nfa-1.dot nfa-3.dot nfa-5.dot nfa-7.dot nfa-9.dot ``` ## Solve them using prism ```console -time ./target/release/schaeppert -f dot examples/guess-empty-n/bottleneck-5.dot iterate tmp/ +time ./target/release/schaeppert -f dot examples/guess-empty-n/nfa-5.dot iterate tmp/ n=1 -> 1.000 n=2 -> 1.000 n=3 -> 1.000 @@ -32,7 +34,7 @@ n=5 -> 0.962 The value is less than 1.0, stopping the search. The 5-fold power of this NFA is not controllable. -./target/release/schaeppert -f dot examples/guess-empty-n/bottleneck-5.dot 5.82s user 0.33s system 216% cpu 2.847 total +./target/release/schaeppert -f dot examples/guess-empty-n/nfa-5.dot 5.82s user 0.33s system 216% cpu 2.847 total ``` @@ -40,7 +42,7 @@ The 5-fold power of this NFA is not controllable. ```console - time ./target/release/shepherd -f dot examples/guess-empty-n/bottleneck-5.dot + time ./target/release/shepherd -f dot examples/guess-empty-n/nfa-5.dot Maximal winning strategy; Answer: @@ -71,5 +73,5 @@ Play action 'a5' in the downward-closure of ( ω , ω , _ , _ , ω , ω , _ ) -./target/release/shepherd -f dot examples/guess-empty-n/bottleneck-5.dot 0.37s user 0.06s system 175% cpu 0.248 total +./target/release/shepherd -f dot examples/guess-empty-n/nfa-5.dot 0.37s user 0.06s system 175% cpu 0.248 total ``` diff --git a/examples/guess-empty-n/generate_models.py b/examples/guess-empty-n/generate_models.py new file mode 100755 index 0000000..cc03e1c --- /dev/null +++ b/examples/guess-empty-n/generate_models.py @@ -0,0 +1,58 @@ +#!/usr/bin/env python3 +""" +generate_models.py + +This script generates DOT files representing a family of NFA (nondeterministic finite automaton) models. +For each integer i from 1 to n (inclusive), it creates a file named 'nfa-i.dot' describing an NFA +with a specific structure: +- States 0 through i, plus a target state T. +- Initial transitions from state 0 to each state 1..i+1 labeled 'a'. +- For each state j in 1..i+1, transitions from j to T labeled 'a{k}' for every k in 1..i+1 where k != j. + +Usage: + python generate_models.py +Where is a positive integer. + + +Note: All of these models are not congrollable for arbitrary number of processes, but the n-fold product of the size-m model is controllable by playing action "a", then "aj" if node "j" if none of the n processes reside in node j. +""" +import sys +def generate_model_file(n): + filename = f"nfa-{n}.dot" + with open(filename, "w") as f: + f.write('digraph NFA {\n') + f.write(' rankdir=TB;\n') + f.write(' init [label=" ",shape=none,height=0,width=0];\n') + # States 0..N + for i in range(n + 2): + f.write(f' {i} [label="{i}", shape=circle];\n') + # Target state T + f.write(' T [label="T", shape=doublecircle];\n\n') + # Initial arrow + f.write(' init -> 0;\n') + # Transitions from 0 to 1..N + for i in range(1, n + 2): + f.write(f' 0 -> {i} [label="a"];\n') + # For every two nodes 1 <= i, j <= N with i != j, add j -> T [label="i"] + for j in range(1, n + 2): + for i in range(1, n + 2): + if i != j: + f.write(f' {j} -> T [label="a{i}"];\n') + f.write('}\n') + +def main(): + if len(sys.argv) != 2: + print("Usage: python generate_models.py ") + sys.exit(1) + try: + n = int(sys.argv[1]) + if n < 1: + raise ValueError + except ValueError: + print("n must be a positive integer") + sys.exit(1) + for i in range(1, n + 1): + generate_model_file(i) + +if __name__ == "__main__": + main() diff --git a/examples/guess-empty-n/nfa-2.png b/examples/guess-empty-n/nfa-2.png new file mode 100644 index 0000000000000000000000000000000000000000..a7565901699712ef345a5c4cb64c47e49b743264 GIT binary patch literal 24611 zcmd4(c{rBu8a|4@L>WUN6d4L3B#J0=#>`_fr;H8AQ098elp(VeLZXn8Qkj#YkW@m3 zOeHg!W1r7wf4_Sl$KJo=xA*>Q@3q$FSZncm-sidR>%Ok@I?wZZA`J9280om^NF)-Y zmZq8!i9|t(e*$SX<0n({XVmatn;mpC)JPk|zq2ay6G$Xpl9rmXiC@O}5C2mizi(`r z{`TW!S;>=Yi7MB}ZyMM?aLu44$szU} zW;7hv?TP>KSfxgi!Gh0@WAh_sNrp|t&nZNy80tgVD6iYs(BTj4{$KjoK+WO4fUEU4 znC7^z7Eqbdq-wwNo#MH5>()|CtqCP@kN@5K|2J;-|Hne6dU8oSGgDD2hX%iY|33A| zCD-f;->KeVd2!?8SnFXa*Nz8Lm90HJyNaxyCwp;S7ya+27y6Yt3QZrrS=8LKEt>P- z@dKe8dU(*psPuHM%}hKD5o$)`S3JGE28M=mYfN;VO7XkyU!QW~Z{M~Wa-$3-;cCYd z1W&MLL>4e$)ja=ve=0OTKOY%zV$ZhPA3v;XBT}0j$RYa9N&U9jQagolQPSUUw-={`MkGw*n49-D8XtBx--(Hw2LWBB~s56W&TN{Um~ z*8bXWOg4*B>5^%vC||sI!TRDdFEfp#-?SZ%@d365ItpX^oZ~l}sxR}hM}5lI-~H>) zpE=wb4Q`F@X=!OFnM@thDnxtd&K-ZfHzusOP~MA*3W}wG9K((EfBt&)CW)z2B;7Cb zv%@-X8XB_g>#vhSwsIfopQ_%tURruUOiV26{{6RJD)$u-=m9tE5^w7Ys#;iZv}7vA zwzV0o&9y2nEzLNVPVJy0J9j?j8y_EUE3!H~|NHY6K|w(}-4BVM)p0Wp4ULVC&B^;| zXlRsFR48%T{$Ibs7bd#v+uOH|jEuCkwbf(>uSbM#+QKg+w57zh`nZV+E6=fjaGex! zJ_Utc6%`e~u+(p3cgNy0D#E8Vaqh%8ym5VjduAv_9ZtvTN(FIc4hHg zQ%lRpqkoODyAy8T-Wj3B|K$1e{2NTWJ-;3@-iN=)#A6s^hqSD%?*s${2p>FXd@k@u zh1U&t4-c&qCvJW%v6XlplqyB+>*J%e`pwN&&$ot zI&u4ub9*kW-kl@Vr51AMBpGRGm8W_uON0Jh*1dBiX-ZaxR$lr+grII}$oRNB6&026 z2^LZa&(X^@-@fhW?d^SmRML0Rm9<>Mpnh$6H1iiSD8B8+`KsmXQ?lfDr=`3ny4a-B z7_budzI-B^aW$kgypv^hacWdvuXKHRba$CYH@m#gc*u<#TX026A7_Jv z@$TnLB{r3H=`wChF-G^2_gguPca|>w&d-cXNon-W;0k36<5Ce!u>VqMdcn&}_20_h z%=&;>@6idv`gbd5I0# zL`1zYhI{6RZ{NiurfCTY+qZ4s&ce?A*7CM)e5YJkdfk^VY@a@Tdf_v1GOzpczZIF6 zJ`;2}^`R}7}qf5Y5u)? zsgGWsf8cG!wENhb0^@ungnml;v|qn}+t2^{w6r=^eQ|kqSbK3(z+KMoy}dly+1VLo zjjXX)nEtUZ4<)6fROUuLivIZe`*S`8$;ZcsZ1bn5;$TSYqR54Y+S<^kb#?#ihdz4%h*u|PXJyO8ZddaRcx z-b8FCvQ%5Ps@!k-r2v{+2?_PT2R0jXh*HUf6cp_H`SYi&i;k-5CbzGTYAdfSK1MEG zo1mbecyVEXG9WO}{`BcLTDBzS?b|nzoZGS}&U#3Z_qEPTNB3A*T3)>Ddlw;&GcYq4 ztLX6OYf+r$p75JD5k;c?6B8dT6>COyGEsj{q)QK!S>NY1qj3!(BLDOK6YoBJxc2hp z5g`w~bZJ^19v;8>Uo5AkIB`4#Q!L}o|9F{H{gz)qal9>S^Mwl+l+4W7h4gvWZxN&WPmU-G8JNBfTxG{%o+c|%U=jH; zGBO?qZv<)P8CB&Zey_c{CHvmJu%Le{Gu(Myj^wQC#F2Aw;9p<)BSC!N?$Ilfr{6LA zFojY+=8SZW!zTw2-x-;raW@X0ZOPKlJoe(^;O4I9=UaU<#$ryGnk8JjaihMaWovD1 zZHBH9zl0i${H zBarImxbp?={&00j?>ywLbn4WuWC`0A-$ee(pnqImBOhvq-X~bH81N!HZSv?Uqs3jQ zX=>8!+O=ybCP7~?A^U9W-SDWW`ibu6b3#Y#hhipJI@FBw^%}C2uS%kHD+I4+Ovx^f zd`P=0YF;EW;|iMjd{FDTqjZ9Y7(V@o) zec?GAsj}Mo;lmp&*W=Ugw-I^j;F%8w&Kn;#9;+DCe<`-!iF5AUS9Nq3H+N~kvM2eG z(%STZYG+s1Pe2%1pK%UkY~ICVX+KLJZe|E+o#QHZ{X%!(zyas3vVDg^zr4`f zit1PD{o815wpqf!+`RF9f{^|B^R51hx)qNfZvJqVo?VP6;d*x!B3@qlbINu@-4L3G8GuZgTYg8}3IrU#Ra5M`SSLBt&Nj?z~ zy3*28U?Kq{BcrUsLOKr*4-QVw+NLHtGc&WtPoJuOE4J3T6YBRSoP~yosS%k1Ii_Y< z<8;#qKk8sDo$d^`(6w4lxwmE(#lvIZl{x{+Ke9letfz1stvSo?uG zvPHQ&=P3QH#FV>tc@`#rM4_HJ;#*#yDJZ~+4Q>DYd0>2;0jH=Xe|L%Sl`B_1+&#Jz zVgDvUNPj8Dco5;U35kVv-@bh`3=G!{9w?~x=Vu0~M6vJhA0PklJF-dlcj8%ANxFg2 z(HmJ=yyLxoO49M$IY>S`@4gK#lvWr>Np!kxJwD%l2!iCTbdH(!x)xQO+szKKG z0OEhXl{B_0Zk!svZ(GttWD;b%0}gL!kY|44+kVRHMZAsSrWXVU7y>Eu= zO|~#sUBLu^dG41lUv|E@DA0FNdykJr;bZP7vdamf$v)N9Pqsxh zVC~cb0u)9*-UbT!?*n7FDT^nkY0ZjHSq=+rk~w&=9yn;`Pf7JpBq7{YGVba+0;PXw z=o;{o$!&jbCU(2yzFjPKj8V{VOK$*3P>VKK4Vs__G7$h|xR#Q# z19zF<@sQj6`0Bz$>4gE6wds1M@bK_{dA(<~_{R98B zow(z2_wSSk4<4)<6jlQ$D|Kw#N+dDl8=$?UMmlA-l(@JM+U8uNs^NF5ZMtC4Ts|*t*#_Lj+qWA|fWn(3~RCh|7H{G!@0?3O%~Zi9JI+hahB8 zOSB!xS#&GY14K&r1YoXvS0QamR(k+2O9RJj;OEb<*xibVx+Z&aRwN(4pP!!+0;sRA z`s5FlQ=C|k_4Rd4Ev?!|mQQiqhH=~)+);Rh^zXjut-SJm)^5YF#OCPI>Z)Vw-J|~j z)Qg3zW;BIyTbOw4CVMI@%A8q{)0bm%5?2-`q9V2nIm`~d$FdJ%O|V;R@$vDYECR=~ ztY7)Kw`}~Ex+P^~oKjeul|T5B?z`XD&y4w2VmpX)g6!7R7xd@r{#{4BY4CTv{AFlK z0CCh%ef-}SF!%#8F|)E>Lv!W`_>srna_t%w?rjiB4-cV??zewnz;IZ|dmj@@DD|#m z0USX=L7h*}GI1SpPpuBbAN^{}-ZVQqD|zv!8UyzcR_t)2xosdBd3&EizSOYGr+d_> z$uVf%2C?uBRa3LW&5{QXs`~lK0$xZ4t@-T{6uhT;V=E0Eospfx-I0-@h&Gx`95mY;7}F7N<%cgfBPW6VOx&$n2v!{>Ah3JTP# zMseCY&|EZq{J8(|k58ZC85kIZg@iO%442uP=t8$OfBcw-wMjo&=By0RCo+H8+gp0C zpdfqK`p3h4aRB1{{M$Zl(1ku3T7Hho6c-UeTk-NG`|=7--EUL^a=C<6c{Hi*j=b*> zw;|`XCtg(A?zLgmFRm<#pX+%+ap}@um6C4{&6%(S4LC_ND}UWipFT}m3b@3#e?Oy9 zL0Qc*mA`Sh0?7`Mtf;6sKheFT^77xXr%$~?zcDf}T$t)T>fZaBla`hin?S+B$HzxO znnqC|j|?;R<%RD%>Fg|whP4X`ExrUN*ZB4!50D(67W;zrh4eDA(5%xjGVVnYpfqsy zHMfb5j&=qqp`DN~{5fA==){Q=k&%%ij{}<$_fdshXW&%1v6cHCP@#ddv-A2wf4|+` zZKAC5(gw%1w6sj}^|-Ou7Nt|PxFkuvDnEE*olb&^fFtP&>hGJH?xBhqBD2iJuFlQQ z;yw^*hS`fH*00Ksvr+ndQF_nJf@8Y{{Ssi-j@2ssA5~#iAUaB1f4Lhi0t*jMargsj z4lXVc)4Ll+rl#r!2FyGPesR@YWvI|;X`IIbmJIss^UBJkcOAW)Sn^=4{}t;2>VM!Q z_OM6&1`^Aw`qtVS%fQG;^yUaOjYEeHbyQyQ9qTL=pvWq=e$@^LJ#=@u`MrwMd*fSZ zd*cm+bFotV{4f3I1ZCX5MuUa1w6ZeBVmxqaPL@WuO{uissyr82YC7GLLWNq*JKqzTJHAQ1s241A~KC z5zE5rciS1bq-ma??|Ta{kX2H`#IK^O%YZJ15q%$;gMs1Zl<=6C%_L_RmuzIG*JqNS zMm=H{j+meKE_3^~6-0|{@cQez)?)Lw)%41y(+d+;W$xd%q06ZQpRg2@!yrxseTb2O&Ojz;uXDs~t9E_;`t^d3&v8Ayt$i2$Ku*OHOd5~} zJw5#+i_$Rg1~F><%64|V_wL;*{5NKh2a;3+CAtC4BvKBQsi`SIvL-t_yTvP?{bnUL zH|IuMQOOQJVxA^YqeXSlQKE*3iXu^WIN!Z{m*ZG~Y|oD$Gm}5$k-Ed!D0yD{&k+UV zzhCt9EXCB5h{~hJ&jRYG)tA-gu}YR5n1|xxVxpTvHO3>YDOy`wgU0Abn&>Qb1k=D8 z!$wJM^~{w`+~#$7O^uSX8&Of0Q-F|(gq(W7ar0zfb*t|#vIAKu6m19X?%libjFjB+ zK11?bjjtiKF+n&nP!RV{*D4;>=Xz-Ry))lqF7K; zQrbB<)cNkZ&w!;kfDQ%ti5(Q$h>X+G2NIJ$i2&-WSc>!yVziJGHOwI9F9MMg0n z=&Kh*usW2!sHr#NkEhuoVRP-~O~%~^)JB1MNN&22-VVRQnb8NiZcJQV*C`(U3y!+~FQ+&15=%{(R3X-`FYH+4^rinqSma zR8-=-_3s=}2lBzAvSw(mUuWETd|Sjd66@*|`p#%g*Mz$t|DUczV`ryz{^|8mb2NP(YzM?szW=o7Z3) zj;4c44xI>IUl!uz;%W!E;-~$V){I6(;J|@+WCL0%O7trE;o&s5wDUT!ldfRO^78U# zxDCYtXti{79=_uT6mkap6rhn9h1MWJi8l+7-1y8HL8O@d8>6-zx4cbhM5&TW(LijA zP@@V#d}{64Hak7di!<;NMWb(Ks0sINVq!waMj5K4gf1gBR4ssj;R9)FH+hb}YaNw{upwGxa;k}0s z??89)>vKL6`~H(A&TS@Ja5p&`vEmmj6T>9|^mvTlH{$Yk9v(Nrfl(ed`e%i-6MFPb z;dQn!x+DIxd-iP8DlG~AZroYnC4@SV^}vEo1}y(t{ib+L0zB7rcBYP+^zie8Tipz@ zX@6?2U=Tj1Ygu(JN-5zh3~9Q}nU$SQ5gZ)6OU{#O z^XAQTdifSeFr;IORq{|A?tXr!zc~4Wg_AQa_?K~qbpjq8@s)os=b{SWnYy-)PCXLc z4AM3*fs#m)ij~z)bf?Z}0n&n9z-H63u_f`hru+VGrv{XKU|U_Ka4f9dZ+UhvSf|+% z=CbpBJb)$F{&&Xyypmkor%$!OYzM%;MDIMj73>-H0v)RHh1nr3&AfK0BD01senV8T z-^7O}ks->^BM_R(7xX!AtQ;ufLPIG)jz^()(ej<_*;j7u=JtouR){@HOI@7|rdwYs zO*b^t;6Sd?KJxYJ?P1jP?^;@lJ8wr+t!<|xqg^>JE-qenwv|U)S9fSt;DY#}L&=Z_ zG=*8&SJoPePVX<7c^5kNoXZo86u{;dpq^8&d>GMmJ%0XN1N8K#*Zy9pmi3*T00CUg zbY!BdM$r!eLBl5{wGBZ@!^qeGkZ$kc!HA>bclol4x%rNo(dujW@84fO8>`OG;_mKF zloqu8#}to@{u~@Eb!uiuuIB}SLZKlTaO4Pk7Z+MDFE3!7eh_>YJUvxF&7uO|eDFY6 zAz+CaiC+ca6!q-W)3f@~yA^phZP|Lwz~X3(W&}<3`iki5%1VlWUI7C`!%%d+fEAmS z)(7JSc0ByZqwM2zsL1+N@>oZKs;jH((D=A69w6`a>(_M8d?&hORwiFfX_}j-fFyN6 z0!zGgOU0_({e5+Uff)PeCr-^GJvW|Qp7}|AbLZh0X^JN?w^AcG%c^R1` zvqu)n*RNkEz}?E&!x9>TZ+(Bo_r$>e6PctBy&*xCeGKMkuB%hw8$2K^93FM%p%34? zk01A^D92AX=<8;vP6hGi1BTtBfgWn`V1rYBx%2IX^9~idz9XQ#(hRIyJAgqn1LUz zqMP~k$=#X~-un_FRYZdW z**Z+L#8s9jshSzM;TCjYkKWg5Q^I+4Tek|5=FvXQap!5u`%dmbWwvQOm-6Kr?e+&i zWZIXuUVYFNqcJQ&1qhpmRe$$a@38pyuCDeFicL!~hT#AuK)!jscm6#eZOu$jwoU;(CN9=@m01;5a1gQK12Bpc?KzAJE&gOZ?Ml#S{`(Wx(>SxpL9LX4@^|lm32d zO9%GbyiSEkt&6_!9(vBtG2HUPqM}h(b2koxMjLC-qtEv++x%^C2EQx=gUhAhC;4~s z$88{AeZc1G&PULprz{(gLva0 zBw$*SoV@&Jv>?AAo=7{sWdPRcD7KbwnVc0H^fQ@Mk@Ok20B9P_Edu>YL_TUyJ05Gu zj3)fW$B$$j$@VW_hKDFJvEXd}lw(kLc}W@T)U8M+XpZvyB_o#4|Nh+F_oRl+CaLwrPrV?7$qVhtcql;jSgi!X_kl^hlRsV|h<9r0>!-LWI$c_v zw9d`Vy)aw3w!S)5iXKa)d-d<1EkL*sBX-CS`}!kPI=j0Cq@@!R7DS?&XI?me;s?E5 z+_r!|l9F`ySYVTuqSE)bIqmFWDH68)hYqnXEG%S{owc(gZQs6KuS?`+PL2Rl>BWC5 zm&o(x>Bzfv@7~cMGnaTq>R#H;3=09GSl0+y$kBW+hUkb5; zo-Z(o1efpCbq=&H!5r+_yZ2((IsbhQ3cVFxTR?(oU|WeDY3bVE>}S%Y!pz1-jYUTB zo#oC`dGzQJGbiVJUj|ZUbqem+(@hbe4!A{wkV*e7_IY(Jr1S&?OAO2L;O6blo!bgX zPB6_Vo+6LKSa)dejMbLE<8NeitIlV5INN8UtD!hB%NZCdW1@XMMOUzXX=ae1ve1FI zY?)3uP_wvbba(LL%+CfwN-egjj8uKDOT^Eh8iMC#P)YK^d7BS?}}tYxj^s z2Z$`tNFwFt=d0ph;vQEnU;c^B22e<9_B@Lo2f3NR5u+X{HxwENQ}~bK?05rMAyeJZ z6}$=!=WJl&A)cg#HePx8+jG_8k-7Kpn~n1qL?++4!-yo%(rx|X0w2`V*dvW zeLCtl8zJ}AVn4xs4$mJF%JG159Y8`KD!z>V6QwU3&oeaK5GmrJ zATl9G2~Gm^c8Wi@oYVH5J0D6%g@HKc7Z;C7C?^_Q@bMfwcRK!j6G65K2I3U@7r;Vj zm<_$JvV>2?XdtYjc1YAUH`9Z0YTBUw2ci@_e$=B!Vju3v@4#}OQrlv%LOg?=lM@++ zf!BUBlxNPI$taTpKd5&6I6qns(qp(UpvTu>31PSx$z|%FOPl}o%elhli6|2q{+7uW zD^w3DDJdwZ2^%^h`p}t~X{caSi0D}rp-mYyw6^9Zv{&?_=!YqR_-M!~3jVWHU0q!k zXyx-$?3<-{lFFH-&-dE19vmh|6 z*-FU=U@&+!On+W^@#5-C6zcGBN$EQw@x~m`Pyl;?e(07X!A>IR2(SvpE2D48G?@rZ zC1d05NGA>80|>1{uM3R#exZrPk+tQywr}4w@J(#(wk{AK~sQsfg`sa-P%<>31amH$2dBRM(JpU^cm^13>4GY#`&?3LS7Ts=twBqLKN{5He zI2M>bB|JQfZldS4zwtgg3WG{y{pb#dXf7E-o6??X)3OA)`4hJQr2A7|n?g@dud_N> z5lFtzuxT8MCUC4WED1|7lv$T!HS)x%Ka_YZp4g0!LA*lXm-fVK3Znx+Wo`QKAs6McjY)B>2D0qm ziSCpH%ShG%FtGe2@4>f>RXMB%CveZL25R&EcVD30Z%5Gu9w>xID9!atq5ApW*8}p} z@kj~UBw<;(u9ZOj!&p$$03s60}h~cMiMw1)GTiG z6AJYM%cp0wD?1H8awGLQ)c&jC*Gs)bfwZx)rB5k9Z3M za>H(wNkEj;R1N}4FE1@k11Lm9M4*Qw5b&_Pb}4vhsGBDFGY?*qc@G{;7-_kq!yg}h zd0|`&Ns%9@F#TBIk-krK-(UM5B)%S20qnqOlqSF|VHBGwVQPpPW4)E~mKGKUIKO=t zwOQHNOz*tS@njDJ3-P41ln)XkSePs8Pkx}x3xO@D{@6CT1(+?qjE1c8rVZArU?E=uU>4OBm$Hlx*4MzplXdtgNhWd=otj z1P2ZM>1rXXsiLe4Ub=MYWQC_w>25W_g!ue?p@Ihw+MpV-X3PeIOdZRQN(LCe~E}mf3;9EAxclNNh;?`M%<| zstOavw*u8<-hKNbfF4!1MdZGz4Eg!Uw)!pzufM-P6T<%9{KSofA%8r>U6n22J-<5HJ)XU6RA|bb3=ig;{eNpb;gof_b3dVEp?g z($fM{*9qjp+?*U$;Fc_O9b1iqAaVVw3EgA@QAkQsGRv_s=3?)bzN$ybV(d``prKjW z*#%RA+S}WIL4p#(Zh`7y-M(EQC1}YLm;pfQk?Wx047tBKJH$flJ~*<^2n^95XO17= z{4rB8)5O%Yz%b`{89HG-pYP~^9$*d23Z;42tZ0q}t!bjL z3YA*uBCv*D|Lg3u_^;muA&+xNP;&%w1Op=KwUg*$artzRt1vU%##aN?g`s#i`rA0g zW6_DFgZMRao}QML58#4Q38{AI&mWz`=X!*{O^zaNoIyuRJGb#7H26T~&CbkZ!xs8} z&~aK^Oe`8S+r;;$H^K`${217n_l*pUp~5imC~$x+eT!ghLj+d*O#+_A(@cfB!}gcN|RpT?PLzGzd80+rjTOK=cplp=E5@JbbMn3LD zY5WPgia>F=ag>Puv9UrE{cWE6Wn|dke+UCryS_9SOIczXI^$=^NA7P*66FBshw5-~ z{+A(n-C^(Ey?oNrtXQ8K;KZ4=WiP_bgImW5YU}8@22ji;<4Uk28H&L?gqaIyoi#aL zAFZ?+g!5AWxijbxlUI6y$w138q3FVvq>htsWNZu|u^Bn+|736Q&kVI-fmnKRVcfE( zI=H%KesY5-hebt7B*fbVFP(!^KI%n^-yk?WwM4&@#N`?CTQketiIXqDkZ2WVLc zM1+IW0D^&qgM&s!M#leAW7p0kmu}!N z-aBeYgeeN0VE;_lq}XnDn{c3EFS zRFocSX9I%!!pgi0MDOc=#D~s7MkQQ3P*Rs-_zz!M7_Ws-p?`4DxWEUMB_zE<<1tVQ z)s`&+l9F+s=XgznVgZFWZQ9IG1IdV3{R$h-xO^zX{aCga-oMd<5Aox>;E`zn*0w)) z&ZeN;bu7CU4FmLlMLRfZ9zT0FTs9$6sSyWIgVw1ZHMcfTC#9{xSg1JNOcrRev$NBr zyZ$P&I=`G8r{emOV_tV*1esStf@yMcl5i7&$Zz#uJtc9$h&_WfEIOKD{?9iixG!nw z>5bFLM@1ZoN4q@loRq%)N(|v%>iR{55R{OlOT4ehlroFiyyjryQBZ>BhvYjtF*-b~ zEM_*|rJ5v8B_}6G$U8Vv7bknVjLxo&fs?sd+CXD)m_bK+%ytlL*H!Ve4**YjvhiP04*B>fs#1 z6X93Let5_5$Oz%?OO4m)QW`}TQ(6Y zbO5kgy@i;5z^;Z=d~n}Q+*cL?3wC0OK0}fH(Dfj%rUG;1Pkg<$N_ZIY^c0|n^vqSn zTL8SX5crEh>qR}}esIEohjs7b1rGR5p7K9!By#TDIc%CRlKMN}MD1mutphl(dc~}3 zRwp_IuqaZ%3PH=mJIM2kXfTJxsbJfNB6z)`Le2*ia*3|C)6l#4IPE;sm0Wx9snB~R zFO8YBbQe#K(x4wC>VAA3(nF-3M6UsvC{ch&>rt~aBv{})ew_pWo3mQ+2$RSCfrs?kfq2g z71oNTW(ZZ{NMQBf09S;mWU8-NQhp~y8_2busli^qI zc_dD$g9qhawdOo(GNB3j_tzY(lLHv&FP=LdOQWnnyX<`CmQuHSbHSsK5E4_(d-EnWiL4)M?n;n}#I6%vcn&~HgJ0iDGEc1*h?99?iY5|1YU}W2 zVbgRV4Vy@V(*Lp&7VbI%8@PupP0IxguWsfsZuBI6*mMADZ{*zY28W8)ZKl?Aggulm zNtO)8@be8V(WF8XV%&L1 z4SeoU)hiKw>^aBbbGz`YG$6Gqj_zF;dcPg=(w^YF+r*|IT#*C)(t>7+ZL4EY*34gQ zz~STg>7F{&c}|RH*p9D?oTL$1U4Ai(;SS<~kxf)_{ic6^anRpl(*`Cdx0;)O({=(K zu{Hcb51ALW0cH^;YzTy<#({6`z&_>h?)b;H#G}jgZTK;YUF7l}7ZnAQIly)!jQ4XtFSOadCq0(yLi3CXADAMie`!46@pm|d@ zH-Bz4#{|*Q0rD%koQYG4id49EDg;>MDAFqdCtA8~plcvcnmb=XlA;I*Vtu^_c9Y}K zafw+Y&&8u>TXqq(1)Ye~|N0~#cIpK)x<^!N)rzXGH8rHgslLWstpwT1 z&kLYWhwuJw24O=GeDj>xqV-dJPRrJ!v%3gD0V&tIfayC9694mHOX*zxt0rlL*Q_sS zbw7q@+Mb`c)!U+W(Mz!kd=QEF^v`dNZ{C=^2v1pzzNAj4?4)SxY0Lc4!zDi)2E05T8kv!O8X3!TlcW~EdQs%j#nByepPA^fiK zn|)tPx`gi|^hKCIN5u4T!cg6s4?Q$8+`?e}(mNXmimj^(u5F?R155xx!b;fMiMFi$ z+qZli+2qR#fX~G7!v`K2^;wz1C6)quUMJ8Nej_bth(YViXOF;Kju?%BCh`EFdGFm_ zPcg-W-9q2W4o~`ZkkC3450NW}5V&e;K)~=z6#%MwqiHx2uq4UIeIyYb2gaq6JM}DE zSm2P2g^tR)vMe%)3Q8zISS;#tbLkBjXyoKHh=H`RzUtt-xqulb@(2=Tj@XYKflsFU zHvR59(|Y#=+GXnU%HWN=cxd{7@O$V&l5xD$K|Cd>uYrl9>8<2I>znADX+tJ9npfk@cF4n`{@BbUAgG1-?FEPlMjMCjeL8%p2hVN=OJSCsS#pnPMrzxoL4b2sR}Z&VF5CcHoRnza!(aS*6ct_Cun8W zy{&||=jEj+)OULK1noR9FDHj;#F~(tX-PLZ58i*X=;G?y4!jZm%ZnmtZRuk6qS*g* z4Muw8i;-)(yKf)y{*~3%YHkR00wT#|h@;p!NSv+~c%GJoBw==>72gKgA{Is{qq{WO z>URPDC530%yDzmEyG~AR# z*n+l#&KaMv0L*y||1{xhAS`$fe~b(d6O$TFV`o9PV`Qif=?D(%uMR>V&^<2qo!zu) z6Hy<5x{t$10*Oxva}=7S5UEA$3<=|;eY10>Z$KdZPh$jZYGj*H{$O=#YU*tNxe;o; zX|p~0fDZ(KqNZn0yh4%8Pp^!fnA0B%j0duXS&{ex_&_+MoekC}9%A;O1~RI$8g}2wR$35mZ(>$y&z?Os$j%*$FdMPqq26LzP7*x|@RtfNb3br!CkzP{E8>wD z4MTN;AmX{!v8S7-~?`wkSJN3 z08FRZy7estVV$i;9YF*=0L9eM$7f+{7P|WTSSQ+G(ea>BL}LFX18JSoVCYUdrb|wrJ)5$zflAMh5WWo2H+%7ZZZ6t6 zE__XrpU^23!FPRqndmG3H)rM}lv@&^5`;>5%HkQ=^tcYj9XN>>>S0FRN@l6D8yKvhE&9C*pe z)6>&y9&j*RHxO2X`inv1+2#7EB!^>p)|jo`=GS+Vz#KbR9f_z52?z9g@w5#CHmm-2wMgLl#wQG zm6spFiW;Ly!aU3;4093wQxjO(LHK3^EgKM<_~s2U@?tvX@e#1R3|!6sE#vA?um>)S zt0z=e9t91{9J02tfk9sSzr(+OYhkd^;Mb_=Loj2o4&)LCbEyh@UX?0oPf7eyUfy1c zEC8YS%F4j_D<2vnVq*yd23m=S7w%%+QkJf4&eFX?1#1~o2nOFEryhd9w8J7z=KsnV zODyzWaUKy?x~NKlLXmE?9q>q8#~!hzFG;~DjWXA)c>n8{FAao|af-AGqY7Qmv*iDy z{^IoVYALirVssXFK!JdTW_1-%OVzfJ*Os0{+FhfC_X61NhLA~gDyY;HBpjXP=jBxx zVFJpLcw#Lo`cUQ1I)Zkqgl*NEw1a0^7nYm&L2`f`KMtD#aIV??e6{9;4Pa^Y$^8!s z3rG4`P11=;Q*`)#Ge6biAMQ@s8ygu(cdoC>+CdSmRo;oZ%cY%1!+>F+hL^!OEoCk{ zGPjop$<7tCTjx`>UtRh`%$OT#+M)<_049;=O?fbd0Uh! z&lVO^=2^o_=+=RJ=XSh2tu4e#N31)}njLEC>(i2l4vAmj(YU)FSYTvHfEmVbrU zP!q%Wub-2etvXey%APUKL5*;mV{1sdH0`G$kZK}*{ z-y>)ZrVYx3QZmkwbG;)62@ z9o9C9e9!l7ZOk~Objz0enzL(t`vPHp&j{Y8#|cJy3&BEG1->#0Xk9P*aMquI$IvQ> z*$HUcvmZ=~9uyP|Jnsvt2SHYP<|7yRZ#POD(1yAAUjq{OYTAd)47Y|LO~ ztr`FR^Z+auHups(PNdO?T8O>Hv&7xKyLHEo9TmsI4S!%uHbX3_fzF7z=KFESCdS8E zr6l(Bk$D9LHxuJwm{%dZ%DtY6*TN<3>!@IN-J$qzetX}=NVDFn5eOkPe+9EonMKoe z1#|dRuN$C2Ve{N3v1iXUQX3H4P?tVVtP6aMo)bB;Mg@uE6B7j}{p7np%mpC~9fau> zh97oFZpP&aj`I)(74XLP!Fx5Pd!MpVN+W=g!X<_8fY$PJKhf1|lMo&~X4mZ-^_!lwW8x zVs`Om8>DVr%X%$#vMd~Q`|uH(SKhx>Ap0d*t^PLvQBt)M3FFcu_mqKIr!!}ahzSB< z{KWM1Cf|&9lVWCo?@vG&?`mqY-ucg@{@ic*PD-q?vI5T266~HGIjWru#;hhiqgFQ+cdPbh5&KGM~^O zaaYwnQQBWm!yj_`+&MjL-+g!rTDld{-@tDM5tUPDA}u{V*@6lbF+9%c303QE;N8&l z>p~!o*I7-v1cDecr|G*0yO@jS*h%;Y2s<00w}DO?e)8LO0v_4iqM{Qpt7c?&5|cnE z*`IIi)uD55ZEk+pc4{4Td-$36J^Hs6!=+wUmrZ9!SrmS7?3C zC0S6RHxhmAo`$0Y*LgcQD>`@diM-I*(xsfV$z4g$q4yGUoATAo?*rc-k{hUEW@Z^4 z8fpVJB}}=v*xp$2!aOub@zDK1Ja~0YqJGhkPNYhP!r?{0JtbaV7%1qTeM5xvM}YZlL=Ia_p99m1G39;2!Vh|ES5egBuvDS8 zg+JF#=Xo}JdCjSq(~Ed1{!2M4uzp)#j6K0Xcn?5$UPaV2XaYiZM?{(a&8P|9cOTnC zI1h-oglK5wt6Y60IJ>YQ2;mkqnZ)8Zs4UVOr+(_Nz?1$H~XH z0Trs{M_Rp-G}Od)o5)`s0I&LiPOhQuP-UTk91^#iuHA7O(UT zzaEwR*Y!I!Dd|g2rdTt!ww6kPKPej*<+(`|plMpML-C&4%#k%QO zW-N-W=tM%9Yl#x?FY~Elcv3Z3@Gd7z#i`*1Fzp_~I+m84gsK;>nfspQY2kLt{`cR+ zVJydB0T>TqF)@=oc~^aRcQKCZ%CNnCFf%csf-22y7)x;&O*WlF&EU**yN<-)_cyLz z-wa>J01g@9rwzZ$s`at8Rpa8tQlo>vb_Yy{*0tX++W~dv29EKuJ}+KbOhka;k#uTG zb9z>Uj365KpYGTdzV0G+v8yp;D zvpHmI+jp+@yqlXU{O%5pjt2r)yon8{j2ZA(;332hyko`@=LpX-{_Oc-@Pv=W9!kpn z8W;$jo%PHM7IpH6GnLS}cw%pWq+n{|VU|%ndX41QF0ZMha}}V8xC-dN!mho~oNy&9 zAgB}1gNtBN&<0P=bU~h|*wOO!tJ&lWj6!xPnRA($mxPl96@H z<8vz>@^n2FCdEkl`!8S7L(0QQ}FCSL`^#&;P6Ea*@i0*%wBhq9;xhet;pF_VU;gLWi)W#Q2W zrt9|1+qT^^$#o2N@$hIsJyTW-kBsDsP&NL`h8Q&$fouyVh#0w5Q3<=R=DF`9Ajg$x z#<-Zz8#A%N^OsAer!Rb8erQ&t0*aMcfnxfzz9OHjEC)k9#%wI|o{{M3=!iL84i1j! zA*I8A*(vuud-g0mA_Di-h?=l@KV$OCr|52Mg#P5(nj0H`=DA`BEQ=`)$-{@IWcL39 zAcvT66<5PcE{JJ+w9`-IsBm!cZWoMLb3&Q)Tm0c`XkgIx&^iD9ePSvGnA$&+2-begX2?rNT%Qm0OxI-TJDLw)P9 zqu;;v^hBefP!?wOxoz<@FOM45P}qPs$2O{Bo)Ycgs)GBA%YQ{677Rf5Wxm1|-Km?yknUFqoh#!bwfrkm?i|Qd(uFVYk zd~rr5Cf6Wsg*6V=e*DOo8MyF0d>d82*4r$M#Ncf#O7M(`J8NRq%$~e1EoDJ}N^I<* z3x6=BcT+z0J`3}*(dXqE5n!e(Fzew7D?DuqB5oVR3vwZhKcp0B%T=}+7! z;z0%PQ0wSm1!q|LB=%kb!+G3=krCl?dn`teAuq&A(uZRYZ=u8DKX%NfTvzBvO}!)o zMmz|M2TY=g$;l$8R{Lu=5hNc&J@FEztI4~N@L4gMOsbbeeEya)7{xoELg8ZrT|D<; z5x7MhHZajYoCg?)Niq;GiAhO(kUAOadHMMr+McL0c}c6%)P5LH;*e5+RO1+9!3mM0_8JC1fyYq;6#CupO@p80+xqU z>?{}3jKaQs`&JK!i@o2QCt_fNC{S{MukU4L*-7%K8@Gw^#kF^KhQnG34I6J0q@t!q z=J0xhq~JSs*Zs#aG^_)D0Nq&X15gC`rj(PCl8D^`S_w#TxRaVnlk9XwH>A70ouB^1 zlxvI{FEg*W__;TXJCc+Rl9eLS6cTg!=+=pC#w$vIsK%aLc@#ms4Fcv`ztxH7Y})O_ zq)pq`uWzAWnXunBw6%=|K&^Z8h6+Y^Gud?%Fye1vv7u{(I3WpDnCJ6j9CjCn$&gy5 zr{sPY!W8i4?c1h>%GKrNft=W5T$5TtuZE%Y5m9evmsR)1Dk$g}YTI<9;=19m&ROC` zEFebF@Tu&tM{y+d7<81Fd~R?+!nm~4dU-yxs%ky_wuDhwya1IEtOw9lcLJ>{VFnEM zK@k7&$VqFn_6BbR;{AEhz)!T;SX=KG{Zb@uJ+iWL8QfldeZ8vvPA{xtIL*fTVl{<= zrE7F#q)}&4r*TQYMDTKy2#=fWf!S;QF0O8F7pMD`;R_4FYC#M`Rv^yy(MO}(fh}&p zQn&8|y|<4KKYSKYHeAgG2<4x6+m^R?SzRgcc=Lk3`}Ze#-~UJiKn!!jj4 zp5nTF-0j<67OpL{2JBnVvLB`y?ya9MYxxRGor1In> z@otraA65%RGY4g-skK!o*=Zlley9N&c(DKo%pBJpukuPu-?-Q=Reqm!hu&KE@2QE!wAQgROJVvMdF+m0Q@V`mlY5@>1(4KyM4uk~e2)pav z89xQ7Lx=8TV~z1b!rt1e`iiAV- zIQnK2OG_=Zxp_z-T+rqN@kTvquyFt5WlJY9P9M1PJAWSB@8ab?tO!eHD`C|{C5KRZ z1d};AD0O(V%@3QDJ9kb1vcTCXEw>6q%LUz$b_D6u_Ww*8U?MbIs?PTv>w;tBl8;Z* z_rae(A3S+tR8Srs4$j8~vyX{)?~0$b#pHyHw6uY;a%lVF$gj<&i(1lYcy3~F78xuQ zlgOvWgD+f=Twi!zJphZ^12mDZ#HFQ8>?5M>IdCerY`Jl6PLh}`fL5FGREs`&K}aYV z*8gzL>~mq51Pa%*pXh^+3+hf$`vgS|YIYXZN3t7Upjaq)Pi+@R3_@-TaA=>jvI4jW z!QzNnzhp&_KH1R=H5=3|>O^Q!kw@&GK{YCn7?{+0H@QDv6Yu7TM!9Hu#<^q17IX=D zi%UBHVs73vO)dGQM}sW$FX+5IqShxR!XoG1z3Dpo|D}X84{G{~qHx$OL{t#5w6Yj$ z6*LGc)&L1aAR-YVvMMA2tSnMTW0WG&f)YSmWeKD%Kmw>}EUVCJu~Y+&Z7RyH0xrdv zAS2)gT|khYH~!^}Gl?eoz5DJx=ex&geE5kqRpeEc2rO3gekuiWhaI}A7ElJI4hO;x zwaFZUMGz@M!oo6+E#RuNGBcymhDtQ4$zIMphP(ThXj#Qq;KSWis}p$ri<-5GbM8_y z&$&Z1nV6g`sI7G}H-G%gJ_*|F?%|}aeG~A>+4u}3F3ZOUpGy23yz?0-+#mH0my;#! z5I&zCzaR7hDj?Z{16i(Aue~cNriZMBaiy5xJ611un|qkh%JkMQNR`XopY->0@w`(t z&U`>&XS=$BT#Es4n*TkTtQoSY@hyu(btOnINkb8TP5cfvQmnR}B#9%SaA`>ADT0AO zEZyt>X=WF(Qm>2@VRDxOAAxsTo_0d78QXm@L$tfmn)>*lA-_mH<+3oqxaUND{hAje zBTKVmj48-VEI>9VHdhPbx0AD1Sy}1j-;7oT`qb?{e9y;@B|ru89-LwCh>m8Dj*j+p zcG6OXAV4%@6Ft4X${nv5&81!o zV({n3+ZifRVb-S^JbT$3BgGZ-&bsMCU#wea-dcYiEm{K(OAz*|>ug>sSC*J17^5lc z>F8J-U%0CF9_*x+iZncD-Z;_Xhu>GU_db|jWX-y1awHq0?q-~P@jE>%XsUa94yaD` z!+72Wk}M=Lax=uarm?xm@-$6Yl2yRM z&HAbOL$ZubN9y|`Ah}!7&|!HnqAd*~4l2IPD0rW#>7x#|_rTZ$0S;i%7B*ljN=}wH z$e<;SzfCyK#JzjNdxPYlT;RX0c+1`YG?OhMsG{6;|Hih3W@c>cbdUGNmtIn@)DaAk zJOZ1R7LZ?jh|GB!RcAW>my7ic3@$Y_@%M=H+n;xz-(V(7nlQf z$`I`qIwU8r&%P|yaeu6;I)CSmziTRVf^X4qApv!@Wy(LhoBn;0+Vkjfl^ z^Kjxp??-VIyBI6lPPD8xCUg#FK5ELGZ~)2VdaQngLNW_aI&=izHbC1H7%fOg^~Q^s z{2$kB(cYMucCyNDMxUu2!89&`nZwMvrm8Y{o&kQwonTWjv%DWG zow2u$L>vsVH*)PfYxLXSmqP!S#8{z}Mm_BXl+avX@dBM{|GGA_q zfWGiEB+=1ZHPEoUUxq_(5~hx>dwr0J>CN8SiB8XCFIFKBm!-X)!^XdP;KlGTl1nIP zrm$V;V4aRR9s%AMCa*C)tWc0{B31*PC7wQI%NzVI?4|QDC@7<{wlfr;1Q>7BhgVxy zSEqsxevR&+0K$NwWLsq9v*S+Jtz0}YiJ>8lj*FXxdwdGyKJ_^iCp&PNu*Z4!qiw4b zL|)E8gi6KNX|`ZNkM0!l77yxv2xt3%AbpWM+Hz64X(=OZios;D%B!n$(0~56*$!oM z05N1Re8|dz!F>W{*aTviw_VJDKza&U8tpgqi&A>Qcw+}sOzRJ%N9CIZn%+1@EV>@8*1_&V#S{P&s$ zOtl=v8aTS`@zW5MfP5JM)&V+4B*M##N@PAR3sjtd1Wxky1Z{qsE>&0Gg2~+MY${Bj zPFfYlP7<*)q*Th}fMi|*uG*cku^h0K6&U=5wZkJL=aFKQ1>-{5*mwq|A0}Qtjv)(T zvkTCW#;ThFnsgJv<4B7P>q=Hq;*a^~6Q%F7A$NXW^!Z?cAO{1inK^uDfDjdR+jo_j z9lxbktBDwZ(Xsr*hE3`Zj+GZP%Z%zZ?41`;VRYfLABS0zGt9olKY!qjK z`yu;2WWgJ@09Am$LNamVq+z1|dY6Ixb4ukgkEz$*Zm5v=9y}nI~g1$ zOeW*f;c$!qj&FsHjry96YhMkg2$cyNmIX-Z$bNZ*p~zwe7&ES+yOa=Q64-scC1tAC ztpUC9ZlMZzE6xklsPABnDG>r|>zU>c51kZw^xWqlS4c}s|5|IgU&k{kF%vNtVFfHC zB7zHyBm|dHPEHOfZ%7^^8*{J%5Y$CB(E)B@;bK>BSd8rvk(UZGZwfyuM