From 907c3af139cf7605ee1a3dfc6b051bc51d8ba838 Mon Sep 17 00:00:00 2001 From: Filip Macak Date: Mon, 22 Apr 2024 15:44:45 +0200 Subject: [PATCH] added user friendly SAYNT CLI option; updated README with new options/examples --- README.md | 26 +++++++++++++++++--------- paynt/cli.py | 24 +++++++++++++++++++++--- 2 files changed, 38 insertions(+), 12 deletions(-) diff --git a/README.md b/README.md index 3f65127a7..49cd63dc0 100644 --- a/README.md +++ b/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 diff --git a/paynt/cli.py b/paynt/cli.py index 7241e20e4..2fbad7e20 100644 --- a/paynt/cli.py +++ b/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 )