diff --git a/learning/paynt-learner.dockerfile b/learning/paynt-learner.dockerfile deleted file mode 100644 index 10d92225e..000000000 --- a/learning/paynt-learner.dockerfile +++ /dev/null @@ -1,8 +0,0 @@ -ARG paynt_base=randriu/paynt:ci -FROM $paynt_base - -RUN pip install torch==2.1.* - -RUN pip install ipykernel joblib tensorboard==2.15.* einops==0.7.* gym==0.22.* pygame==2.5.* - -WORKDIR /opt/learning diff --git a/learning/paynt_pomdp_sketch.py b/learning/paynt_pomdp_sketch.py deleted file mode 100644 index 08471c3ef..000000000 --- a/learning/paynt_pomdp_sketch.py +++ /dev/null @@ -1,127 +0,0 @@ -# using Paynt for POMDP sketches - -import paynt.cli -import paynt.parser.sketch -import paynt.quotient.pomdp_family -import paynt.synthesizer.synthesizer_onebyone -import paynt.synthesizer.synthesizer_ar - -import os -import random -import cProfile, pstats - -def load_sketch(project_path): - project_path = os.path.abspath(project_path) - sketch_path = os.path.join(project_path, "sketch.templ") - properties_path = os.path.join(project_path, "sketch.props") - pomdp_sketch = paynt.parser.sketch.Sketch.load_sketch(sketch_path, properties_path) - - target_label = pomdp_sketch.get_property().get_target_label() - target_states = pomdp_sketch.quotient_mdp.labeling.get_states(target_label) - for state in pomdp_sketch.quotient_mdp.labeling.get_states("deadlock"): - assert state in target_states, "have deadlock in a non-target state {}".format(state) - - return pomdp_sketch - - -def investigate_hole_assignment(pomdp_sketch, hole_assignment): - print("investigating hole assignment: ", hole_assignment) - pomdp = pomdp_sketch.build_pomdp(hole_assignment) - - # create a random k-FSC - fsc_is_deterministic = False - num_nodes = 3 - fsc = paynt.quotient.pomdp_family.FSC(num_nodes, pomdp_sketch.num_observations, fsc_is_deterministic) - fsc.fill_trivial_actions(pomdp_sketch.observation_to_actions) - # fsc.fill_trivial_updates(pomdp_sketch.observation_to_actions) - for node in range(num_nodes): - for obs in range(pomdp_sketch.num_observations): - available_actions = pomdp_sketch.observation_to_actions[obs] - if fsc.is_deterministic: - # random deterministic FSC - fsc.action_function[node][obs] = random.choice(available_actions) - else: - # random randomized FSC - num_samples = min(len(available_actions),node+1) - sampled_actions = random.sample(available_actions,num_samples) - prob = 1/num_samples - randomized_action_selection = {action:prob for action in sampled_actions} - fsc.action_function[node][obs] = randomized_action_selection - - fsc.update_function[node][obs] = random.randrange(num_nodes) - - return fsc - -def compute_qvalues(pomdp_sketch, dtmc_sketch): - print() - subfamily = dtmc_sketch.design_space - dtmc_sketch.build(subfamily) - print("computing Q-values...") - qvalues = pomdp_sketch.compute_qvalues_for_product_submdp(subfamily.mdp) - print("Q-values computed") - -def evaluate_all(dtmc_sketch): - ''' To each singleton environment, assign a value corresponding to the specification satisfiability. ''' - print() - synthesizer = paynt.synthesizer.synthesizer_onebyone.SynthesizerOneByOne(dtmc_sketch) - family_to_value = synthesizer.evaluate(keep_value_only=True) - - # pick the worst family - import numpy - values = numpy.array([value for family,value in family_to_value]) - if dtmc_sketch.get_property().minimizing: - worst_index = values.argmax() - else: - worst_index = values.argmin() - - worst_family,worst_value = family_to_value[worst_index] - print("the worst family has value {}, printing the family below:".format(worst_value)) - print(worst_family) - -def synthesize_worst(dtmc_sketch): - '''Identify assignment with the worst specification satisfiability.''' - print() - dtmc_sketch.specification = dtmc_sketch.specification.negate() - dtmc_sketch.specification.optimality.epsilon = 0.05 - synthesizer = paynt.synthesizer.synthesizer_ar.SynthesizerAR(dtmc_sketch) - worst_assignment = synthesizer.synthesize(return_all=True) - - -profiling = False - -if profiling: - profiler = cProfile.Profile() - profiler.enable() - - -# random.seed(11) - -# enable PAYNT logging -paynt.cli.setup_logger() - -# load sketch -project_path="models/pomdp/sketches/obstacles" -# project_path="models/pomdp/sketches/avoid" -pomdp_sketch = load_sketch(project_path) -print("specification: ", pomdp_sketch.specification) -print("design space:\n", pomdp_sketch.design_space) -print("number of holes: ", pomdp_sketch.design_space.num_holes) -print("design space size: {} members".format(pomdp_sketch.design_space.size)) - -# fix some hole options -hole_assignment = pomdp_sketch.design_space.pick_any() - -# investigate this hole assignment and return an FSC -fsc = investigate_hole_assignment(pomdp_sketch, hole_assignment) - -# apply this FSC to a POMDP sketch, obtaining a DTMC sketch -dtmc_sketch = pomdp_sketch.build_dtmc_sketch(fsc) - -# compute_qvalues(pomdp_sketch, dtmc_sketch) -# evaluate_all(dtmc_sketch) -# synthesize_worst(dtmc_sketch) - -if profiling: - profiler.disable() - stats = profiler.create_stats() - pstats.Stats(profiler).sort_stats('tottime').print_stats(20) diff --git a/models/mdp/obstacles/sketch.templ b/models/mdp/obstacles/sketch.templ index a0985de1d..76010472b 100755 --- a/models/mdp/obstacles/sketch.templ +++ b/models/mdp/obstacles/sketch.templ @@ -1,65 +1,47 @@ -mdp - -const int N = 10; -const int gMIN = 1; -const int gMAX = N; - -const int o1x = 2; -const int o1y = 2; - -const int o2x = 2; -const int o2y = 6; - -const int o3x = 4; -const int o3y = 3; - -const int o4x = 3; -const int o4y = 6; - -const int o5x = 5; -const int o5y = 5; - -const int o6x = 8; -const int o6y = 8; - -formula at1 = (x = o1x & y = o1y); -formula at2 = (x = o2x & y = o2y); -formula at3 = (x = o3x & y = o3y); -formula at4 = (x = o4x & y = o4y); -formula at5 = (x = o5x & y = o5y); -formula at6 = (x = o6x & y = o6y); - -formula crash = at1 | at2 | at3 | at4 | at5 | at6; -formula goal = (x=gMAX & y=gMAX); - -label "notbad" = !crash; -label "goal" = goal; - - -const double slip = 0.2; - -formula al = min(max(x-1,gMIN),gMAX); -formula all = min(max(x-2,gMIN),gMAX); -formula ar = min(max(x+1,gMIN),gMAX); -formula arr = min(max(x+2,gMIN),gMAX); -formula au = min(max(y-1,gMIN),gMAX); -formula auu = min(max(y-2,gMIN),gMAX); -formula ad = min(max(y+1,gMIN),gMAX); -formula add = min(max(y+2,gMIN),gMAX); - -module agent - x : [gMIN..gMAX] init gMIN; - y : [gMIN..gMAX] init gMIN; - - [le] !crash -> 1-slip : (x'=al) + slip : (x'=all); - [ri] !crash -> 1-slip : (x'=ar) + slip : (x'=arr); - [up] !crash -> 1-slip : (y'=au) + slip : (y'=auu); - [do] !crash -> 1-slip : (y'=ad) + slip : (y'=add); -endmodule - -rewards "steps" - [le] true: 1; - [ri] true: 1; - [up] true: 1; - [do] true: 1; -endrewards \ No newline at end of file +mdp + +const int N = 10; +const int gMIN = 1; +const int gMAX = N; + +formula at1 = (x = 1 & y = 5); +formula at2 = (x = 5 & y = 1); +formula at3 = (x = 2 & y = 2); +formula at4 = (x = 9 & y = 10); +formula at5 = (x = 9 & y = 9); +formula at6 = (x = 2 & y = 5); + +formula crash = at1 | at2 | at3 | at4 | at5 | at6; +formula goal = (x=gMAX & y=gMAX); + +label "notbad" = !crash; +label "goal" = goal; + + +const double slip = 0.2; + +formula al = min(max(x-1,gMIN),gMAX); +formula all = min(max(x-2,gMIN),gMAX); +formula ar = min(max(x+1,gMIN),gMAX); +formula arr = min(max(x+2,gMIN),gMAX); +formula au = min(max(y-1,gMIN),gMAX); +formula auu = min(max(y-2,gMIN),gMAX); +formula ad = min(max(y+1,gMIN),gMAX); +formula add = min(max(y+2,gMIN),gMAX); + +module agent + x : [gMIN..gMAX] init gMIN; + y : [gMIN..gMAX] init gMIN; + + [le] !crash -> 1-slip : (x'=al) + slip : (x'=all); + [ri] !crash -> 1-slip : (x'=ar) + slip : (x'=arr); + [up] !crash -> 1-slip : (y'=au) + slip : (y'=auu); + [do] !crash -> 1-slip : (y'=ad) + slip : (y'=add); +endmodule + +rewards "steps" + [le] true: 1; + [ri] true: 1; + [up] true: 1; + [do] true: 1; +endrewards diff --git a/paynt/parser/sketch.py b/paynt/parser/sketch.py index 269fa9671..2f86bc538 100644 --- a/paynt/parser/sketch.py +++ b/paynt/parser/sketch.py @@ -117,7 +117,11 @@ def load_sketch(cls, sketch_path, properties_path, logger.info("sketch parsing OK") paynt.verification.property.Property.initialize() - + + updated = payntbind.synthesis.addMissingChoiceLabels(explicit_quotient) + if updated is not None: explicit_quotient = updated + payntbind.synthesis.assertChoiceLabelingIsCanonic(explicit_quotient.choice_labeling) + make_rewards_action_based(explicit_quotient) logger.debug("constructed explicit quotient having {} states and {} actions".format( explicit_quotient.nr_states, explicit_quotient.nr_choices)) diff --git a/paynt/quotient/mdp.py b/paynt/quotient/mdp.py index 6196bb917..e747cf543 100644 --- a/paynt/quotient/mdp.py +++ b/paynt/quotient/mdp.py @@ -190,12 +190,12 @@ def custom_decision_tree(mdp): if model == "obstacles": decide(dt.root, "x") - # decide(dt.root.child_true, "x") - # decide(dt.root.child_true.child_true, "y") - # decide(dt.root.child_true.child_false, "y") + decide(dt.root.child_true, "x") + decide(dt.root.child_true.child_true, "y") + decide(dt.root.child_true.child_false, "y") decide(dt.root.child_false, "x") - # decide(dt.root.child_false.child_true, "y") - # decide(dt.root.child_false.child_false, "y") + decide(dt.root.child_false.child_true, "y") + decide(dt.root.child_false.child_false, "y") return dt @@ -206,11 +206,13 @@ class MdpQuotient(paynt.quotient.quotient.Quotient): def __init__(self, mdp, specification): super().__init__(specification=specification) - mdp = payntbind.synthesis.restoreActionsInAbsorbingStates(mdp) + updated = payntbind.synthesis.restoreActionsInAbsorbingStates(mdp) + if updated is not None: mdp = updated + self.quotient_mdp = mdp paynt_mdp = paynt.models.models.Mdp(mdp) logger.info(f"optimal scheduler has value: {paynt_mdp.model_check_property(self.get_property())}") - self.choice_destinations = payntbind.synthesis.computeChoiceDestinations(self.quotient_mdp) + self.choice_destinations = payntbind.synthesis.computeChoiceDestinations(mdp) self.action_labels,self.choice_to_action = payntbind.synthesis.extractActionLabels(mdp) decision_tree = custom_decision_tree(mdp) diff --git a/paynt/quotient/mdp_family.py b/paynt/quotient/mdp_family.py index 9a9cb4ef2..37789aa71 100644 --- a/paynt/quotient/mdp_family.py +++ b/paynt/quotient/mdp_family.py @@ -53,7 +53,7 @@ def __init__(self, quotient_mdp, family, coloring, specification): # for each state of the quotient, a list of available actions self.state_to_actions = None - self.action_labels,self.choice_to_action = payntbind.synthesis.extractActionLabels(mdp) + self.action_labels,self.choice_to_action = payntbind.synthesis.extractActionLabels(quotient_mdp) self.num_actions = len(self.action_labels) self.state_action_choices = MdpFamilyQuotient.map_state_action_to_choices( self.quotient_mdp, self.num_actions, self.choice_to_action) diff --git a/payntbind/src/synthesis/quotient/JaniChoices.cpp b/payntbind/src/synthesis/quotient/JaniChoices.cpp index 4615160e5..4e03808ff 100644 --- a/payntbind/src/synthesis/quotient/JaniChoices.cpp +++ b/payntbind/src/synthesis/quotient/JaniChoices.cpp @@ -1,4 +1,5 @@ #include "JaniChoices.h" +#include "src/synthesis/translation/choiceTransformation.h" #include #include @@ -27,37 +28,9 @@ namespace synthesis { choice_labeling.addLabelToChoice(jani.getAction(action_index).getName(), choice); } } - - return choice_labeling; - } - /** - * Given model and its choice labeling, remove unused labels and make sure that all choices have at most 1 label. - * If the choice does not have a label, label it with the label derived from the provided prefix. - * Make sure that for each state of the MDP, either all its rows have no labels or all its rows have exactly one - */ - template - void makeChoiceLabelingCanonic( - storm::models::sparse::Model const& model, - storm::models::sparse::ChoiceLabeling& choice_labeling, - std::string const& no_label_prefix - ) { - for(auto const& label: choice_labeling.getLabels()) { - if(choice_labeling.getChoices(label).empty()) { - choice_labeling.removeLabel(label); - } - } - storm::storage::BitVector no_label_labeling(model.getNumberOfChoices()); - for(uint64_t choice = 0; choice < model.getNumberOfChoices(); choice++) { - uint64_t choice_num_labels = choice_labeling.getLabelsOfChoice(choice).size(); - if(choice_num_labels > 1) { - throw std::invalid_argument("A choice of the model contains multiple labels."); - } - if(choice_num_labels == 0) { - no_label_labeling.set(choice,true); - } - } - std::string empty_label = choice_labeling.addUniqueLabel(no_label_prefix, no_label_labeling); + removeUnusedLabels(choice_labeling); + return choice_labeling; } template @@ -68,9 +41,8 @@ namespace synthesis { if(model.hasStateValuations()) { components.stateValuations = model.getStateValuations(); } - storm::models::sparse::ChoiceLabeling choice_labeling = reconstructChoiceLabelsFromJani(model); - makeChoiceLabelingCanonic(model,choice_labeling,"empty_label"); - components.choiceLabeling = choice_labeling; + components.choiceLabeling = reconstructChoiceLabelsFromJani(model); + addMissingChoiceLabelsLabeling(model,components.choiceLabeling.value()); components.rewardModels = model.getRewardModels(); return std::make_shared>(std::move(components)); } diff --git a/payntbind/src/synthesis/translation/bindings.cpp b/payntbind/src/synthesis/translation/bindings.cpp index 6254650c0..42cb9a701 100644 --- a/payntbind/src/synthesis/translation/bindings.cpp +++ b/payntbind/src/synthesis/translation/bindings.cpp @@ -2,212 +2,18 @@ #include "SubPomdpBuilder.h" #include "src/synthesis/translation/componentTranslations.h" +#include "src/synthesis/translation/choiceTransformation.h" #include #include #include -namespace synthesis { - -/** - * Add an explicit label to the choices that do not have any. - */ -template -std::shared_ptr> addMissingChoiceLabels( - storm::models::sparse::Model const& model -) { - STORM_LOG_THROW(model.hasChoiceLabeling(), storm::exceptions::InvalidModelException, "model does not have the choice labeling"); - - storm::storage::sparse::ModelComponents components; - components.stateLabeling = model.getStateLabeling(); - components.stateValuations = model.getOptionalStateValuations(); - components.transitionMatrix = model.getTransitionMatrix(); - components.choiceLabeling = model.getChoiceLabeling(); - components.choiceOrigins = model.getOptionalChoiceOrigins(); - components.rewardModels = model.getRewardModels(); - - auto const& labeling = model.getChoiceLabeling(); - storm::storage::BitVector choices_without_label(model.getNumberOfChoices(),false); - for(uint64_t choice = 0; choice < model.getNumberOfChoices(); ++choice) { - if(labeling.getLabelsOfChoice(choice).empty()) { - choices_without_label.set(choice,true); - } - } - const std::string NO_ACTION_LABEL = "__no_label__"; - if(not choices_without_label.empty()) { - components.choiceLabeling->addUniqueLabel(NO_ACTION_LABEL,choices_without_label); - } - if (model.getType() == storm::models::ModelType::Pomdp) { - auto pomdp = static_cast const&>(model); - components.observabilityClasses = pomdp.getObservations(); - components.observationValuations = pomdp.getOptionalObservationValuations(); - } - - return storm::utility::builder::buildModelFromComponents(model.getType(),std::move(components)); -} - - -/** - * Given an MDP with canonic choice labeling, make sure that in each state from the provided \p state_maks all actions - * are available. If an action is not available in a state, add it to this state with the behavior of the first - * existing action. - */ -template -std::shared_ptr> enableAllActions( - storm::models::sparse::Model const& model, - storm::storage::BitVector const& state_mask -) { - auto [action_labels,choice_to_action] = synthesis::extractActionLabels(model); - uint64_t num_actions = action_labels.size(); - uint64_t num_states = model.getNumberOfStates(); - uint64_t num_choices = model.getNumberOfChoices(); - - // for each action, find some choice that corresponds to this action - std::vector action_reference_choice(num_actions); - for(uint64_t choice = 0; choice < num_choices; ++choice) { - action_reference_choice[choice_to_action[choice]] = choice; - } - - // for each state-action pair, find the corresponding choice - // translate choices - auto const& row_groups_old = model.getTransitionMatrix().getRowGroupIndices(); - std::vector translated_to_original_choice; - std::vector translated_to_original_choice_label; - std::vector row_groups_new; - for(uint64_t state = 0; state < num_states; ++state) { - row_groups_new.push_back(translated_to_original_choice.size()); - if(not state_mask[state]) { - for(uint64_t choice: model.getTransitionMatrix().getRowGroupIndices(state)) { - translated_to_original_choice.push_back(choice); - translated_to_original_choice_label.push_back(choice); - } - } else { - std::vector action_exists(num_actions,false); - for(uint64_t choice: model.getTransitionMatrix().getRowGroupIndices(state)) { - uint64_t action = choice_to_action[choice]; - action_exists[action] = true; - translated_to_original_choice.push_back(choice); - translated_to_original_choice_label.push_back(choice); - } - for(uint64_t action = 0; action < num_actions; ++action) { - if(action_exists[action]) { - continue; - } - uint64_t choice = row_groups_old[state]; - translated_to_original_choice.push_back(choice); - translated_to_original_choice_label.push_back(action_reference_choice[action]); - } - } - } - row_groups_new.push_back(translated_to_original_choice.size()); - uint64_t num_translated_choices = translated_to_original_choice.size(); - - // build components - storm::storage::sparse::ModelComponents components; - components.stateLabeling = model.getStateLabeling(); - components.stateValuations = model.getOptionalStateValuations(); - storm::storage::BitVector translated_choice_mask(num_translated_choices,true); - components.choiceLabeling = synthesis::translateChoiceLabeling(model,translated_to_original_choice_label,translated_choice_mask); - - storm::storage::SparseMatrixBuilder builder(num_translated_choices, num_states, 0, true, true, num_states); - for(uint64_t state = 0; state < num_states; ++state) { - builder.newRowGroup(row_groups_new[state]); - for(uint64_t translated_choice = row_groups_new[state]; translated_choice < row_groups_new[state+1]; ++translated_choice) { - uint64_t choice = translated_to_original_choice[translated_choice]; - for(auto entry: model.getTransitionMatrix().getRow(choice)) { - builder.addNextValue(translated_choice, entry.getColumn(), entry.getValue()); - } - } - } - components.transitionMatrix = builder.build(); - - components.rewardModels = synthesis::translateRewardModels(model,translated_to_original_choice,translated_choice_mask); - - if (model.getType() == storm::models::ModelType::Pomdp) { - auto pomdp = static_cast const&>(model); - components.observabilityClasses = pomdp.getObservations(); - components.observationValuations = pomdp.getOptionalObservationValuations(); - } - - return storm::utility::builder::buildModelFromComponents>(model.getType(),std::move(components)); -} - -/** - * Given an MDP with canonic choice labeling, remove an action from the given set \p state_mask of states. - */ -template -std::shared_ptr> removeAction( - storm::models::sparse::Model const& model, - std::string const& action_to_remove_label, - storm::storage::BitVector const& state_mask -) { - auto [action_labels,choice_to_action] = synthesis::extractActionLabels(model); - uint64_t num_actions = action_labels.size(); - uint64_t num_states = model.getNumberOfStates(); - uint64_t num_choices = model.getNumberOfChoices(); - uint64_t action_to_remove = num_actions; - for(action_to_remove = 0; action_to_remove < num_actions; ++action_to_remove) { - if(action_labels[action_to_remove] == action_to_remove_label) { - break; - } - } - - storm::storage::BitVector choice_enabled(num_choices,true); - for(uint64_t state: state_mask) { - for(uint64_t choice: model.getTransitionMatrix().getRowGroupIndices(state)) { - uint64_t action = choice_to_action[choice]; - if(action == action_to_remove) { - choice_enabled.set(choice,false); - } - } - } - storm::storage::BitVector all_states(num_states,true); - storm::transformer::SubsystemBuilderReturnType build_result = storm::transformer::buildSubsystem(model, all_states, choice_enabled); - return build_result.model; -} - -/** - * Given an MDP, for any absorbing state with an unlabeled action, explicitly add all availabled actions and - * subsequently remove these unlabeled actions. - */ -template -std::shared_ptr> restoreActionsInAbsorbingStates( - storm::models::sparse::Model const& model -) { - auto model_canonic = synthesis::addMissingChoiceLabels(model); - const std::string NO_ACTION_LABEL = "__no_label__"; - storm::storage::BitVector const& no_action_label_choices = model_canonic->getChoiceLabeling().getChoices(NO_ACTION_LABEL); - storm::storage::BitVector absorbing_states(model.getNumberOfStates(),true); - for(uint64_t state = 0; state < model.getNumberOfStates(); ++state) { - bool state_is_absorbing = true; - for(uint64_t choice: model_canonic->getTransitionMatrix().getRowGroupIndices(state)) { - if(not no_action_label_choices[choice]) { - absorbing_states.set(state,false); - break; - } - for(auto const& entry: model_canonic->getTransitionMatrix().getRow(choice)) { - if(entry.getColumn() != state) { - absorbing_states.set(state,false); - break; - } - } - if(not absorbing_states[state]) { - break; - } - } - } - auto model_target_enabled = synthesis::enableAllActions(*model_canonic, absorbing_states); - auto model_target_fixed = synthesis::removeAction(*model_target_enabled, NO_ACTION_LABEL, absorbing_states); - return model_target_fixed; -} - -} - void bindings_translation(py::module& m) { - m.def("addMissingChoiceLabels", &synthesis::addMissingChoiceLabels); + m.def("addMissingChoiceLabels", &synthesis::addMissingChoiceLabelsModel); + m.def("assertChoiceLabelingIsCanonic", &synthesis::assertChoiceLabelingIsCanonic); m.def("extractActionLabels", &synthesis::extractActionLabels); - m.def("enableAllActions", &synthesis::enableAllActions); + m.def("enableAllActions", py::overload_cast const&>(&synthesis::enableAllActions)); m.def("restoreActionsInAbsorbingStates", &synthesis::restoreActionsInAbsorbingStates); py::class_, std::shared_ptr>>(m, "SubPomdpBuilder") diff --git a/payntbind/src/synthesis/translation/choiceTransformation.cpp b/payntbind/src/synthesis/translation/choiceTransformation.cpp new file mode 100644 index 000000000..aa187f6e7 --- /dev/null +++ b/payntbind/src/synthesis/translation/choiceTransformation.cpp @@ -0,0 +1,281 @@ +#include "choiceTransformation.h" + +#include "src/synthesis/translation/componentTranslations.h" + +#include +#include +#include +#include +#include + +namespace synthesis { + +template +void addMissingChoiceLabelsLabeling( + storm::models::sparse::Model const& model, + storm::models::sparse::ChoiceLabeling& choice_labeling +) { + storm::storage::BitVector choice_has_no_label(model.getNumberOfChoices(),false); + for(uint64_t choice = 0; choice < model.getNumberOfChoices(); ++choice) { + if(choice_labeling.getLabelsOfChoice(choice).size() == 0) { + choice_has_no_label.set(choice,true); + } + } + if(choice_has_no_label.empty()) { + return; + } + STORM_LOG_THROW(not choice_labeling.containsLabel(NO_ACTION_LABEL), storm::exceptions::InvalidModelException, "model already has the '" << NO_ACTION_LABEL << "' label"); + choice_labeling.addLabel(NO_ACTION_LABEL, choice_has_no_label); +} + +template +std::shared_ptr> addMissingChoiceLabelsModel( + storm::models::sparse::Model const& model +) { + storm::storage::sparse::ModelComponents components = componentsFromModel(model); + addMissingChoiceLabelsLabeling(model,components.choiceLabeling.value()); + if(not components.choiceLabeling.value().containsLabel(NO_ACTION_LABEL)) { + return NULL; + } + return storm::utility::builder::buildModelFromComponents(model.getType(),std::move(components)); +} + +void assertChoiceLabelingIsCanonic(storm::models::sparse::ChoiceLabeling const& choice_labeling) { + for(uint64_t choice = 0; choice < choice_labeling.getNumberOfItems(); ++choice) { + auto const& labels = choice_labeling.getLabelsOfChoice(choice); + STORM_LOG_THROW(labels.size()==1, storm::exceptions::InvalidModelException, "expected exactly 1 label for choice " << choice); + } +} + +void removeUnusedLabels(storm::models::sparse::ChoiceLabeling & choice_labeling) { + for(auto const& label: choice_labeling.getLabels()) { + if(choice_labeling.getChoices(label).empty()) { + choice_labeling.removeLabel(label); + } + } +} + + +template +std::pair,std::vector> extractActionLabels( + storm::models::sparse::Model const& model +) { + // collect action labels + storm::models::sparse::ChoiceLabeling const& choice_labeling = model.getChoiceLabeling(); + std::vector action_labels; + std::map action_label_index; + std::set action_labels_set; + for(uint64_t choice = 0; choice < model.getNumberOfChoices(); ++choice) { + for(std::string const& label: choice_labeling.getLabelsOfChoice(choice)) { + action_labels_set.insert(label); + } + } + for(std::string const& label: action_labels_set) { + action_label_index[label] = action_labels.size(); + action_labels.push_back(label); + } + + assertChoiceLabelingIsCanonic(choice_labeling); + std::vector choice_to_action(model.getNumberOfChoices()); + for(uint64_t choice = 0; choice < model.getNumberOfChoices(); ++choice) { + auto const& labels = choice_labeling.getLabelsOfChoice(choice); + std::string const& label = *(labels.begin()); + uint64_t action = action_label_index[label]; + choice_to_action[choice] = action; + } + return std::make_pair(action_labels,choice_to_action); +} + +template +std::pair>,std::vector> enableAllActions( + storm::models::sparse::Model const& model +) { + storm::storage::BitVector all_states(model.getNumberOfStates(),true); + return enableAllActions(model,all_states); +} + +template +std::pair>,std::vector> enableAllActions( + storm::models::sparse::Model const& model, + storm::storage::BitVector const& state_mask +) { + auto [action_labels,choice_to_action] = synthesis::extractActionLabels(model); + uint64_t num_actions = action_labels.size(); + uint64_t num_states = model.getNumberOfStates(); + uint64_t num_choices = model.getNumberOfChoices(); + + // for each action, find any choice that corresponds to this action + // we compute this to easily build choice labeling later + std::vector action_reference_choice(num_actions); + for(uint64_t choice = 0; choice < num_choices; ++choice) { + action_reference_choice[choice_to_action[choice]] = choice; + } + std::vector translated_to_true_action; + + // for each state-action pair, find the corresponding choice + // translate choices + auto const& row_groups_old = model.getTransitionMatrix().getRowGroupIndices(); + std::vector translated_to_original_choice; + std::vector translated_to_original_choice_label; + std::vector row_groups_new; + storm::storage::BitVector action_exists(num_actions,false); + for(uint64_t state = 0; state < num_states; ++state) { + row_groups_new.push_back(translated_to_original_choice.size()); + if(not state_mask[state]) { + // keep choices + for(uint64_t choice: model.getTransitionMatrix().getRowGroupIndices(state)) { + translated_to_original_choice.push_back(choice); + translated_to_original_choice_label.push_back(choice); + translated_to_true_action.push_back(choice_to_action[choice]); + } + } else { + // identify existing actions + action_exists.clear(); + for(uint64_t choice: model.getTransitionMatrix().getRowGroupIndices(state)) { + uint64_t action = choice_to_action[choice]; + action_exists.set(action,true); + translated_to_original_choice.push_back(choice); + translated_to_original_choice_label.push_back(choice); + translated_to_true_action.push_back(action); + } + // add missing actions + for(uint64_t action: ~action_exists) { + uint64_t default_choice = row_groups_old[state]; + translated_to_original_choice.push_back(default_choice); + translated_to_original_choice_label.push_back(action_reference_choice[action]); + translated_to_true_action.push_back(choice_to_action[default_choice]); + } + } + } + row_groups_new.push_back(translated_to_original_choice.size()); + uint64_t num_translated_choices = translated_to_original_choice.size(); + + // build components + storm::storage::sparse::ModelComponents components = componentsFromModel(model); + components.choiceOrigins.reset(); + storm::storage::BitVector translated_choice_mask(num_translated_choices,true); + components.choiceLabeling = synthesis::translateChoiceLabeling(model,translated_to_original_choice_label,translated_choice_mask); + storm::storage::SparseMatrixBuilder builder(num_translated_choices, num_states, 0, true, true, num_states); + for(uint64_t state = 0; state < num_states; ++state) { + builder.newRowGroup(row_groups_new[state]); + for(uint64_t translated_choice = row_groups_new[state]; translated_choice < row_groups_new[state+1]; ++translated_choice) { + uint64_t choice = translated_to_original_choice[translated_choice]; + for(auto entry: model.getTransitionMatrix().getRow(choice)) { + builder.addNextValue(translated_choice, entry.getColumn(), entry.getValue()); + } + } + } + components.transitionMatrix = builder.build(); + components.rewardModels = synthesis::translateRewardModels(model,translated_to_original_choice,translated_choice_mask); + auto new_model = storm::utility::builder::buildModelFromComponents>(model.getType(),std::move(components)); + return std::make_pair(new_model,translated_to_true_action); +} + + +template +std::shared_ptr> removeAction( + storm::models::sparse::Model const& model, + std::string const& action_to_remove_label, + storm::storage::BitVector const& state_mask +) { + auto [action_labels,choice_to_action] = synthesis::extractActionLabels(model); + uint64_t num_actions = action_labels.size(); + uint64_t num_states = model.getNumberOfStates(); + uint64_t num_choices = model.getNumberOfChoices(); + // identify action to remove + uint64_t action_to_remove = num_actions; + for(action_to_remove = 0; action_to_remove < num_actions; ++action_to_remove) { + if(action_labels[action_to_remove] == action_to_remove_label) { + break; + } + } + if(action_to_remove == num_actions) { + return NULL; + } + + // identify choices to remove + storm::storage::BitVector choice_enabled(num_choices,true); + for(uint64_t state: state_mask) { + for(uint64_t choice: model.getTransitionMatrix().getRowGroupIndices(state)) { + if(choice_to_action[choice] == action_to_remove) { + choice_enabled.set(choice,false); + } + } + } + if(choice_enabled.full()) { + return NULL; + } + + // construct the corresponding sub-MDP + storm::storage::BitVector all_states(num_states,true); + storm::storage::sparse::ModelComponents components = componentsFromModel(model); + if((model.getChoiceLabeling().getChoices(action_to_remove_label) & choice_enabled).empty()) { + components.choiceLabeling.value().removeLabel(action_to_remove_label); + } + std::shared_ptr> mdp = storm::utility::builder::buildModelFromComponents(storm::models::ModelType::Mdp,std::move(components)); + storm::transformer::SubsystemBuilderReturnType build_result = storm::transformer::buildSubsystem(*mdp, all_states, choice_enabled); + std::shared_ptr> submdp = build_result.model; + if (model.getType() != storm::models::ModelType::Pomdp) { + return submdp; + } + components = componentsFromModel(*submdp); + components.observabilityClasses = translateObservabilityClasses(model,build_result.newToOldStateIndexMapping); + return storm::utility::builder::buildModelFromComponents(model.getType(),std::move(components)); +} + + +template +std::shared_ptr> restoreActionsInAbsorbingStates( + storm::models::sparse::Model const& model +) { + auto model_canonic = addMissingChoiceLabelsModel(model); + if(model_canonic == NULL) { + return NULL; + } + assertChoiceLabelingIsCanonic(model_canonic->getChoiceLabeling()); + storm::storage::BitVector const& no_action_label_choices = model_canonic->getChoiceLabeling().getChoices(NO_ACTION_LABEL); + storm::storage::BitVector absorbing_states(model.getNumberOfStates(),true); + for(uint64_t state = 0; state < model.getNumberOfStates(); ++state) { + for(uint64_t choice: model_canonic->getTransitionMatrix().getRowGroupIndices(state)) { + if(not no_action_label_choices[choice]) { + absorbing_states.set(state,false); + break; + } + for(auto const& entry: model_canonic->getTransitionMatrix().getRow(choice)) { + if(entry.getColumn() != state) { + absorbing_states.set(state,false); + break; + } + } + if(not absorbing_states[state]) { + break; + } + } + } + if(absorbing_states.empty()) { + return NULL; + } + auto [model_absorbing_enabled,translated_to_true_action] = synthesis::enableAllActions(*model_canonic, absorbing_states); + return synthesis::removeAction(*model_absorbing_enabled, NO_ACTION_LABEL, absorbing_states); +} + +template std::pair,std::vector> extractActionLabels( + storm::models::sparse::Model const& model); +template void addMissingChoiceLabelsLabeling( + storm::models::sparse::Model const& model, + storm::models::sparse::ChoiceLabeling& choice_labeling); +template std::shared_ptr> addMissingChoiceLabelsModel( + storm::models::sparse::Model const& model); +template std::pair>,std::vector> enableAllActions( + storm::models::sparse::Model const& model); +template std::pair>,std::vector> enableAllActions( + storm::models::sparse::Model const& model, + storm::storage::BitVector const& state_mask); +template std::shared_ptr> removeAction( + storm::models::sparse::Model const& model, + std::string const& action_to_remove_label, + storm::storage::BitVector const& state_mask); +template std::shared_ptr> restoreActionsInAbsorbingStates( + storm::models::sparse::Model const& model); + +} diff --git a/payntbind/src/synthesis/translation/choiceTransformation.h b/payntbind/src/synthesis/translation/choiceTransformation.h new file mode 100644 index 000000000..1d7fb64c4 --- /dev/null +++ b/payntbind/src/synthesis/translation/choiceTransformation.h @@ -0,0 +1,90 @@ +#pragma once + +#include +#include +#include +#include +#include + +#include + +namespace synthesis { + +// label used for choices that do not have an explicit one +const std::string NO_ACTION_LABEL = "__no_label__"; + +/** + * Add \p NO_ACTION_LABEL label to any choice that does not have any. + */ +template +void addMissingChoiceLabelsLabeling( + storm::models::sparse::Model const& model, + storm::models::sparse::ChoiceLabeling& choice_labeling +); + +/** + * Add \p NO_ACTION_LABEL label to any choice that does not have any. + * @return an updated model or NULL if no change took place + */ +template +std::shared_ptr> addMissingChoiceLabelsModel( + storm::models::sparse::Model const& model +); + +/** + * Assert that choice labeling is canonic, i.e. each choice has exactly one label. + */ +void assertChoiceLabelingIsCanonic(storm::models::sparse::ChoiceLabeling const& choice_labeling); + +/** + * Remove labels that have zero associated choices. + */ +void removeUnusedLabels(storm::models::sparse::ChoiceLabeling & choice_labeling); + +/** + * Given a model with canonic choice labeling, return a list of action labels and a choice-to-action mapping. + */ +template +std::pair,std::vector> extractActionLabels( + storm::models::sparse::Model const& model +); + +template +std::pair>,std::vector> enableAllActions( + storm::models::sparse::Model const& model +); + +/** + * Given a model with canonic choice labeling, make sure that in each state in the set \p state_maks all actions + * are available. If an action is not available in a state, add it to this state with the behavior of the first + * existing action. + * @return the updated model and a choice-to-action mapping + */ +template +std::pair>,std::vector> enableAllActions( + storm::models::sparse::Model const& model, + storm::storage::BitVector const& state_mask +); + +/** + * Given a model with canonic choice labeling, remove an action from the given set \p state_mask of states. + * @return an updated model or NULL if no change took place + */ +template +std::shared_ptr> removeAction( + storm::models::sparse::Model const& model, + std::string const& action_to_remove_label, + storm::storage::BitVector const& state_mask +); + +/** + * For any absorbing state with an unlabeled action, explicitly add all available actions and subsequently remove + * these unlabeled actions. + * @return an updated model or NULL if no change took place + */ +template +std::shared_ptr> restoreActionsInAbsorbingStates( + storm::models::sparse::Model const& model +); + +} diff --git a/payntbind/src/synthesis/translation/componentTranslations.cpp b/payntbind/src/synthesis/translation/componentTranslations.cpp index 27a6cab43..92bd03a11 100644 --- a/payntbind/src/synthesis/translation/componentTranslations.cpp +++ b/payntbind/src/synthesis/translation/componentTranslations.cpp @@ -1,218 +1,205 @@ #include "componentTranslations.h" +#include +#include #include #include namespace synthesis { - template - std::pair,std::vector> extractActionLabels( - storm::models::sparse::Model const& model - ) { - // collect action labels - STORM_LOG_THROW(model.hasChoiceLabeling(), storm::exceptions::InvalidModelException, - "model does not have the choice labeling"); - storm::models::sparse::ChoiceLabeling const& choice_labeling = model.getChoiceLabeling(); - std::vector action_labels; - std::map action_label_index; - std::set action_labels_set; - for(uint64_t choice = 0; choice < model.getNumberOfChoices(); ++choice) { - for(std::string const& label: choice_labeling.getLabelsOfChoice(choice)) { - action_labels_set.insert(label); - } - } - for(std::string const& label: action_labels_set) { - action_label_index[label] = action_labels.size(); - action_labels.push_back(label); - } - auto num_choices = model.getNumberOfChoices(); - - // assert that each choice has exactly one label - std::vector choice_to_action(num_choices); - for(uint64_t choice = 0; choice < model.getNumberOfChoices(); ++choice) { - auto const& labels = choice_labeling.getLabelsOfChoice(choice); - STORM_LOG_THROW(labels.size()==1, storm::exceptions::InvalidModelException, - "expected exactly 1 label for choice " << choice); - std::string const& label = *(labels.begin()); - uint64_t action = action_label_index[label]; - choice_to_action[choice] = action; - } - return std::make_pair(action_labels,choice_to_action); +template +storm::storage::sparse::ModelComponents componentsFromModel( + storm::models::sparse::Model const& model +) { + storm::storage::sparse::ModelComponents components; + components.stateLabeling = model.getStateLabeling(); + components.stateValuations = model.getOptionalStateValuations(); + components.transitionMatrix = model.getTransitionMatrix(); + components.choiceLabeling = model.getOptionalChoiceLabeling(); + components.choiceOrigins = model.getOptionalChoiceOrigins(); + components.rewardModels = model.getRewardModels(); + if (model.getType() == storm::models::ModelType::Pomdp) { + auto pomdp = static_cast const&>(model); + components.observabilityClasses = pomdp.getObservations(); + components.observationValuations = pomdp.getOptionalObservationValuations(); } + return components; +} - - template - storm::models::sparse::StateLabeling translateStateLabeling( - storm::models::sparse::Model const& model, - std::vector const& translated_to_original_state, - uint64_t translated_initial_state - ) { - auto translated_num_states = translated_to_original_state.size(); - storm::models::sparse::StateLabeling translated_labeling(translated_num_states); - for (auto const& label : model.getStateLabeling().getLabels()) { - translated_labeling.addLabel(label, storm::storage::BitVector(translated_num_states,false)); +template +storm::models::sparse::StateLabeling translateStateLabeling( + storm::models::sparse::Model const& model, + std::vector const& translated_to_original_state, + uint64_t translated_initial_state +) { + auto translated_num_states = translated_to_original_state.size(); + storm::models::sparse::StateLabeling translated_labeling(translated_num_states); + for (auto const& label : model.getStateLabeling().getLabels()) { + translated_labeling.addLabel(label, storm::storage::BitVector(translated_num_states,false)); + } + for(uint64_t translated_state=0; translated_state= model.getNumberOfStates()) { + continue; } - for(uint64_t translated_state=0; translated_state= model.getNumberOfStates()) { + for (auto const& label : model.getStateLabeling().getLabelsOfState(state)) { + if(label=="init") { continue; } - for (auto const& label : model.getStateLabeling().getLabelsOfState(state)) { - if(label=="init") { - continue; - } - translated_labeling.addLabelToState(label,translated_state); - } + translated_labeling.addLabelToState(label,translated_state); } - translated_labeling.addLabelToState("init",translated_initial_state); - return translated_labeling; } + translated_labeling.addLabelToState("init",translated_initial_state); + return translated_labeling; +} - template - std::vector translateObservabilityClasses( - storm::models::sparse::Pomdp const& model, - std::vector const& translated_to_original_state - ) { - uint64_t translated_num_states = translated_to_original_state.size(); - std::vector observation_classes(translated_num_states); - for(uint64_t translated_state=0; translated_state= model.getNumberOfStates()) { - continue; - } - observation_classes[translated_state] = model.getObservation(state); +template +std::vector translateObservabilityClasses( + storm::models::sparse::Model const& model, + std::vector const& translated_to_original_state +) { + STORM_LOG_THROW(model.getType() == storm::models::ModelType::Pomdp, storm::exceptions::InvalidModelException, "the model is not a POMDP"); + auto pomdp = static_cast const&>(model); + uint64_t translated_num_states = translated_to_original_state.size(); + std::vector observation_classes(translated_num_states); + for(uint64_t translated_state=0; translated_state= pomdp.getNumberOfStates()) { + continue; } - return observation_classes; + observation_classes[translated_state] = pomdp.getObservation(state); } + return observation_classes; +} - template - storm::models::sparse::ChoiceLabeling translateChoiceLabeling( - storm::models::sparse::Model const& model, - std::vector const& translated_to_original_choice, - storm::storage::BitVector const& translated_choice_mask - ) { - uint64_t translated_num_choices = translated_to_original_choice.size(); - storm::models::sparse::ChoiceLabeling translated_labeling(translated_num_choices); - for(uint64_t translated_choice: translated_choice_mask) { - uint64_t choice = translated_to_original_choice[translated_choice]; - if(choice >= model.getNumberOfChoices()) { - continue; - } - for (std::string const& label : model.getChoiceLabeling().getLabelsOfChoice(choice)) { - if(not translated_labeling.containsLabel(label)) { - translated_labeling.addLabel(label); - } - translated_labeling.addLabelToChoice(label,translated_choice); +template +storm::models::sparse::ChoiceLabeling translateChoiceLabeling( + storm::models::sparse::Model const& model, + std::vector const& translated_to_original_choice, + storm::storage::BitVector const& translated_choice_mask +) { + uint64_t translated_num_choices = translated_to_original_choice.size(); + storm::models::sparse::ChoiceLabeling translated_labeling(translated_num_choices); + for(uint64_t translated_choice: translated_choice_mask) { + uint64_t choice = translated_to_original_choice[translated_choice]; + if(choice >= model.getNumberOfChoices()) { + continue; + } + for (std::string const& label : model.getChoiceLabeling().getLabelsOfChoice(choice)) { + if(not translated_labeling.containsLabel(label)) { + translated_labeling.addLabel(label); } + translated_labeling.addLabelToChoice(label,translated_choice); } - return translated_labeling; } + return translated_labeling; +} - template - storm::models::sparse::StandardRewardModel translateRewardModel( - storm::models::sparse::StandardRewardModel const& reward_model, - std::vector const& translated_to_original_choice, - storm::storage::BitVector const& translated_choice_mask - ) { - std::optional> state_rewards; - STORM_LOG_THROW(!reward_model.hasStateRewards(), storm::exceptions::NotSupportedException, - "state rewards are currently not supported."); - STORM_LOG_THROW(!reward_model.hasTransitionRewards(), storm::exceptions::NotSupportedException, - "transition rewards are currently not supported."); - - uint64_t num_choices = reward_model.getStateActionRewardVector().size(); - std::vector action_rewards(translated_to_original_choice.size()); - for(uint64_t translated_choice: translated_choice_mask) { - uint64_t choice = translated_to_original_choice[translated_choice]; - if(choice >= num_choices) { - continue; - } - action_rewards[translated_choice] = reward_model.getStateActionReward(choice); +template +storm::models::sparse::StandardRewardModel translateRewardModel( + storm::models::sparse::StandardRewardModel const& reward_model, + std::vector const& translated_to_original_choice, + storm::storage::BitVector const& translated_choice_mask +) { + std::optional> state_rewards; + STORM_LOG_THROW(!reward_model.hasStateRewards(), storm::exceptions::NotSupportedException, + "state rewards are currently not supported."); + STORM_LOG_THROW(!reward_model.hasTransitionRewards(), storm::exceptions::NotSupportedException, + "transition rewards are currently not supported."); + + uint64_t num_choices = reward_model.getStateActionRewardVector().size(); + std::vector action_rewards(translated_to_original_choice.size()); + for(uint64_t translated_choice: translated_choice_mask) { + uint64_t choice = translated_to_original_choice[translated_choice]; + if(choice >= num_choices) { + continue; } - return storm::models::sparse::StandardRewardModel(std::move(state_rewards), std::move(action_rewards)); + action_rewards[translated_choice] = reward_model.getStateActionReward(choice); } - template - std::unordered_map> translateRewardModels( - storm::models::sparse::Model const& model, - std::vector const& translated_to_original_choice, - storm::storage::BitVector const& translated_choice_mask - ) { - std::unordered_map> reward_models; - for(auto const& reward_model : model.getRewardModels()) { - auto new_reward_model = translateRewardModel(reward_model.second,translated_to_original_choice,translated_choice_mask); - reward_models.emplace(reward_model.first, new_reward_model); - } - return reward_models; + return storm::models::sparse::StandardRewardModel(std::move(state_rewards), std::move(action_rewards)); +} +template +std::unordered_map> translateRewardModels( + storm::models::sparse::Model const& model, + std::vector const& translated_to_original_choice, + storm::storage::BitVector const& translated_choice_mask +) { + std::unordered_map> reward_models; + for(auto const& reward_model : model.getRewardModels()) { + auto new_reward_model = translateRewardModel(reward_model.second,translated_to_original_choice,translated_choice_mask); + reward_models.emplace(reward_model.first, new_reward_model); } + return reward_models; +} - template - void translateTransitionMatrixRow( - storm::models::sparse::Model const& model, - storm::storage::SparseMatrixBuilder & builder, - std::vector const& original_to_translated_state, - std::vector const& original_to_translated_choice, - uint64_t choice - ) { - uint64_t translated_choice = original_to_translated_choice[choice]; - for(auto entry: model.getTransitionMatrix().getRow(choice)) { - uint64_t translated_dst = original_to_translated_state[entry.getColumn()]; - builder.addNextValue(translated_choice, translated_dst, entry.getValue()); - } +template +void translateTransitionMatrixRow( + storm::models::sparse::Model const& model, + storm::storage::SparseMatrixBuilder & builder, + std::vector const& original_to_translated_state, + std::vector const& original_to_translated_choice, + uint64_t choice +) { + uint64_t translated_choice = original_to_translated_choice[choice]; + for(auto entry: model.getTransitionMatrix().getRow(choice)) { + uint64_t translated_dst = original_to_translated_state[entry.getColumn()]; + builder.addNextValue(translated_choice, translated_dst, entry.getValue()); } +} - template - void translateTransitionMatrixRowGroup( - storm::models::sparse::Model const& model, - storm::storage::SparseMatrixBuilder & builder, - std::vector const& original_to_translated_state, - std::vector const& original_to_translated_choice, - uint64_t state - ) { - for(uint64_t const& choice: model.getTransitionMatrix().getRowGroupIndices(state)) { - synthesis::translateTransitionMatrixRow( - model, builder, original_to_translated_state, original_to_translated_choice, choice - ); - } +template +void translateTransitionMatrixRowGroup( + storm::models::sparse::Model const& model, + storm::storage::SparseMatrixBuilder & builder, + std::vector const& original_to_translated_state, + std::vector const& original_to_translated_choice, + uint64_t state +) { + for(uint64_t const& choice: model.getTransitionMatrix().getRowGroupIndices(state)) { + synthesis::translateTransitionMatrixRow( + model, builder, original_to_translated_state, original_to_translated_choice, choice + ); } +} - template std::pair,std::vector> extractActionLabels( - storm::models::sparse::Model const& model); +template storm::storage::sparse::ModelComponents componentsFromModel( + storm::models::sparse::Model const& model); + +template storm::models::sparse::StateLabeling translateStateLabeling( + storm::models::sparse::Model const& model, + std::vector const& translated_to_original_state, + uint64_t translated_initial_state); + +template void translateTransitionMatrixRow( + storm::models::sparse::Model const& model, + storm::storage::SparseMatrixBuilder & builder, + std::vector const& original_to_translated_state, + std::vector const& original_to_translated_choice, + uint64_t choice); +template void translateTransitionMatrixRowGroup( + storm::models::sparse::Model const& model, + storm::storage::SparseMatrixBuilder & builder, + std::vector const& original_to_translated_state, + std::vector const& original_to_translated_choice, + uint64_t state); + +template storm::models::sparse::ChoiceLabeling translateChoiceLabeling( + storm::models::sparse::Model const& model, + std::vector const& translated_to_original_choice, + storm::storage::BitVector const& translated_choice_mask); +template storm::models::sparse::StandardRewardModel translateRewardModel( + storm::models::sparse::StandardRewardModel const& reward_model, + std::vector const& translated_to_original_choice, + storm::storage::BitVector const& translated_choice_mask); +template std::unordered_map> translateRewardModels( + storm::models::sparse::Model const& model, + std::vector const& translated_to_original_choice, + storm::storage::BitVector const& translated_choice_mask); + +template std::vector translateObservabilityClasses( + storm::models::sparse::Model const& model, + std::vector const& translated_to_original_state); - template storm::models::sparse::StateLabeling translateStateLabeling( - storm::models::sparse::Model const& model, - std::vector const& translated_to_original_state, - uint64_t translated_initial_state); - - template void translateTransitionMatrixRow( - storm::models::sparse::Model const& model, - storm::storage::SparseMatrixBuilder & builder, - std::vector const& original_to_translated_state, - std::vector const& original_to_translated_choice, - uint64_t choice); - template void translateTransitionMatrixRowGroup( - storm::models::sparse::Model const& model, - storm::storage::SparseMatrixBuilder & builder, - std::vector const& original_to_translated_state, - std::vector const& original_to_translated_choice, - uint64_t state); - - template storm::models::sparse::ChoiceLabeling translateChoiceLabeling( - storm::models::sparse::Model const& model, - std::vector const& translated_to_original_choice, - storm::storage::BitVector const& translated_choice_mask); - template storm::models::sparse::StandardRewardModel translateRewardModel( - storm::models::sparse::StandardRewardModel const& reward_model, - std::vector const& translated_to_original_choice, - storm::storage::BitVector const& translated_choice_mask); - template std::unordered_map> translateRewardModels( - storm::models::sparse::Model const& model, - std::vector const& translated_to_original_choice, - storm::storage::BitVector const& translated_choice_mask); - - template std::vector translateObservabilityClasses( - storm::models::sparse::Pomdp const& model, - std::vector const& translated_to_original_state); - } diff --git a/payntbind/src/synthesis/translation/componentTranslations.h b/payntbind/src/synthesis/translation/componentTranslations.h index 0badb9b93..871aeb4a0 100644 --- a/payntbind/src/synthesis/translation/componentTranslations.h +++ b/payntbind/src/synthesis/translation/componentTranslations.h @@ -1,8 +1,8 @@ #pragma once #include +#include #include -#include #include #include #include @@ -11,64 +11,62 @@ namespace synthesis { - /** - * Given a (nondeterministic) model with canonic choice labeling (exactly 1 label per choice), return a list of action - * labels and a choice-to-action mapping. - */ - template - std::pair,std::vector> extractActionLabels( - storm::models::sparse::Model const& model - ); +/** + * Copy components from existing model. + */ +template +storm::storage::sparse::ModelComponents componentsFromModel( + storm::models::sparse::Model const& model +); +template +storm::models::sparse::StateLabeling translateStateLabeling( + storm::models::sparse::Model const& model, + std::vector const& translated_to_original_state, + uint64_t translated_initial_state +); - template - storm::models::sparse::StateLabeling translateStateLabeling( - storm::models::sparse::Model const& model, - std::vector const& translated_to_original_state, - uint64_t translated_initial_state - ); +template +std::vector translateObservabilityClasses( + storm::models::sparse::Model const& model, + std::vector const& translated_to_original_state +); - template - std::vector translateObservabilityClasses( - storm::models::sparse::Pomdp const& model, - std::vector const& translated_to_original_state - ); - - template - storm::models::sparse::ChoiceLabeling translateChoiceLabeling( - storm::models::sparse::Model const& model, - std::vector const& translated_to_original_choice, - storm::storage::BitVector const& translated_choice_mask - ); - - template - storm::models::sparse::StandardRewardModel translateRewardModel( - storm::models::sparse::StandardRewardModel const& reward_model, - std::vector const& translated_to_original_choice, - storm::storage::BitVector const& translated_choice_mask - ); - template - std::unordered_map> translateRewardModels( - storm::models::sparse::Model const& model, - std::vector const& translated_to_original_choice, - storm::storage::BitVector const& translated_choice_mask - ); +template +storm::models::sparse::ChoiceLabeling translateChoiceLabeling( + storm::models::sparse::Model const& model, + std::vector const& translated_to_original_choice, + storm::storage::BitVector const& translated_choice_mask +); - template - void translateTransitionMatrixRow( - storm::models::sparse::Model const& model, - storm::storage::SparseMatrixBuilder & builder, - std::vector const& original_to_translated_state, - std::vector const& original_to_translated_choice, - uint64_t choice - ); - template - void translateTransitionMatrixRowGroup( - storm::models::sparse::Model const& model, - storm::storage::SparseMatrixBuilder & builder, - std::vector const& original_to_translated_state, - std::vector const& original_to_translated_choice, - uint64_t state - ); +template +storm::models::sparse::StandardRewardModel translateRewardModel( + storm::models::sparse::StandardRewardModel const& reward_model, + std::vector const& translated_to_original_choice, + storm::storage::BitVector const& translated_choice_mask +); +template +std::unordered_map> translateRewardModels( + storm::models::sparse::Model const& model, + std::vector const& translated_to_original_choice, + storm::storage::BitVector const& translated_choice_mask +); + +template +void translateTransitionMatrixRow( + storm::models::sparse::Model const& model, + storm::storage::SparseMatrixBuilder & builder, + std::vector const& original_to_translated_state, + std::vector const& original_to_translated_choice, + uint64_t choice +); +template +void translateTransitionMatrixRowGroup( + storm::models::sparse::Model const& model, + storm::storage::SparseMatrixBuilder & builder, + std::vector const& original_to_translated_state, + std::vector const& original_to_translated_choice, + uint64_t state +); }