added user friendly SAYNT CLI option; updated README with new options…

…/examples

README.md

@@ -75,13 +75,20 @@ Options associated with the synthesis of finite-state controllers (FSCs) for a P
 - ``--pomdp-memory-size INTEGER``    implicit memory size for POMDP FSCs [default: 1]
 - ``--fsc-synthesis``: enables incremental synthesis of FSCs for a POMDP using iterative exploration of k-FSCs
 - ``--posterior-aware``: enables the synthesis of posterior aware FSCs
+- ``--native-discount``: runs synthesis with discounted model checking instead of performing model transformation
 
-SAYNT [6] and Storm associated options (pomdp-api branch of Storm and Stormpy are needed):
+SAYNT [6] and New SAYNT [CAV23SI] basic options:
+- ``--saynt``: run SAYNT with default options (15min timeout, to adjust look at advanced SAYNT options)
+- ``--new-saynt``: run SAYNT with computing multiple cut-off FSCs (15min timeout)
+
+Advanced SAYNT [6] and Storm associated options:
 - ``--storm-pomdp``: enables the use of Storm features, this flag is necessary for the other options in this section to work
 - ``--iterative-storm INTEGER INTEGER INTEGER``: runs the SAYNT algorithm, the parameters represent overall timeout, paynt timeout, storm timeout respectivelly. The recommended parameters for 15 minute runtime are 900 60 10
 - ``--get-storm-result INTEGER``: runs PAYNT for specified amount of seconds and then runs Storm using the computed FSC at cut-offs
 - ``--storm-options [cutoff|clip2|clip4|overapp|5mil|10mil|20mil|refine]``: sets the options for Storm [default: ``cutoff``]
 - ``--prune-storm``: if enabled Storm results are used to prune the family of FSCs
+- ``--saynt-threads INTEGER``: specifies the number of cut-off FSCs SAYNT should compute in one iteration, if set to 0 the number is chosen automatically based on the belief exploration
+- ``--saynt-overapprox``: enables the use of overapproximations in choosing from what beliefs FSCs should be computed
 - ``--unfold-strategy-storm [paynt|storm|cutoff]``: sets how the memory is unfolded [default: ``storm``]
 - ``--use-storm-cutoffs``: if enabled the actions from cut-offs are considered in the prioritization and unfolding
 - ``--export-fsc-paynt PATH``: stores the best found FSC from PAYNT to specified file
@@ -91,18 +98,19 @@ Other options:
 - ``--help``: shows the help message of the PAYNT and aborts
 - ``--export [drn|pomdp]``: exports the model to *.drn/*.pomdp and aborts
 - ``--incomplete-search``:  uses incomplete search during synthesis
+- ``--alpha_vector_analysis PATH``: takes alpha vector set from specified file and performs unrolling on the given POMDP using these alpha vectors to analyse their quality 
 
 
 Here are various PAYNT calls:
 ```shell
-python3 paynt.py --project models/cav21/maze --props hard.props
-python3 paynt.py --project models/cav21/maze --props hard.props --method hybrid
-python3 paynt.py --project models/pomdp/uai/grid-avoid-4-0
-python3 paynt.py --project models/pomdp/uai/grid-avoid-4-0 --pomdp-memory-size 2
-python3 paynt.py --project models/pomdp/uai/grid-avoid-4-0 --pomdp-memory-size 5 --method ar_multicore
-timeout 10s python3 paynt.py --project models/pomdp/uai/grid-avoid-4-0 --fsc-synthesis
-python3 paynt.py --project models/pomdp/storm-integration/4x3-95 --fsc-synthesis --storm-pomdp --iterative-storm 180 60 10
-python3 paynt.py --project models/pomdp/storm-integration/rocks-12 --fsc-synthesis --storm-pomdp --get-storm-result 0
+python3 paynt.py --project models/archive/cav21-paynt/maze --props hard.props
+python3 paynt.py --project models/archive/cav21-paynt/maze --props hard.props --method hybrid
+python3 paynt.py --project models/archive/uai22-pomdp/grid-avoid-4-0
+python3 paynt.py --project models/archive/uai22-pomdp/grid-avoid-4-0 --pomdp-memory-size 2
+python3 paynt.py --project models/archive/uai22-pomdp/grid-avoid-4-0 --pomdp-memory-size 5 --method ar_multicore
+timeout 10s python3 paynt.py --project models/archive/uai22-pomdp/grid-avoid-4-0 --fsc-synthesis
+python3 paynt.py --project models/archive/cav23-saynt/4x3-95 --saynt --iterative-storm 180 60 10
+python3 paynt.py --project models/archive/cav23-saynt/rocks-12 --fsc-synthesis --storm-pomdp --get-storm-result 0
 ```
 
 The Python environment can be deactivated by runnning

paynt/cli.py

@@ -114,10 +114,14 @@ def setup_logger(log_path = None):
     type=click.Choice(["storm", "paynt", "cutoff"]),
     show_default=True,
     help="specify memory unfold strategy. Can only be used together with --storm-pomdp flag")
-@click.option("--enhanced-saynt", default=None, type=int,
+@click.option("--saynt-threads", default=None, type=int,
     help="run SAYNT with FSCs for non-initial beliefs. 0 - for dynamic number of different beliefs, N > 0 - set number of different beliefs")
 @click.option("--saynt-overapprox", is_flag=True, default=False,
     help="run Storm to obtain belief value overapproximations that can be used to better choose from what beliefs FSCs should be computed")
+@click.option("--saynt", is_flag=True, default=False,
+    help="run default SAYNT")
+@click.option("--new-saynt", is_flag=True, default=False,
+    help="run SAYNT with multiple cut-offs FSCs")
 
 @click.option("--export-fsc-storm", type=click.Path(), default=None,
     help="path to output file for SAYNT belief FSC")
@@ -165,7 +169,7 @@ def paynt_run(
     incomplete_search, disable_expected_visits,
     fsc_synthesis, pomdp_memory_size, posterior_aware,
     storm_pomdp, iterative_storm, get_storm_result, storm_options, storm_exploration_heuristic, prune_storm,
-    use_storm_cutoffs, unfold_strategy_storm, enhanced_saynt, saynt_overapprox,
+    use_storm_cutoffs, unfold_strategy_storm, saynt_threads, saynt_overapprox, saynt, new_saynt,
     export_fsc_storm, export_fsc_paynt, export_evaluation,
     all_in_one,
     mdp_split_wrt_mdp, mdp_discard_unreachable_choices, mdp_use_randomized_abstraction,
@@ -192,12 +196,26 @@ def paynt_run(
     paynt.synthesizer.policy_tree.SynthesizerPolicyTree.discard_unreachable_choices = mdp_discard_unreachable_choices
     paynt.synthesizer.policy_tree.SynthesizerPolicyTree.use_randomized_abstraction = mdp_use_randomized_abstraction
 
+    # QoL change for calling SAYNT, TODO discuss the default values because this is what we use for 15min timeout
+    if saynt:
+        fsc_synthesis = True
+        storm_pomdp = True
+        if iterative_storm is None:
+            iterative_storm = (900, 60, 10)
+    elif new_saynt:
+        fsc_synthesis = True
+        storm_pomdp = True
+        if iterative_storm is None:
+            iterative_storm = (900, 90, 2)
+        if saynt_threads is None:
+            saynt_threads = 0
+
     storm_control = None
     if storm_pomdp:
         storm_control = paynt.quotient.storm_pomdp_control.StormPOMDPControl()
         storm_control.set_options(
             storm_options, get_storm_result, iterative_storm, use_storm_cutoffs,
-            unfold_strategy_storm, prune_storm, export_fsc_storm, export_fsc_paynt, enhanced_saynt, saynt_overapprox,
+            unfold_strategy_storm, prune_storm, export_fsc_storm, export_fsc_paynt, saynt_threads, saynt_overapprox,
             storm_exploration_heuristic
         )