diff --git a/paynt/cli.py b/paynt/cli.py
index 21948614..f4323410 100644
--- a/paynt/cli.py
+++ b/paynt/cli.py
@@ -114,14 +114,8 @@ def setup_logger(log_path = None):
 @click.option("--export-synthesis", type=click.Path(), default=None,
     help="base filename to output synthesis result")
 
-@click.option("--mdp-split-wrt-mdp", is_flag=True, default=False,
-    help="if set, MDP abstraction scheduler will be used for splitting, otherwise game abstraction scheduler will be used")
 @click.option("--mdp-discard-unreachable-choices", is_flag=True, default=False,
     help="if set, unreachable choices will be discarded from the splitting scheduler")
-@click.option("--mdp-use-randomized-abstraction", is_flag=True, default=False,
-    help="if set, randomized abstraction guess-and-verify will be used instead of game abstraction;" +
-    " MDP abstraction scheduler will be used for splitting"
-)
 
 @click.option("--tree-depth", default=0, type=int,
     help="decision tree synthesis: tree depth")
@@ -152,7 +146,7 @@ def paynt_run(
     storm_pomdp, iterative_storm, get_storm_result, storm_options, prune_storm,
     use_storm_cutoffs, unfold_strategy_storm,
     export_fsc_storm, export_fsc_paynt, export_synthesis,
-    mdp_split_wrt_mdp, mdp_discard_unreachable_choices, mdp_use_randomized_abstraction,
+    mdp_discard_unreachable_choices,
     tree_depth, tree_enumeration, tree_map_scheduler, add_dont_care_action,
     constraint_bound,
     ce_generator,
@@ -176,9 +170,7 @@ def paynt_run(
     paynt.quotient.decpomdp.DecPomdpQuotient.initial_memory_size = fsc_memory_size
     paynt.quotient.posmg.PosmgQuotient.initial_memory_size = fsc_memory_size
 
-    paynt.synthesizer.policy_tree.SynthesizerPolicyTree.split_wrt_mdp_scheduler = mdp_split_wrt_mdp
     paynt.synthesizer.policy_tree.SynthesizerPolicyTree.discard_unreachable_choices = mdp_discard_unreachable_choices
-    paynt.synthesizer.policy_tree.SynthesizerPolicyTree.use_randomized_abstraction = mdp_use_randomized_abstraction
 
     paynt.synthesizer.decision_tree.SynthesizerDecisionTree.tree_depth = tree_depth
     paynt.synthesizer.decision_tree.SynthesizerDecisionTree.tree_enumeration = tree_enumeration
diff --git a/paynt/parser/drn_parser.py b/paynt/parser/drn_parser.py
index 4f42a4f9..360de3bf 100644
--- a/paynt/parser/drn_parser.py
+++ b/paynt/parser/drn_parser.py
@@ -27,7 +27,7 @@ def parse_drn(cls, sketch_path):
                 pomdp_path = sketch_path + '.tmp'
                 state_player_indications = DrnParser.pomdp_from_posmg(sketch_path, pomdp_path)
                 pomdp = DrnParser.read_drn(pomdp_path)
-                explicit_model = payntbind.synthesis.create_posmg(pomdp, state_player_indications)
+                explicit_model = payntbind.synthesis.posmg_from_pomdp(pomdp, state_player_indications)
                 os.remove(pomdp_path)
             else:
                 explicit_model = DrnParser.read_drn(sketch_path)
diff --git a/paynt/quotient/mdp_family.py b/paynt/quotient/mdp_family.py
index 49792104..504c14fe 100644
--- a/paynt/quotient/mdp_family.py
+++ b/paynt/quotient/mdp_family.py
@@ -186,7 +186,7 @@ def build_game_abstraction_solver(self, prop):
         target_label = prop.get_target_label()
         precision = paynt.verification.property.Property.model_checking_precision
         solver = payntbind.synthesis.GameAbstractionSolver(
-            self.quotient_mdp, len(self.action_labels), self.choice_to_action, target_label, precision
+            self.quotient_mdp, len(self.action_labels), self.choice_to_action, prop.formula, prop.maximizing, target_label, precision
         )
         return solver
 
diff --git a/paynt/synthesizer/policy_tree.py b/paynt/synthesizer/policy_tree.py
index a249a2fe..e02ec5cb 100644
--- a/paynt/synthesizer/policy_tree.py
+++ b/paynt/synthesizer/policy_tree.py
@@ -483,12 +483,8 @@ class SynthesizerPolicyTree(paynt.synthesizer.synthesizer.Synthesizer):
 
     # if True, tree leaves will be double-checked after synthesis
     double_check_policy_tree_leaves = False
-    # if True, MDP abstraction scheduler will be used for splitting, otherwise game abstraction scheduler will be used
-    split_wrt_mdp_scheduler = False
     # if True, unreachable choices will be discarded from the splitting scheduler
     discard_unreachable_choices = False
-    # if True, randomized abstraction guess-and-verify will be used instead of game abstraction
-    use_randomized_abstraction = False
     
     @property
     def method_name(self):
@@ -532,9 +528,12 @@ def solve_singleton(self, family, prop):
     def solve_game_abstraction(self, family, prop, game_solver):
         # construct and solve the game abstraction
         # logger.debug("solving game abstraction...")
-        game_solver.solve(family.selected_choices, prop.maximizing, prop.minimizing)
-        self.stat.iteration_game(family.mdp.states)
+
+        # game_solver.solve_sg(family.selected_choices)
+        game_solver.solve_smg(family.selected_choices)
+
         game_value = game_solver.solution_value
+        self.stat.iteration_game(family.mdp.states)
         game_sat = prop.satisfies_threshold_within_precision(game_value)
         # logger.debug("game solved, value is {}".format(game_value))
         game_policy = game_solver.solution_state_to_player1_action
@@ -546,35 +545,6 @@ def solve_game_abstraction(self, family, prop, game_solver):
         game_policy = game_policy_fixed
         return game_policy,game_sat
 
-    def try_randomized_abstraction(self, family, prop):
-        # build randomized abstraction
-        choice_to_action = []
-        for choice in range(family.mdp.model.nr_choices):
-            action = self.quotient.choice_to_action[family.mdp.quotient_choice_map[choice]]
-            choice_to_action.append(action)
-        state_action_choices = self.quotient.map_state_action_to_choices(family.mdp.model,self.quotient.num_actions,choice_to_action)
-        model,choice_to_action = payntbind.synthesis.randomize_action_variant(family.mdp.model, state_action_choices)
-
-        # model check
-        result = Property.model_check(model, prop.formula)
-        self.stat.iteration(model)
-        value = result.at(model.initial_states[0])
-        policy_sat = prop.satisfies_threshold(value) # does this value matter?
-
-        # extract policy for the quotient
-        scheduler = result.scheduler
-        policy = self.quotient.empty_policy()
-        for state in range(model.nr_states):
-            state_choice = scheduler.get_choice(state).get_deterministic_choice()
-            choice = model.transition_matrix.get_row_group_start(state) + state_choice
-            action = choice_to_action[choice]
-            quotient_state = family.mdp.quotient_state_map[state]
-            policy[quotient_state] = action
-
-        # apply policy and check if it is SAT for all MDPs in the family
-        policy_sat = self.verify_policy(family, prop, policy)
-        return policy,policy_sat
-
     def state_to_choice_to_hole_selection(self, state_to_choice):
         if SynthesizerPolicyTree.discard_unreachable_choices:
             state_to_choice = self.quotient.discard_unreachable_choices(state_to_choice)
@@ -588,18 +558,6 @@ def parse_game_scheduler(self, game_solver):
         state_values = game_solver.solution_state_values
         return scheduler_choices,hole_selection,state_values
 
-    def parse_mdp_scheduler(self, family, mdp_result):
-        state_to_choice = self.quotient.scheduler_to_state_to_choice(
-            family.mdp, mdp_result.result.scheduler, discard_unreachable_choices=False
-        )
-        scheduler_choices,hole_selection = self.state_to_choice_to_hole_selection(state_to_choice)
-        state_values = [0] * self.quotient.quotient_mdp.nr_states
-        for state in range(family.mdp.states):
-            quotient_state = family.mdp.quotient_state_map[state]
-            state_values[quotient_state] = mdp_result.result.at(state)
-        return scheduler_choices,hole_selection,state_values
-
-    
     def verify_family(self, family, game_solver, prop):
         # logger.info("investigating family of size {}".format(family.size))
         self.quotient.build(family)
@@ -609,18 +567,10 @@ def verify_family(self, family, game_solver, prop):
             mdp_family_result.policy = self.solve_singleton(family,prop)
             return mdp_family_result
         
-        if not SynthesizerPolicyTree.use_randomized_abstraction:
-            if family.candidate_policy is None:
-                game_policy,game_sat = self.solve_game_abstraction(family,prop,game_solver)
-            else:
-                game_policy = family.candidate_policy
-                game_sat = False
+        if family.candidate_policy is None:
+            game_policy,game_sat = self.solve_game_abstraction(family,prop,game_solver)
         else:
-            randomization_policy,policy_sat = self.try_randomized_abstraction(family,prop)
-            if policy_sat:
-                mdp_family_result.policy = randomization_policy
-                return mdp_family_result
-            game_policy = None
+            game_policy = family.candidate_policy
             game_sat = False
 
         mdp_family_result.game_policy = game_policy
@@ -638,10 +588,7 @@ def verify_family(self, family, game_solver, prop):
             return mdp_family_result
 
         # undecided: choose scheduler choices to be used for splitting
-        if not (SynthesizerPolicyTree.use_randomized_abstraction or SynthesizerPolicyTree.split_wrt_mdp_scheduler):
-            scheduler_choices,hole_selection,state_values = self.parse_game_scheduler(game_solver)
-        else:
-            scheduler_choices,hole_selection,state_values = self.parse_mdp_scheduler(family, mdp_result)
+        scheduler_choices,hole_selection,state_values = self.parse_game_scheduler(game_solver)
 
         splitter = self.choose_splitter(family,prop,scheduler_choices,state_values,hole_selection)
         mdp_family_result.splitter = splitter
@@ -723,7 +670,7 @@ def split(self, family, prop, hole_selection, splitter, policy):
             subfamily.candidate_policy = None
             subfamilies.append(subfamily)
 
-        if not (SynthesizerPolicyTree.use_randomized_abstraction or SynthesizerPolicyTree.split_wrt_mdp_scheduler) and not SynthesizerPolicyTree.discard_unreachable_choices:
+        if not SynthesizerPolicyTree.discard_unreachable_choices:
             self.assign_candidate_policy(subfamilies, hole_selection, splitter, policy)
 
         return suboptions,subfamilies
diff --git a/payntbind/src/synthesis/pomdp_family/GameAbstractionSolver.cpp b/payntbind/src/synthesis/pomdp_family/GameAbstractionSolver.cpp
index 2b23f83e..2c62e470 100644
--- a/payntbind/src/synthesis/pomdp_family/GameAbstractionSolver.cpp
+++ b/payntbind/src/synthesis/pomdp_family/GameAbstractionSolver.cpp
@@ -1,108 +1,33 @@
 #include "GameAbstractionSolver.h"
 
-
+#include "src/synthesis/pomdp_family/SmgAbstraction.h"
+#include "src/synthesis/smg/smgModelChecker.h"
+#include "src/synthesis/translation/componentTranslations.h"
+#include "src/synthesis/translation/ItemKeyTranslator.h"
+#include "src/synthesis/translation/ItemTranslator.h"
+
+#include <storm/environment/solver/GameSolverEnvironment.h>
+#include <storm/environment/solver/NativeSolverEnvironment.h>
+#include <storm/models/sparse/Smg.h>
+#include <storm/solver/GameSolver.h>
+#include <storm/storage/PlayerIndex.h>
+#include <storm/utility/builder.h>
 
 #include <queue>
 
 namespace synthesis {
-        
-    /*template<typename ValueType>
-    std::pair<std::shared_ptr<storm::models::sparse::Mdp<ValueType>>,std::vector<uint64_t>> randomizeActionVariant(
-        storm::models::sparse::Model<ValueType> const& model,
-        std::vector<std::vector<std::vector<uint64_t>>> const& state_action_choices
-    ) {
-        storm::storage::sparse::ModelComponents<ValueType> components;
-
-        // copy state labeling
-        storm::models::sparse::StateLabeling state_labeling(model.getNumberOfStates());
-        for (auto const& label : model.getStateLabeling().getLabels()) {
-            state_labeling.addLabel(label, storm::storage::BitVector(model.getStates(label)));
-        }
-        components.stateLabeling = state_labeling;
-        
-        // build transition matrix and reward models
-        storm::storage::SparseMatrixBuilder<ValueType> builder(0, 0, 0, false, true, 0);
-        std::map<std::string,std::vector<ValueType>> reward_vectors;
-        for(auto const& reward_model : model.getRewardModels()) {
-            reward_vectors.emplace(reward_model.first, std::vector<ValueType>());
-        }
-
-        uint64_t num_rows = 0;
-        std::vector<uint64_t> choice_to_action;
-        auto num_actions = state_action_choices[0].size();
-        for(uint64_t state=0; state<model.getNumberOfStates(); ++state) {
-            builder.newRowGroup(num_rows);
-            for(uint64_t action = 0; action<num_actions; ++action) {
-                auto & choices = state_action_choices[state][action];
-                if(choices.empty()) {
-                    continue;
-                }
-
-                // new choice
-                choice_to_action.push_back(action);
-
-                // handle transition matrix
-                auto num_choices = choices.size();
-                std::map<uint64_t,ValueType> dst_prob;
-                for(auto choice: choices) {
-                    for(auto const &entry: model.getTransitionMatrix().getRow(choice)) {
-                        dst_prob[entry.getColumn()] += entry.getValue() / num_choices;
-                    }
-                }
-                for(auto const& [dst,prob] : dst_prob) {
-                    builder.addNextValue(num_rows,dst,prob);
-                }
-                num_rows++;
-
-                // handle reward models
-                for(auto const& reward_model : model.getRewardModels()) {
-                    ValueType reward_value = 0;
-                    for(auto choice: choices) {
-                        reward_value += reward_model.second.getStateActionReward(choice) / num_choices;
-                    }
-                    reward_vectors[reward_model.first].push_back(reward_value);
-                }
-            }
-        }
-        components.transitionMatrix = builder.build();
-
-        for(auto const& [name,choice_rewards]: reward_vectors) {
-            std::optional<std::vector<ValueType>> state_rewards;
-            components.rewardModels.emplace(name, storm::models::sparse::StandardRewardModel<ValueType>(std::move(state_rewards), std::move(choice_rewards)));
-        }
-
-        auto randomized_model = std::make_shared<storm::models::sparse::Mdp<ValueType>>(std::move(components));
-        return std::make_pair(randomized_model,choice_to_action);
-    }
-    template std::pair<std::shared_ptr<storm::models::sparse::Mdp<double>>,std::vector<uint64_t>> randomizeActionVariant(storm::models::sparse::Model<double> const& model, std::vector<std::vector<std::vector<uint64_t>>> const& state_action_choices);*/
-
-
-    template<typename ValueType>
-    void print_matrix(storm::storage::SparseMatrix<ValueType> matrix) {
-        auto const& row_group_indices = matrix.getRowGroupIndices();
-        for(uint64_t state=0; state < matrix.getRowGroupCount(); state++) {
-            std::cout << "state " << state << ": " << std::endl;
-            for(uint64_t row=row_group_indices[state]; row<row_group_indices[state+1]; row++) {
-                for(auto const &entry: matrix.getRow(row)) {
-                    std::cout << state << "-> "  << entry.getColumn() << " ["  << entry.getValue() << "];";
-                }
-                std::cout << std::endl;
-            }
-        }
-        std::cout << "-----" << std::endl;
-    }
-
-    template void print_matrix<storm::storage::sparse::state_type>(storm::storage::SparseMatrix<storm::storage::sparse::state_type> matrix);
-    template void print_matrix<double>(storm::storage::SparseMatrix<double> matrix);
 
     template<typename ValueType>
     GameAbstractionSolver<ValueType>::GameAbstractionSolver(
         storm::models::sparse::Model<ValueType> const& quotient,
         uint64_t quotient_num_actions,
         std::vector<uint64_t> const& choice_to_action,
+        std::shared_ptr<storm::logic::Formula const> formula,
+        bool player1_maximizing,
         std::string const& target_label,
         double precision
-    ) : quotient(quotient), quotient_num_actions(quotient_num_actions), choice_to_action(choice_to_action) {
+    ) : quotient(quotient), quotient_num_actions(quotient_num_actions), choice_to_action(choice_to_action),
+        player1_maximizing(player1_maximizing) {
 
         auto quotient_num_states = quotient.getNumberOfStates();
         auto quotient_num_choices = quotient.getNumberOfChoices();
@@ -115,6 +40,11 @@ namespace synthesis {
         }
         this->setupSolverEnvironment(precision);
 
+        std::vector<std::variant<std::string, storm::storage::PlayerIndex>> coalition_vector;
+        coalition_vector.emplace_back((storm::storage::PlayerIndex)0);
+        storm::logic::PlayerCoalition coalition(coalition_vector);
+        this->game_formula = std::make_shared<storm::logic::GameFormula const>(coalition,formula);
+
         // identify target states
         this->state_is_target = storm::storage::BitVector(quotient_num_states,false);
         for(auto state: quotient.getStateLabeling().getStates(target_label)) {
@@ -149,17 +79,14 @@ namespace synthesis {
 
 
     template<typename ValueType>
-    void GameAbstractionSolver<ValueType>::solve(
-        storm::storage::BitVector quotient_choice_mask,
-        bool player1_maximizing, bool player2_maximizing
-    ) {
+    void GameAbstractionSolver<ValueType>::solveSg(storm::storage::BitVector const& quotient_choice_mask) {
         if(profiling_enabled) {
             this->timer_total.start();
         }
 
-        auto quotient_num_states = this->quotient.getNumberOfStates();
-        auto quotient_num_choices = this->quotient.getNumberOfChoices();
-        auto quotient_initial_state = *(this->quotient.getInitialStates().begin());
+        uint64_t quotient_num_states = this->quotient.getNumberOfStates();
+        uint64_t quotient_num_choices = this->quotient.getNumberOfChoices();
+        uint64_t quotient_initial_state = *(this->quotient.getInitialStates().begin());
 
         ItemTranslator state_to_player1_state(quotient_num_states);
         ItemKeyTranslator<uint64_t> state_action_to_player2_state(quotient_num_states);
@@ -172,20 +99,20 @@ namespace synthesis {
         state_is_encountered.set(quotient_initial_state,true);
         auto const& quotient_row_group_indices = this->quotient.getTransitionMatrix().getRowGroupIndices();
         while(not unexplored_states.empty()) {
-            auto state = unexplored_states.front();
+            uint64_t state = unexplored_states.front();
             unexplored_states.pop();
-            auto player1_state = state_to_player1_state.translate(state);
+            uint64_t player1_state = state_to_player1_state.translate(state);
             player1_state_to_actions.resize(state_to_player1_state.numTranslations());
-            for(auto choice = quotient_row_group_indices[state]; choice < quotient_row_group_indices[state+1]; choice++) {
+            for(uint64_t choice = quotient_row_group_indices[state]; choice < quotient_row_group_indices[state+1]; choice++) {
                 if(not quotient_choice_mask[choice]) {
                     continue;
                 }
-                auto action = choice_to_action[choice];
+                uint64_t action = choice_to_action[choice];
                 player1_state_to_actions[player1_state].insert(action);
-                auto player2_state = state_action_to_player2_state.translate(state,action);
+                uint64_t player2_state = state_action_to_player2_state.translate(state,action);
                 player2_state_to_choices.resize(state_action_to_player2_state.numTranslations());
                 player2_state_to_choices[player2_state].push_back(choice);
-                for(auto state_dst: this->choice_to_destinations[choice]) {
+                for(uint64_t state_dst: this->choice_to_destinations[choice]) {
                     if(state_is_encountered[state_dst]) {
                         continue;
                     }
@@ -194,12 +121,12 @@ namespace synthesis {
                 }
             }
         }
-        auto player1_num_states = state_to_player1_state.numTranslations();
-        auto player2_num_states = state_action_to_player2_state.numTranslations();
+        uint64_t player1_num_states = state_to_player1_state.numTranslations();
+        uint64_t player2_num_states = state_action_to_player2_state.numTranslations();
         
         // add fresh target states
-        auto player1_target_state = player1_num_states++;
-        auto player2_target_state = player2_num_states++;
+        uint64_t player1_target_state = player1_num_states++;
+        uint64_t player2_target_state = player2_num_states++;
 
         // build the matrix of Player 1
         std::vector<uint64_t> player1_choice_to_action;
@@ -207,10 +134,10 @@ namespace synthesis {
         uint64_t player1_num_rows = 0;
         for(uint64_t player1_state=0; player1_state<player1_num_states-1; player1_state++) {
             player1_matrix_builder.newRowGroup(player1_num_rows);
-            auto state = state_to_player1_state.retrieve(player1_state);
-            for(auto action: player1_state_to_actions[player1_state]) {
+            uint64_t state = state_to_player1_state.retrieve(player1_state);
+            for(uint64_t action: player1_state_to_actions[player1_state]) {
                 player1_choice_to_action.push_back(action);
-                auto player2_state = state_action_to_player2_state.translate(state,action);
+                uint64_t player2_state = state_action_to_player2_state.translate(state,action);
                 player1_matrix_builder.addNextValue(player1_num_rows,player2_state,1);
                 player1_num_rows++;
             }
@@ -263,8 +190,8 @@ namespace synthesis {
         // solve the game
         auto solver = storm::solver::GameSolverFactory<ValueType>().create(env, player1_matrix, player2_matrix);
         solver->setTrackSchedulers(true);
-        auto player1_direction = this->getOptimizationDirection(player1_maximizing);
-        auto player2_direction = this->getOptimizationDirection(player2_maximizing);
+        auto player1_direction = this->getOptimizationDirection(this->player1_maximizing);
+        auto player2_direction = this->getOptimizationDirection(not this->player1_maximizing);
         std::vector<double> player1_state_values(player1_num_states,0);
         if(profiling_enabled) {
             this->timer_game_solving.start();
@@ -311,7 +238,63 @@ namespace synthesis {
         }
 
         this->solution_value = this->solution_state_values[quotient_initial_state];
+    }
+
+    template<typename ValueType>
+    void GameAbstractionSolver<ValueType>::solveSmg(storm::storage::BitVector const& quotient_choice_mask) {
+        if(profiling_enabled) {
+            this->timer_total.start();
+        }
+
+        SmgAbstraction<ValueType> abstraction = synthesis::SmgAbstraction<ValueType>(
+            quotient,quotient_num_actions,choice_to_action,quotient_choice_mask
+        );
+
+        // solve the game
+        if(profiling_enabled) {
+            this->timer_game_solving.start();
+        }
+        std::shared_ptr<storm::modelchecker::CheckResult> result = synthesis::modelCheckSmg(*(abstraction.smg),this->game_formula,false,true,this->env);
+        if(profiling_enabled) {
+            this->timer_game_solving.stop();
+        }
+        storm::modelchecker::ExplicitQuantitativeCheckResult<ValueType> const& result_quan = result->asExplicitQuantitativeCheckResult<ValueType>();
+        storm::storage::Scheduler<ValueType> const& scheduler = result_quan.getScheduler();
+        this->solution_state_values = result_quan.getValueVector();
+
+        std::fill(this->solution_state_to_player1_action.begin(),this->solution_state_to_player1_action.end(),this->quotient_num_actions);
+        std::fill(this->solution_state_to_quotient_choice.begin(),this->solution_state_to_quotient_choice.end(),this->quotient.getNumberOfChoices());
+        std::vector<uint64_t> const& game_row_groups = abstraction.smg->getTransitionMatrix().getRowGroupIndices();
 
+        // get actions selected by Player 0
+        for(uint64_t game_state = 0; game_state < abstraction.smg->getNumberOfStates(); ++game_state) {
+            if(abstraction.smg->getPlayerOfState(game_state) != 0) {
+                continue;
+            }
+            auto [state,_] = abstraction.state_to_quotient_state_action[game_state];
+            uint64_t game_choice = game_row_groups[game_state]+scheduler.getChoice(game_state).getDeterministicChoice();
+            uint64_t player1_action = choice_to_action[abstraction.choice_to_quotient_choice[game_choice]];
+            this->solution_state_to_player1_action[state] = player1_action;
+        }
+        // get action variants selected by Player 1 in corresponding states
+        for(uint64_t game_state = 0; game_state < abstraction.smg->getNumberOfStates(); ++game_state) {
+            if(abstraction.smg->getPlayerOfState(game_state) != 1) {
+                continue;
+            }
+            auto [state,action] = abstraction.state_to_quotient_state_action[game_state];
+            if(action !=  this->solution_state_to_player1_action[state]) {
+                continue;
+            }
+            uint64_t game_choice = game_row_groups[game_state]+scheduler.getChoice(game_state).getDeterministicChoice();
+            this->solution_state_to_quotient_choice[state] = abstraction.choice_to_quotient_choice[game_choice];
+        }
+
+        if(profiling_enabled) {
+            this->timer_total.stop();
+        }
+
+        uint64_t quotient_initial_state = *(this->quotient.getInitialStates().begin());
+        this->solution_value = this->solution_state_values[quotient_initial_state];
     }
 
 
diff --git a/payntbind/src/synthesis/pomdp_family/GameAbstractionSolver.h b/payntbind/src/synthesis/pomdp_family/GameAbstractionSolver.h
index 241f63b6..9b812749 100644
--- a/payntbind/src/synthesis/pomdp_family/GameAbstractionSolver.h
+++ b/payntbind/src/synthesis/pomdp_family/GameAbstractionSolver.h
@@ -1,28 +1,12 @@
 #pragma once
 
 #include <storm/models/sparse/Model.h>
-#include <storm/models/sparse/Mdp.h>
-#include <storm/solver/GameSolver.h>
 #include <storm/environment/Environment.h>
-#include <storm/environment/solver/GameSolverEnvironment.h>
-#include <storm/environment/solver/NativeSolverEnvironment.h>
 #include <storm/utility/Stopwatch.h>
-
-#include "src/synthesis/translation/ItemTranslator.h"
-#include "src/synthesis/translation/ItemKeyTranslator.h"
+#include <storm/logic/GameFormula.h>
 
 namespace synthesis {
 
-
-    /**
-     * Given an MDP having multiple variants of actions, create an MDP in which this variant selection is randomized.
-     */
-    template<typename ValueType>
-    std::pair<std::shared_ptr<storm::models::sparse::Mdp<ValueType>>,std::vector<uint64_t>> randomizeActionVariant(
-        storm::models::sparse::Model<ValueType> const& model,
-        std::vector<std::vector<std::vector<uint64_t>>> const& state_action_choices
-    );
-
     template<typename ValueType>
     class GameAbstractionSolver {
 
@@ -43,6 +27,8 @@ namespace synthesis {
          * @param quotient The quotient MDP. Sub-MDPs from the quotient will be used to construct sub-games.
          * @param quotient_num_action The total number of distinct actions in the quotient.
          * @param choice_to_action For each row of the quotient, the associated action.
+         * @param formula Game formula to model check.
+         * @param player1_maximizing Whether Player 1 maximizes.
          * @param target_label Label of the target states.
          * @param precision Game solving precision.
          */
@@ -50,6 +36,8 @@ namespace synthesis {
             storm::models::sparse::Model<ValueType> const& quotient,
             uint64_t quotient_num_actions,
             std::vector<uint64_t> const& choice_to_action,
+            std::shared_ptr<storm::logic::Formula const> formula,
+            bool player1_maximizing,
             std::string const& target_label,
             double precision
         );
@@ -58,10 +46,8 @@ namespace synthesis {
          * Solve the game induced by the sub-MDP.
          * @param quotient_choice_mask Choices of the quotient that remained in the sub-MDP.
          */
-        void solve(
-            storm::storage::BitVector quotient_choice_mask,
-            bool player1_maximizing, bool player2_maximizing
-        );
+        void solveSg(storm::storage::BitVector const& quotient_choice_mask);
+        void solveSmg(storm::storage::BitVector const& quotient_choice_mask);
 
         /** State values for the solution. */
         std::vector<double> solution_state_values;
@@ -88,6 +74,8 @@ namespace synthesis {
         storm::models::sparse::Model<ValueType> const& quotient;
         uint64_t quotient_num_actions;
         std::vector<uint64_t> choice_to_action;
+        std::shared_ptr<storm::logic::GameFormula const> game_formula;
+        bool player1_maximizing;
         
         /** Identification of target states. */
         storm::storage::BitVector state_is_target;
diff --git a/payntbind/src/synthesis/pomdp_family/ObservationEvaluator.cpp b/payntbind/src/synthesis/pomdp_family/ObservationEvaluator.cpp
index 1fd91e2a..8506aaaf 100644
--- a/payntbind/src/synthesis/pomdp_family/ObservationEvaluator.cpp
+++ b/payntbind/src/synthesis/pomdp_family/ObservationEvaluator.cpp
@@ -12,7 +12,7 @@ namespace synthesis {
         storm::prism::Program & prism,
         storm::models::sparse::Model<ValueType> const& model
     ) {
-        // substitute constanst and simplify formulas in the program
+        // substitute constants and simplify formulas in the program
         prism = prism.substituteConstantsFormulas(true,true);
 
         // identify names and types of observation labels
@@ -79,7 +79,6 @@ namespace synthesis {
         return this->obs_class_to_evaluation[obs_class].getAsInt(OBS_EXPR_VALUE_SIZE*obs_expr,OBS_EXPR_VALUE_SIZE);
     }
 
-    
     template<typename ValueType>
     std::shared_ptr<storm::models::sparse::Pomdp<ValueType>> ObservationEvaluator<ValueType>::addObservationsToSubMdp(
         storm::models::sparse::Mdp<ValueType> const& sub_mdp,
diff --git a/payntbind/src/synthesis/pomdp_family/SmgAbstraction.cpp b/payntbind/src/synthesis/pomdp_family/SmgAbstraction.cpp
new file mode 100644
index 00000000..8a8fc3f7
--- /dev/null
+++ b/payntbind/src/synthesis/pomdp_family/SmgAbstraction.cpp
@@ -0,0 +1,136 @@
+#include "SmgAbstraction.h"
+
+#include "src/synthesis/translation/componentTranslations.h"
+#include "src/synthesis/translation/ItemKeyTranslator.h"
+#include "src/synthesis/posmg/Posmg.h"
+
+#include <storm/storage/PlayerIndex.h>
+#include <storm/utility/builder.h>
+
+#include <queue>
+
+namespace synthesis {
+
+    template<typename ValueType>
+    SmgAbstraction<ValueType>::SmgAbstraction(
+        storm::models::sparse::Model<ValueType> const& quotient,
+        uint64_t quotient_num_actions,
+        std::vector<uint64_t> const& choice_to_action,
+        storm::storage::BitVector const& quotient_choice_mask
+    ) {
+        uint64_t quotient_num_states = quotient.getNumberOfStates();
+        uint64_t quotient_initial_state = *(quotient.getInitialStates().begin());
+        uint64_t quotient_num_choices = quotient.getNumberOfChoices();
+        auto const& quotient_row_groups = quotient.getTransitionMatrix().getRowGroupIndices();
+
+        ItemKeyTranslator<uint64_t> state_action_to_game_state(quotient_num_states);
+        // for Player 1 states, contains available actions; for Player 2 states, contains enabled choices
+        std::vector<std::vector<uint64_t>> game_state_to_choices;
+
+        std::queue<uint64_t> unexplored_states;
+        storm::storage::BitVector state_is_encountered(quotient_num_states,false);
+        unexplored_states.push(quotient_initial_state);
+        state_is_encountered.set(quotient_initial_state,true);
+        std::vector<std::vector<uint64_t>> state_enabled_actions(quotient_num_states);
+        std::vector<std::vector<uint64_t>> state_action_choice(quotient_num_states);
+        while(not unexplored_states.empty()) {
+            uint64_t state = unexplored_states.front();
+            unexplored_states.pop();
+            std::set<uint64_t> enabled_actions;
+            state_action_choice[state] = std::vector(quotient_num_actions,quotient_num_choices);
+            uint64_t player1_state = state_action_to_game_state.translate(state,quotient_num_actions);
+            game_state_to_choices.resize(state_action_to_game_state.numTranslations());
+            for(uint64_t choice = quotient_row_groups[state]; choice < quotient_row_groups[state+1]; ++choice) {
+                if(not quotient_choice_mask[choice]) {
+                    continue;
+                }
+                uint64_t action = choice_to_action[choice];
+                enabled_actions.insert(action);
+                state_action_choice[state][action] = choice;
+                uint64_t player2_state = state_action_to_game_state.translate(state,action);
+                game_state_to_choices.resize(state_action_to_game_state.numTranslations());
+                game_state_to_choices[player2_state].push_back(choice);
+                for(auto const &entry: quotient.getTransitionMatrix().getRow(choice)) {
+                    uint64_t state_dst = entry.getColumn();
+                    if(state_is_encountered[state_dst]) {
+                        continue;
+                    }
+                    unexplored_states.push(state_dst);
+                    state_is_encountered.set(state_dst,true);
+                }
+            }
+            state_enabled_actions[state] = std::vector(enabled_actions.begin(),enabled_actions.end());
+        }
+
+        uint64_t game_num_states = state_action_to_game_state.numTranslations();
+        storm::storage::SparseMatrixBuilder<ValueType> game_matrix_builder(0,0,0,false,true);
+        uint64_t game_num_choices = 0;
+        // for Player 1, contains a representative choice with the appropriate label; for Player 2, contains the corresponding choice
+        std::vector<uint64_t> game_choice_to_quotient_choice;
+        std::vector<bool> game_choice_is_player1;
+
+        for(uint64_t game_state = 0; game_state < game_num_states; ++game_state) {
+            auto [state,state_action] = state_action_to_game_state.retrieve(game_state);
+            game_matrix_builder.newRowGroup(game_num_choices);
+            if(state_action == quotient_num_actions) {
+                // Player 1 state
+                for(uint64_t action: state_enabled_actions[state]) {
+                    uint64_t player2_state = state_action_to_game_state.translate(state,action);
+                    game_matrix_builder.addNextValue(game_num_choices,player2_state,1);
+                    // game_state_to_choices[player1_state].push_back(action);
+                    game_choice_to_quotient_choice.push_back(state_action_choice[state][action]);
+                    game_choice_is_player1.push_back(true);
+                    game_num_choices++;
+                }
+            } else {
+                // Player 2 state
+                uint64_t player2_state = game_state;
+                for(uint64_t choice: game_state_to_choices[game_state]) {
+                    for(auto const& entry: quotient.getTransitionMatrix().getRow(choice)) {
+                        uint64_t state_dst = entry.getColumn();
+                        uint64_t game_state_dst = state_action_to_game_state.translate(state_dst,quotient_num_actions);
+                        game_matrix_builder.addNextValue(game_num_choices,game_state_dst,entry.getValue());
+                    }
+                    game_choice_to_quotient_choice.push_back(choice);
+                    game_choice_is_player1.push_back(false);
+                    game_num_choices++;
+                }
+            }
+        }
+
+        storm::storage::sparse::ModelComponents<ValueType> components;
+        components.transitionMatrix =  game_matrix_builder.build();
+        uint64_t game_initial_state = state_action_to_game_state.translate(quotient_initial_state,quotient_num_actions);
+
+        components.stateLabeling = synthesis::translateStateLabeling(quotient,state_action_to_game_state.translationToItem(),game_initial_state);
+        std::vector<storm::storage::PlayerIndex> game_state_to_player;
+        for(auto [_,action]: state_action_to_game_state.translationToItemKey()) {
+            uint64_t player = action == quotient_num_actions ? 0 : 1;
+            game_state_to_player.push_back(player);
+        }
+        components.statePlayerIndications = std::move(game_state_to_player);
+        // skipping state valuations
+
+        storm::storage::BitVector game_choice_mask(game_num_choices,true);
+        storm::storage::BitVector player1_choice_mask(game_num_choices);
+        for(uint64_t game_choice = 0; game_choice < game_num_choices; ++game_choice) {
+            player1_choice_mask.set(game_choice_is_player1[game_choice]);
+        }
+        components.choiceLabeling = synthesis::translateChoiceLabeling(quotient,game_choice_to_quotient_choice,game_choice_mask);
+        components.rewardModels = synthesis::translateRewardModels(quotient,game_choice_to_quotient_choice,player1_choice_mask);
+        // skipping choice origins
+
+        if (quotient.getType() == storm::models::ModelType::Pomdp) {
+            components.observabilityClasses = synthesis::translateObservabilityClasses(quotient,state_action_to_game_state.translationToItem());
+            // skipping observation valuations
+            this->smg = std::make_shared<synthesis::Posmg<ValueType>>(std::move(components));
+        } else {
+            this->smg = std::make_shared<storm::models::sparse::Smg<ValueType>>(std::move(components));
+        }
+
+        this->state_to_quotient_state_action = state_action_to_game_state.translationToItemKey();
+        this->choice_to_quotient_choice = std::move(game_choice_to_quotient_choice);
+    }
+
+    template class SmgAbstraction<double>;
+}
\ No newline at end of file
diff --git a/payntbind/src/synthesis/pomdp_family/SmgAbstraction.h b/payntbind/src/synthesis/pomdp_family/SmgAbstraction.h
new file mode 100644
index 00000000..db442c8f
--- /dev/null
+++ b/payntbind/src/synthesis/pomdp_family/SmgAbstraction.h
@@ -0,0 +1,45 @@
+#pragma once
+
+#include <storm/models/sparse/Model.h>
+#include <storm/models/sparse/Smg.h>
+
+namespace synthesis {
+
+/**
+ * SMG abstraction for MDP sketch. States of Player 0 are the states of the quotient. In each state s, Player 0
+ * has picks action a, which leads to state (s,a) of Player 1. In state (s,a), Player 1 chooses the color of a
+ * to be executed.
+ */
+template<typename ValueType>
+class SmgAbstraction {
+public:
+
+    /**
+     * Create game abstraction for the sub-MDP.
+     * @param quotient The quotient MDP. If the quotient is a POMDP, then @ref smg can be recast to a Posmg.
+     * @param quotient_num_action The total number of distinct actions in the quotient.
+     * @param choice_to_action For each row of the quotient, the associated action.
+     * @param quotient_choice_mask Choices of the quotient that remained in the sub-MDP.
+     */
+    SmgAbstraction(
+        storm::models::sparse::Model<ValueType> const& quotient,
+        uint64_t quotient_num_actions,
+        std::vector<uint64_t> const& choice_to_action,
+        storm::storage::BitVector const& quotient_choice_mask
+    );
+
+    /** The game. */
+    std::shared_ptr<storm::models::sparse::Smg<ValueType>> smg;
+    /**
+     * For each state s of the game, the corresponding (s,a) pair.
+     * @note States of Player 0 are encoded as (s,num_actions).
+     */
+    std::vector<std::pair<uint64_t,uint64_t>> state_to_quotient_state_action;
+    /**
+     * For each choice of the game, the corresponding choice in the quotient.
+     * @note Choice of Player 0 executing an action is mapped to its arbitrary variant.
+     */
+    std::vector<uint64_t> choice_to_quotient_choice;
+};
+
+}
diff --git a/payntbind/src/synthesis/pomdp_family/bindings.cpp b/payntbind/src/synthesis/pomdp_family/bindings.cpp
index 97b83771..5cb2ccd4 100644
--- a/payntbind/src/synthesis/pomdp_family/bindings.cpp
+++ b/payntbind/src/synthesis/pomdp_family/bindings.cpp
@@ -3,6 +3,7 @@
 #include "ObservationEvaluator.h"
 #include "FscUnfolder.h"
 #include "GameAbstractionSolver.h"
+#include "SmgAbstraction.h"
 
 void bindings_pomdp_family(py::module& m) {
 
@@ -34,10 +35,19 @@ void bindings_pomdp_family(py::module& m) {
     // m.def("randomize_action_variant", &synthesis::randomizeActionVariant<double>);
     py::class_<synthesis::GameAbstractionSolver<double>>(m, "GameAbstractionSolver")
         .def(
-            py::init<storm::models::sparse::Model<double> const&, uint64_t, std::vector<uint64_t> const&, std::string const&, double>(),
-            py::arg("quotient"), py::arg("quoitent_num_actions"), py::arg("choice_to_action"), py::arg("target_label"), py::arg("precision")
+            py::init<
+                storm::models::sparse::Model<double> const&,
+                uint64_t,
+                std::vector<uint64_t> const&,
+                std::shared_ptr<storm::logic::Formula const>,
+                bool,
+                std::string const&,
+                double
+            >(),
+            py::arg("quotient"), py::arg("num_actions"), py::arg("choice_to_action"), py::arg("formula"), py::arg("player1_maximizing"), py::arg("target_label"), py::arg("precision")
         )
-        .def("solve", &synthesis::GameAbstractionSolver<double>::solve)
+        .def("solve_sg", &synthesis::GameAbstractionSolver<double>::solveSg)
+        .def("solve_smg", &synthesis::GameAbstractionSolver<double>::solveSmg)
         .def_property_readonly("solution_state_values", [](synthesis::GameAbstractionSolver<double>& solver) {return solver.solution_state_values;})
         .def_property_readonly("solution_value", [](synthesis::GameAbstractionSolver<double>& solver) {return solver.solution_value;})
         .def_property_readonly("solution_state_to_player1_action", [](synthesis::GameAbstractionSolver<double>& solver) {return solver.solution_state_to_player1_action;})
@@ -45,4 +55,16 @@ void bindings_pomdp_family(py::module& m) {
         .def("enable_profiling", &synthesis::GameAbstractionSolver<double>::enableProfiling)
         .def("print_profiling", &synthesis::GameAbstractionSolver<double>::printProfiling)
         ;
+
+        py::class_<synthesis::SmgAbstraction<double>, std::shared_ptr<synthesis::SmgAbstraction<double>>>(m, "SmgAbstraction")
+        .def(py::init<
+            storm::models::sparse::Model<double> const&,
+            uint64_t,
+            std::vector<uint64_t> const&,
+            storm::storage::BitVector const&
+        >(), py::arg("model"), py::arg("num_actions"), py::arg("choice_to_action"), py::arg("choice_mask"))
+        .def_readonly("smg", &synthesis::SmgAbstraction<double>::smg)
+        .def_readonly("state_to_quotient_state_action", &synthesis::SmgAbstraction<double>::state_to_quotient_state_action)
+        .def_readonly("choice_to_quotient_choice", &synthesis::SmgAbstraction<double>::choice_to_quotient_choice)
+        ;
 }
diff --git a/payntbind/src/synthesis/posmg/Posmg.cpp b/payntbind/src/synthesis/posmg/Posmg.cpp
index 197a1297..9865a85a 100644
--- a/payntbind/src/synthesis/posmg/Posmg.cpp
+++ b/payntbind/src/synthesis/posmg/Posmg.cpp
@@ -1,110 +1,105 @@
 #include "Posmg.h"
 
-namespace synthesis {
-
-    Posmg::Posmg(storm::storage::sparse::ModelComponents<double> const& components)
-        : Smg<double>(components), observations(components.observabilityClasses.value())
-    {
-        calculateP0ObservationCount();
-    }
-    Posmg::Posmg(storm::storage::sparse::ModelComponents<double> &&components)
-        : Smg<double>(std::move(components)), observations(components.observabilityClasses.value())
-    {
-        calculateP0ObservationCount();
-    }
+#include "src/synthesis/translation/componentTranslations.h"
 
-    std::vector<uint32_t> const &Posmg::getObservations() const
-    {
-        return observations;
-    }
-
-    uint32_t Posmg::getObservation(uint64_t state) const
-    {
-        return observations.at(state);
-    }
-
-    uint64_t Posmg::getP0ObservationCount() const
-    {
-        return p0ObservationCount;
-    }
-
-
-    storm::models::sparse::Mdp<double> Posmg::getMdp()
-    {
-        auto components = createComponents(*this);
-
-        return storm::models::sparse::Mdp<double>(std::move(components));
-    }
-
-    storm::models::sparse::Pomdp<double> Posmg::getPomdp()
-    {
-        auto components = createComponents(*this);
-        components.observabilityClasses = this->observations;
-
-        return storm::models::sparse::Pomdp<double>(std::move(components));
-    }
-
-    void Posmg::calculateP0ObservationCount()
-    {
-        // For now, optimizing player always has index 0.
-        // If we need to optimize for another player or for more than one player,
-        // we can for example add a parameter to this method or add a 'optimizingPlayer' property.
-        uint64_t optimizingPlayer = 0;
-
-        auto stateCount = this->getNumberOfStates();
-        auto statePlayerIndications = this->getStatePlayerIndications();
-        std::set<uint32_t> p0Observations;
-
-        for (uint64_t state = 0; state < stateCount; state++)
-        {
-            if (statePlayerIndications[state] == optimizingPlayer)
-            {
-                auto observation = observations[state];
-                p0Observations.insert(observation);
-            }
-        }
-
-        p0ObservationCount = p0Observations.size();
-    }
+namespace synthesis {
 
-    Posmg createPosmg(storm::models::sparse::Pomdp<double> pomdp,
-                      std::vector<storm::storage::PlayerIndex> statePlayerIndications)
+template<typename ValueType, typename RewardModelType>
+Posmg<ValueType,RewardModelType>::Posmg(storm::storage::sparse::ModelComponents<ValueType,RewardModelType> const& components)
+    : storm::models::sparse::Smg<ValueType,RewardModelType>(components), observations(components.observabilityClasses.value())
+{
+    calculateP0ObservationCount();
+}
+template<typename ValueType, typename RewardModelType>
+Posmg<ValueType,RewardModelType>::Posmg(storm::storage::sparse::ModelComponents<ValueType,RewardModelType> &&components)
+    : storm::models::sparse::Smg<ValueType,RewardModelType>(std::move(components)), observations(components.observabilityClasses.value())
+{
+    calculateP0ObservationCount();
+}
+
+template<typename ValueType, typename RewardModelType>
+std::vector<uint32_t> const &Posmg<ValueType,RewardModelType>::getObservations() const
+{
+    return observations;
+}
+
+template<typename ValueType, typename RewardModelType>
+uint32_t Posmg<ValueType,RewardModelType>::getObservation(uint64_t state) const
+{
+    return observations.at(state);
+}
+
+template<typename ValueType, typename RewardModelType>
+uint64_t Posmg<ValueType,RewardModelType>::getP0ObservationCount() const
+{
+    return p0ObservationCount;
+}
+
+template<typename ValueType, typename RewardModelType>
+storm::models::sparse::Mdp<ValueType,RewardModelType> Posmg<ValueType,RewardModelType>::getMdp()
+{
+    auto components = synthesis::componentsFromModel(*this);
+    return storm::models::sparse::Mdp<ValueType,RewardModelType>(std::move(components));
+}
+
+template<typename ValueType, typename RewardModelType>
+storm::models::sparse::Pomdp<ValueType,RewardModelType> Posmg<ValueType,RewardModelType>::getPomdp()
+{
+    auto components = synthesis::componentsFromModel(*this);
+    components.observabilityClasses = this->observations;
+    return storm::models::sparse::Pomdp<ValueType,RewardModelType>(std::move(components));
+}
+
+template<typename ValueType, typename RewardModelType>
+void Posmg<ValueType,RewardModelType>::calculateP0ObservationCount()
+{
+    // For now, optimizing player always has index 0.
+    // If we need to optimize for another player or for more than one player,
+    // we can for example add a parameter to this method or add a 'optimizingPlayer' property.
+    uint64_t optimizingPlayer = 0;
+
+    auto stateCount = this->getNumberOfStates();
+    auto statePlayerIndications = this->getStatePlayerIndications();
+    std::set<uint32_t> p0Observations;
+
+    for (uint64_t state = 0; state < stateCount; state++)
     {
-        auto components = createComponents(pomdp);
-
-        // Smg components
-        components.statePlayerIndications = statePlayerIndications;
-        // todo playerNameToIndexMap ??
-
-        // Pomdp components
-        components.observabilityClasses = pomdp.getObservations();
-        if (pomdp.hasObservationValuations())
+        if (statePlayerIndications[state] == optimizingPlayer)
         {
-            components.observationValuations = pomdp.getObservationValuations();
+            auto observation = observations[state];
+            p0Observations.insert(observation);
         }
-
-        return Posmg(components);
     }
 
-    storm::storage::sparse::ModelComponents<double> createComponents(
-            storm::models::sparse::NondeterministicModel<double> const& model)
-    {
-        storm::storage::sparse::ModelComponents<double> components(
-            model.getTransitionMatrix(),
-            model.getStateLabeling(),
-            model.getRewardModels()
-        );
-        if (model.hasChoiceLabeling()) {
-            components.choiceLabeling = model.getChoiceLabeling();
-        }
-        if (model.hasStateValuations()) {
-            components.stateValuations = model.getStateValuations();
-        }
-        if (model.hasChoiceOrigins()) {
-            components.choiceOrigins = model.getChoiceOrigins();
-        }
-
-        return components;
-    }
+    p0ObservationCount = p0Observations.size();
+}
+
+template class Posmg<double>;
+
+
+template<typename ValueType, typename RewardModelType>
+Posmg<ValueType,RewardModelType> posmgFromPomdp(
+    storm::models::sparse::Pomdp<ValueType,RewardModelType> pomdp,
+    std::vector<storm::storage::PlayerIndex> statePlayerIndications) {
+    auto components = synthesis::componentsFromModel<ValueType>(pomdp);
+    components.statePlayerIndications = statePlayerIndications;
+    return Posmg<ValueType,RewardModelType>(components);
+}
+
+template<typename ValueType, typename RewardModelType>
+Posmg<ValueType,RewardModelType> posmgFromSmg(
+    storm::models::sparse::Smg<ValueType,RewardModelType> smg,
+    std::optional<std::vector<uint32_t>> observabilityClasses) {
+    auto components = synthesis::componentsFromModel<ValueType>(smg);
+    components.observabilityClasses = observabilityClasses;
+    return Posmg<ValueType,RewardModelType>(components);
+}
+
+template Posmg<double> posmgFromPomdp<double>(
+    storm::models::sparse::Pomdp<double> pomdp,
+    std::vector<storm::storage::PlayerIndex> statePlayerIndications);
+template Posmg<double> posmgFromSmg<double>(
+    storm::models::sparse::Smg<double>,
+    std::optional<std::vector<uint32_t>> observabilityClasses);
 
 } // namespace synthesis
\ No newline at end of file
diff --git a/payntbind/src/synthesis/posmg/Posmg.h b/payntbind/src/synthesis/posmg/Posmg.h
index 9e5ef81e..c3de1536 100644
--- a/payntbind/src/synthesis/posmg/Posmg.h
+++ b/payntbind/src/synthesis/posmg/Posmg.h
@@ -1,29 +1,28 @@
 #pragma once
 
-#include "storm/models/sparse/Smg.h"
-#include "storm/models/sparse/Pomdp.h"
+#include <storm/models/sparse/StandardRewardModel.h>
+#include <storm/models/sparse/Smg.h>
+#include <storm/models/sparse/Pomdp.h>
 #include <storm/adapters/RationalFunctionAdapter.h>
 
 namespace synthesis {
 
 /**
- * @brief A class representing Partially observable multiplayer game
- * @todo make generic with template
+ * @brief A class representing partially observable stochastic multiplayer game.
  */
-class Posmg : public storm::models::sparse::Smg<double> {
+template<class ValueType, typename RewardModelType = storm::models::sparse::StandardRewardModel<ValueType>>
+class Posmg : public storm::models::sparse::Smg<ValueType,RewardModelType> {
     public:
     /**
      * @brief Construct a new Posmg object from model components
      *
      * @param components Both statePlayerIndications and observabilityClasses have to be filled
      */
-    Posmg(storm::storage::sparse::ModelComponents<double> const& components);
-    Posmg(storm::storage::sparse::ModelComponents<double> &&components);
+    Posmg(storm::storage::sparse::ModelComponents<ValueType,RewardModelType> const& components);
+    Posmg(storm::storage::sparse::ModelComponents<ValueType,RewardModelType>&& components);
 
     /**
      * @brief Return a vector of observatinos
-     *
-     * @return std::vector<uint32_t> const&
      */
     std::vector<uint32_t> const &getObservations() const;
 
@@ -37,24 +36,18 @@ class Posmg : public storm::models::sparse::Smg<double> {
 
     /**
      * @brief Return number of observations corresponding to player 0 states.
-     *
-     * @return uint64_t
      */
     uint64_t getP0ObservationCount() const;
 
     /**
      * @brief Get the underlying MDP
-     *
-     * @return storm::models::sparse::Mdp<double>
      */
-    storm::models::sparse::Mdp<double> getMdp();
+    storm::models::sparse::Mdp<ValueType,RewardModelType> getMdp();
 
     /**
      * @brief Get the underlying POMDP
-     *
-     * @return storm::models::sparse::Pomdp<double>
      */
-    storm::models::sparse::Pomdp<double> getPomdp();
+    storm::models::sparse::Pomdp<ValueType,RewardModelType> getPomdp();
 
     private:
     /**
@@ -70,22 +63,23 @@ class Posmg : public storm::models::sparse::Smg<double> {
 };
 
 /**
- * @brief Create and return a Posmg object from pomdp and state indications
- *
- * @param pomdp Model information from this pomdp will be used to create the game
+ * @brief Create a POSMG from a POMDP and state indications.
+ * @param pomdp Base POMDP
  * @param statePlayerIndications Vector indicating which states belong to which player
- * @return Posmg
  */
-Posmg createPosmg(storm::models::sparse::Pomdp<double> pomdp,
-            std::vector<storm::storage::PlayerIndex> statePlayerIndications);
+template<typename ValueType,typename RewardModelType = storm::models::sparse::StandardRewardModel<ValueType>>
+Posmg<ValueType,RewardModelType> posmgFromPomdp(
+    storm::models::sparse::Pomdp<ValueType,RewardModelType> pomdp,
+    std::vector<storm::storage::PlayerIndex> statePlayerIndications);
 
 /**
- * @brief Create and return a Components object based on the provided model
- *
- * @param model Properites to create the ModelComponents are taken from this model.
- * @return storm::storage::sparse::ModelComponents<double>
+ * @brief Create a POSMG from an SMG and observability classes.
+ * @param smg Base SMG
+ * @param observabilityClasses for each state an observability class
  */
-storm::storage::sparse::ModelComponents<double> createComponents(
-        storm::models::sparse::NondeterministicModel<double> const& model);
+template<typename ValueType,typename RewardModelType = storm::models::sparse::StandardRewardModel<ValueType>>
+Posmg<ValueType,RewardModelType> posmgFromSmg(
+    storm::models::sparse::Smg<ValueType,RewardModelType> smg,
+    std::optional<std::vector<uint32_t>> observabilityClasses);
 
 } // namespace synthesis
\ No newline at end of file
diff --git a/payntbind/src/synthesis/posmg/PosmgManager.cpp b/payntbind/src/synthesis/posmg/PosmgManager.cpp
index e4891c6f..2a80a091 100644
--- a/payntbind/src/synthesis/posmg/PosmgManager.cpp
+++ b/payntbind/src/synthesis/posmg/PosmgManager.cpp
@@ -2,7 +2,8 @@
 
 namespace synthesis {
 
-    PosmgManager::PosmgManager(Posmg const& posmg, uint64_t optimizingPlayer)
+    template<typename ValueType>
+    PosmgManager<ValueType>::PosmgManager(Posmg<ValueType> const& posmg, uint64_t optimizingPlayer)
         : posmg(posmg), optimizingPlayer(optimizingPlayer)
     {
         this->calculateObservationMap();
@@ -16,17 +17,20 @@ namespace synthesis {
         this->prototypeDuplicates.resize(posmg.getNumberOfStates());
     }
 
-    std::vector<u_int64_t> PosmgManager::getObservationMapping()
+    template<typename ValueType>
+    std::vector<uint64_t> PosmgManager<ValueType>::getObservationMapping()
     {
         return this->optPlayerObservationMap;
     }
 
-    void PosmgManager::setObservationMemorySize(uint64_t observation, uint64_t memorySize)
+    template<typename ValueType>
+    void PosmgManager<ValueType>::setObservationMemorySize(uint64_t observation, uint64_t memorySize)
     {
         this->optPlayerObservationMemorySize[observation] = memorySize;
     }
 
-    std::vector<uint64_t> PosmgManager::getStatePlayerIndications()
+    template<typename ValueType>
+    std::vector<uint64_t> PosmgManager<ValueType>::getStatePlayerIndications()
     {
         std::vector<uint64_t> statePlayerIndications(this->stateCount);
         for (uint64_t state = 0; state < this->stateCount; state++)
@@ -38,8 +42,8 @@ namespace synthesis {
         return statePlayerIndications;
     }
 
-
-    void PosmgManager::calculateObservationMap()
+    template<typename ValueType>
+    void PosmgManager<ValueType>::calculateObservationMap()
     {
         this->optPlayerObservationMap.clear();
 
@@ -59,7 +63,8 @@ namespace synthesis {
         }
     }
 
-    void PosmgManager::calculateObservationSuccesors()
+    template<typename ValueType>
+    void PosmgManager<ValueType>::calculateObservationSuccesors()
     {
         auto transitionMat = this->posmg.getTransitionMatrix();
         auto stateCount = this->posmg.getNumberOfStates();
@@ -83,7 +88,8 @@ namespace synthesis {
         }
     }
 
-    void PosmgManager::calculatePrototypeActionCount()
+    template<typename ValueType>
+    void PosmgManager<ValueType>::calculatePrototypeActionCount()
     {
         auto prototypeCount = this->posmg.getNumberOfStates();
         this->prototypeActionCount.resize(prototypeCount);
@@ -95,7 +101,8 @@ namespace synthesis {
         }
     }
 
-    void PosmgManager::calculateObservationActions()
+    template<typename ValueType>
+    void PosmgManager<ValueType>::calculateObservationActions()
     {
         for (uint64_t prototype = 0; prototype < this->posmg.getNumberOfStates(); prototype++)
         {
@@ -108,7 +115,8 @@ namespace synthesis {
         }
     }
 
-    void PosmgManager::calculatePrototypeRowIndex()
+    template<typename ValueType>
+    void PosmgManager<ValueType>::calculatePrototypeRowIndex()
     {
         this->prototypeRowIndex.resize(this->posmg.getTransitionMatrix().getRowCount());
 
@@ -125,8 +133,8 @@ namespace synthesis {
         }
     }
 
-
-    void PosmgManager::buildStateSpace()
+    template<typename ValueType>
+    void PosmgManager<ValueType>::buildStateSpace()
     {
         auto prototypeCount = this->posmg.getNumberOfStates();
         this->stateDuplicateCount.resize(prototypeCount, 1); // je potreba resize???
@@ -183,7 +191,8 @@ namespace synthesis {
         }
     }
 
-    void PosmgManager::buildTransitionMatrixSpurious() {
+    template<typename ValueType>
+    void PosmgManager<ValueType>::buildTransitionMatrixSpurious() {
         // calculate maxSuccesorDuplicateCount
         for (auto entry : this->succesors)
         {
@@ -236,14 +245,16 @@ namespace synthesis {
         this->rowGroups[this->stateCount] = this->rowCount;
     }
 
-    uint64_t PosmgManager::translateState(uint64_t prototype, uint64_t memory) {
+    template<typename ValueType>
+    uint64_t PosmgManager<ValueType>::translateState(uint64_t prototype, uint64_t memory) {
         if(memory >= this->prototypeDuplicates[prototype].size()) {
             memory = 0;
         }
         return this->prototypeDuplicates[prototype][memory];
     }
 
-    storm::storage::SparseMatrix<double> PosmgManager::constructTransitionMatrix()
+    template<typename ValueType>
+    storm::storage::SparseMatrix<double> PosmgManager<ValueType>::constructTransitionMatrix()
     {
         storm::storage::SparseMatrixBuilder<double> builder(
             this->rowCount, this->stateCount, 0, true, true, this->stateCount
@@ -266,7 +277,8 @@ namespace synthesis {
         return builder.build();
     }
 
-    storm::models::sparse::StateLabeling PosmgManager::constructStateLabeling()
+    template<typename ValueType>
+    storm::models::sparse::StateLabeling PosmgManager<ValueType>::constructStateLabeling()
     {
         storm::models::sparse::StateLabeling labeling(this->stateCount);
         for (auto const& label : this->posmg.getStateLabeling().getLabels())
@@ -297,7 +309,8 @@ namespace synthesis {
         return labeling;
     }
 
-    void PosmgManager::resetDesignSpace()
+    template<typename ValueType>
+    void PosmgManager<ValueType>::resetDesignSpace()
     {
         this->holeCount = 0;
         this->actionHoles.clear();
@@ -316,7 +329,8 @@ namespace synthesis {
     }
 
     // version where each state of non optimising players has it's own action hole
-    void PosmgManager::buildDesignSpaceSpurious()
+    template<typename ValueType>
+    void PosmgManager<ValueType>::buildDesignSpaceSpurious()
     {
         this->resetDesignSpace();
 
@@ -403,34 +417,40 @@ namespace synthesis {
 
     }
 
-    std::shared_ptr<storm::models::sparse::Mdp<double>> PosmgManager::constructMdp()
+    template<typename ValueType>
+    std::shared_ptr<storm::models::sparse::Mdp<double>> PosmgManager<ValueType>::constructMdp()
     {
         this->buildStateSpace();
         this->buildTransitionMatrixSpurious();
 
-        storm::storage::sparse::ModelComponents<double> components;
+        storm::storage::sparse::ModelComponents<ValueType> components;
         components.transitionMatrix = this->constructTransitionMatrix();
         components.stateLabeling = this->constructStateLabeling();
-        this->mdp = std::make_shared<storm::models::sparse::Mdp<double>>(std::move(components));
+        this->mdp = std::make_shared<storm::models::sparse::Mdp<ValueType>>(std::move(components));
 
         this->buildDesignSpaceSpurious();
 
         return this->mdp;
     }
 
-    bool PosmgManager::isOptPlayerState(uint64_t state){
+    template<typename ValueType>
+    bool PosmgManager<ValueType>::isOptPlayerState(uint64_t state){
         return this->posmg.getStatePlayerIndications()[state] == this->optimizingPlayer;
     }
 
-    uint64_t PosmgManager::getActionCount(uint64_t state)
+    template<typename ValueType>
+    uint64_t PosmgManager<ValueType>::getActionCount(uint64_t state)
     {
         auto prototype = this->statePrototype[state];
         return this->prototypeActionCount[prototype];
     }
 
-    bool PosmgManager::contains(std::vector<uint64_t> v, uint64_t elem)
+    template<typename ValueType>
+    bool PosmgManager<ValueType>::contains(std::vector<uint64_t> v, uint64_t elem)
     {
         return std::find(v.begin(), v.end(), elem) != v.end();
     }
 
+    template class PosmgManager<double>;
+
 } // namespace synthesis
\ No newline at end of file
diff --git a/payntbind/src/synthesis/posmg/PosmgManager.h b/payntbind/src/synthesis/posmg/PosmgManager.h
index f6b9cced..27c347b7 100644
--- a/payntbind/src/synthesis/posmg/PosmgManager.h
+++ b/payntbind/src/synthesis/posmg/PosmgManager.h
@@ -5,17 +5,18 @@
 
 namespace synthesis {
 
+template<class ValueType>
 class PosmgManager {
     public:
 
-        PosmgManager(Posmg const& posmg, uint64_t optimizingPlayer);
+        PosmgManager(Posmg<ValueType> const& posmg, uint64_t optimizingPlayer);
 
         /**
          * @brief unfold memory
          */
         std::shared_ptr<storm::models::sparse::Mdp<double>> constructMdp();
 
-        std::vector<u_int64_t> getObservationMapping();
+        std::vector<uint64_t> getObservationMapping();
 
         void setObservationMemorySize(uint64_t observation, uint64_t memorySize);
 
@@ -164,7 +165,7 @@ class PosmgManager {
         bool contains(std::vector<uint64_t> v, uint64_t elem);
 
         /** original POSMG */
-        Posmg const& posmg;
+        Posmg<ValueType> const& posmg;
 
         /** index of optimizing player */
         uint64_t optimizingPlayer;
@@ -174,7 +175,7 @@ class PosmgManager {
          * observability and the other player has complete observability, we keep a vector of
          * optimizing player's observations, which also serves as a mapping.
          */
-        std::vector<u_int64_t> optPlayerObservationMap;
+        std::vector<uint64_t> optPlayerObservationMap;
 
         // For each row in original posmg contains its index withing its row group
         std::vector<uint64_t> prototypeRowIndex;
@@ -201,7 +202,7 @@ class PosmgManager {
         std::vector<uint64_t> rowMemory;
 
         // Unfolded mdp created from posmg
-        std::shared_ptr<storm::models::sparse::Mdp<double>> mdp;
+        std::shared_ptr<storm::models::sparse::Mdp<ValueType>> mdp;
 
 
 }; // class PosmgManager
diff --git a/payntbind/src/synthesis/posmg/bindings.cpp b/payntbind/src/synthesis/posmg/bindings.cpp
index 93687bec..d5eea1d0 100644
--- a/payntbind/src/synthesis/posmg/bindings.cpp
+++ b/payntbind/src/synthesis/posmg/bindings.cpp
@@ -2,51 +2,52 @@
 
 #include "Posmg.h"
 #include "PosmgManager.h"
+
 #include "storm/models/sparse/Smg.h"
 
 void bindings_posmg(py::module &m) {
-    py::class_<synthesis::Posmg, std::shared_ptr<synthesis::Posmg>, storm::models::sparse::Smg<double>>(m, "Posmg")
+    py::class_<synthesis::Posmg<double>, std::shared_ptr<synthesis::Posmg<double>>, storm::models::sparse::Smg<double>>(m, "Posmg")
     //    .def(py::init<storm::storage::sparse::ModelComponents<double> const&>(), py::arg("components"))
     //    .def(py::init<storm::storage::sparse::ModelComponents<double> &&>(), py::arg("components"));
-        .def("get_observations", &synthesis::Posmg::getObservations)
-        .def("get_p0_observation_count", &synthesis::Posmg::getP0ObservationCount)
-        .def("get_mdp", &synthesis::Posmg::getMdp)
-        .def_property_readonly("nondeterministic_choice_indices", [](synthesis::Posmg const& m) { return m.getNondeterministicChoiceIndices(); })
-        .def("get_pomdp", &synthesis::Posmg::getPomdp)
+        .def("get_observations", &synthesis::Posmg<double>::getObservations)
+        .def("get_p0_observation_count", &synthesis::Posmg<double>::getP0ObservationCount)
+        .def("get_mdp", &synthesis::Posmg<double>::getMdp)
+        .def_property_readonly("nondeterministic_choice_indices", [](synthesis::Posmg<double> const& m) { return m.getNondeterministicChoiceIndices(); })
+        .def("get_pomdp", &synthesis::Posmg<double>::getPomdp)
         // this binding (calculation) is done in stormpy for mdp, but posmg doesn't inherit from mdp, so it is also copied here
-        .def("get_nr_available_actions", [](synthesis::Posmg const& posmg, uint64_t stateIndex)
+        .def("get_nr_available_actions", [](synthesis::Posmg<double> const& posmg, uint64_t stateIndex)
             { return posmg.getNondeterministicChoiceIndices()[stateIndex+1] - posmg.getNondeterministicChoiceIndices()[stateIndex] ; },
              py::arg("state"))
         // same as ^
-        .def("get_choice_index", [](synthesis::Posmg const& posmg, uint64_t state, uint64_t actOff)
+        .def("get_choice_index", [](synthesis::Posmg<double> const& posmg, uint64_t state, uint64_t actOff)
             { return posmg.getNondeterministicChoiceIndices()[state]+actOff; },
              py::arg("state"), py::arg("action_offset"), "gets the choice index for the offset action from the given state.");
 
 
-    m.def("create_posmg", &synthesis::createPosmg, py::arg("pomdp"), py::arg("state_player_indications"));
+    m.def("posmg_from_pomdp", &synthesis::posmgFromPomdp<double>, py::arg("pomdp"), py::arg("state_player_indications"));
+    m.def("posmg_from_smg", &synthesis::posmgFromSmg<double>, py::arg("smg"), py::arg("observability_classes"));
 
-    py::class_<synthesis::PosmgManager, std::shared_ptr<synthesis::PosmgManager>>(m, "PosmgManager")
-        .def(py::init<synthesis::Posmg const&, uint64_t>(), py::arg("posmg"), py::arg("optimizing_player"))
-        .def("construct_mdp", &synthesis::PosmgManager::constructMdp)
-        .def("get_observation_mapping", &synthesis::PosmgManager::getObservationMapping)
-        .def("set_observation_memory_size", &synthesis::PosmgManager::setObservationMemorySize,
+    py::class_<synthesis::PosmgManager<double>, std::shared_ptr<synthesis::PosmgManager<double>>>(m, "PosmgManager")
+        .def(py::init<synthesis::Posmg<double> const&, uint64_t>(), py::arg("posmg"), py::arg("optimizing_player"))
+        .def("construct_mdp", &synthesis::PosmgManager<double>::constructMdp)
+        .def("get_observation_mapping", &synthesis::PosmgManager<double>::getObservationMapping)
+        .def("set_observation_memory_size", &synthesis::PosmgManager<double>::setObservationMemorySize,
             py::arg("observation"), py::arg("memory_size"))
-        .def("get_state_player_indications", &synthesis::PosmgManager::getStatePlayerIndications)
-        .def("get_action_count", &synthesis::PosmgManager::getActionCount, py::arg("state"))
-        .def_property_readonly("state_prototype", [](synthesis::PosmgManager& manager) {return manager.statePrototype;})
-        .def_property_readonly("state_memory", [](synthesis::PosmgManager& manager) {return manager.stateMemory;})
-        .def_property_readonly("observation_memory_size", [](synthesis::PosmgManager& manager) {return manager.optPlayerObservationMemorySize;})
-        .def_property_readonly("observation_actions", [](synthesis::PosmgManager& manager) {return manager.optPlayerObservationActions;})
-        .def_property_readonly("observation_successors", [](synthesis::PosmgManager& manager) {return manager.succesors;})
-        .def_property_readonly("max_successor_memory_size", [](synthesis::PosmgManager& manager) {return manager.maxSuccesorDuplicateCount;})
-        .def_property_readonly("num_holes", [](synthesis::PosmgManager& manager) {return manager.holeCount;})
-        .def_property_readonly("action_holes", [](synthesis::PosmgManager& manager) {return manager.actionHoles;})
-        .def_property_readonly("memory_holes", [](synthesis::PosmgManager& manager) {return manager.memoryHoles;})
-        .def_property_readonly("hole_options", [](synthesis::PosmgManager& manager) {return manager.holeOptionCount;})
-        .def_property_readonly("row_action_hole", [](synthesis::PosmgManager& manager) {return manager.rowActionHole;})
-        .def_property_readonly("row_action_option", [](synthesis::PosmgManager& manager) {return manager.rowActionOption;})
-        .def_property_readonly("row_memory_hole", [](synthesis::PosmgManager& manager) {return manager.rowMemoryHole;})
-        .def_property_readonly("row_memory_option", [](synthesis::PosmgManager& manager) {return manager.rowMemoryOption;})
+        .def("get_state_player_indications", &synthesis::PosmgManager<double>::getStatePlayerIndications)
+        .def("get_action_count", &synthesis::PosmgManager<double>::getActionCount, py::arg("state"))
+        .def_property_readonly("state_prototype", [](synthesis::PosmgManager<double>& manager) {return manager.statePrototype;})
+        .def_property_readonly("state_memory", [](synthesis::PosmgManager<double>& manager) {return manager.stateMemory;})
+        .def_property_readonly("observation_memory_size", [](synthesis::PosmgManager<double>& manager) {return manager.optPlayerObservationMemorySize;})
+        .def_property_readonly("observation_actions", [](synthesis::PosmgManager<double>& manager) {return manager.optPlayerObservationActions;})
+        .def_property_readonly("observation_successors", [](synthesis::PosmgManager<double>& manager) {return manager.succesors;})
+        .def_property_readonly("max_successor_memory_size", [](synthesis::PosmgManager<double>& manager) {return manager.maxSuccesorDuplicateCount;})
+        .def_property_readonly("num_holes", [](synthesis::PosmgManager<double>& manager) {return manager.holeCount;})
+        .def_property_readonly("action_holes", [](synthesis::PosmgManager<double>& manager) {return manager.actionHoles;})
+        .def_property_readonly("memory_holes", [](synthesis::PosmgManager<double>& manager) {return manager.memoryHoles;})
+        .def_property_readonly("hole_options", [](synthesis::PosmgManager<double>& manager) {return manager.holeOptionCount;})
+        .def_property_readonly("row_action_hole", [](synthesis::PosmgManager<double>& manager) {return manager.rowActionHole;})
+        .def_property_readonly("row_action_option", [](synthesis::PosmgManager<double>& manager) {return manager.rowActionOption;})
+        .def_property_readonly("row_memory_hole", [](synthesis::PosmgManager<double>& manager) {return manager.rowMemoryHole;})
+        .def_property_readonly("row_memory_option", [](synthesis::PosmgManager<double>& manager) {return manager.rowMemoryOption;})
         ;
-
 }
diff --git a/payntbind/src/synthesis/quotient/Family.cpp b/payntbind/src/synthesis/quotient/Family.cpp
index bdef7f5c..47aeee7f 100644
--- a/payntbind/src/synthesis/quotient/Family.cpp
+++ b/payntbind/src/synthesis/quotient/Family.cpp
@@ -30,15 +30,18 @@ uint64_t Family::addHole(uint64_t num_options) {
 }
 
 void Family::holeSetOptions(uint64_t hole, std::vector<uint64_t> const& options) {
-    hole_options[hole] = options;
     hole_options_mask[hole].clear();
-    for(auto option: options) {
+    for(uint64_t option: options) {
         hole_options_mask[hole].set(option);
     }
+    hole_options[hole].clear();
+    for(uint64_t option: hole_options_mask[hole]) {
+        hole_options[hole].push_back(option);
+    }
 }
 void Family::holeSetOptions(uint64_t hole, BitVector const& options) {
     hole_options[hole].clear();
-    for(auto option: options) {
+    for(uint64_t option: options) {
         hole_options[hole].push_back(option);
     }
     hole_options_mask[hole] = options;
diff --git a/payntbind/src/synthesis/smg/bindings.cpp b/payntbind/src/synthesis/smg/bindings.cpp
index 12aba5fb..d1b07bb5 100644
--- a/payntbind/src/synthesis/smg/bindings.cpp
+++ b/payntbind/src/synthesis/smg/bindings.cpp
@@ -1,39 +1,7 @@
 #include "../synthesis.h"
 
-#include <storm/api/verification.h>
-#include <storm/api/storm.h>
-
-#include "modelchecker/SparseSmgRpatlModelChecker.h"
-
-
-namespace synthesis {
-
-    template<typename ValueType>
-    std::shared_ptr<storm::modelchecker::CheckResult> smgModelChecking (
-        storm::models::sparse::Smg<ValueType> const& smg,
-        std::shared_ptr<storm::logic::Formula const> formula,
-        bool only_initial_states = false,
-        bool set_produce_schedulers = true,
-        storm::Environment const& env = storm::Environment() 
-    ) {
-        //prepare model checking task
-        auto task = storm::api::createTask<ValueType>(formula, only_initial_states);
-        task.setProduceSchedulers(set_produce_schedulers);
-
-        // call model checker
-        std::shared_ptr<storm::modelchecker::CheckResult> result;
-        synthesis::SparseSmgRpatlModelChecker<storm::models::sparse::Smg<ValueType>> modelchecker(smg);
-        if (modelchecker.canHandle(task)) {
-            result = modelchecker.check(env, task);
-        }
-        return result;
-    }
-
-}
+#include "smgModelChecker.h"
 
 void bindings_smg(py::module& m) {
-
-    m.def("smg_model_checking", &synthesis::smgModelChecking<double>, py::arg("smg"), py::arg("formula"), py::arg("only_initial_states") = false, py::arg("set_produce_schedulers") = true, py::arg("env") = storm::Environment() );
-
+    m.def("model_check_smg", &synthesis::modelCheckSmg<double>, py::arg("smg"), py::arg("formula"), py::arg("only_initial_states") = false, py::arg("set_produce_schedulers") = true, py::arg("env") = storm::Environment() );
 }
-
diff --git a/payntbind/src/synthesis/smg/smgModelChecker.h b/payntbind/src/synthesis/smg/smgModelChecker.h
new file mode 100644
index 00000000..66603178
--- /dev/null
+++ b/payntbind/src/synthesis/smg/smgModelChecker.h
@@ -0,0 +1,36 @@
+#include "../synthesis.h"
+
+#include <storm/api/verification.h>
+#include <storm/api/storm.h>
+
+#include "modelchecker/SparseSmgRpatlModelChecker.h"
+
+
+namespace synthesis {
+
+    template<typename ValueType>
+    std::shared_ptr<storm::modelchecker::CheckResult> modelCheckSmg (
+        storm::models::sparse::Smg<ValueType> const& smg,
+        std::shared_ptr<storm::logic::Formula const> formula,
+        bool only_initial_states = false,
+        bool set_produce_schedulers = true,
+        storm::Environment const& env = storm::Environment()
+    ) {
+        auto task = storm::api::createTask<ValueType>(formula, only_initial_states);
+        task.setProduceSchedulers(set_produce_schedulers);
+        std::shared_ptr<storm::modelchecker::CheckResult> result;
+        synthesis::SparseSmgRpatlModelChecker<storm::models::sparse::Smg<ValueType>> modelchecker(smg);
+        if (modelchecker.canHandle(task)) {
+            result = modelchecker.check(env, task);
+        }
+        return result;
+    }
+
+    template std::shared_ptr<storm::modelchecker::CheckResult> modelCheckSmg (
+        storm::models::sparse::Smg<double> const& smg,
+        std::shared_ptr<storm::logic::Formula const> formula,
+        bool only_initial_states = false,
+        bool set_produce_schedulers = true,
+        storm::Environment const& env = storm::Environment()
+    );
+}
diff --git a/payntbind/src/synthesis/translation/ItemKeyTranslator.h b/payntbind/src/synthesis/translation/ItemKeyTranslator.h
index ad38f484..7aba64dc 100644
--- a/payntbind/src/synthesis/translation/ItemKeyTranslator.h
+++ b/payntbind/src/synthesis/translation/ItemKeyTranslator.h
@@ -36,7 +36,6 @@ namespace synthesis {
     private:
 
         uint64_t num_items;
-        
         std::vector<std::map<K,uint64_t>> item_key_to_translation;
         std::vector<std::pair<uint64_t,K>> translation_to_item_key;
     };
diff --git a/payntbind/src/synthesis/translation/componentTranslations.cpp b/payntbind/src/synthesis/translation/componentTranslations.cpp
index 1d9deb81..a359497b 100644
--- a/payntbind/src/synthesis/translation/componentTranslations.cpp
+++ b/payntbind/src/synthesis/translation/componentTranslations.cpp
@@ -1,6 +1,7 @@
 #include "componentTranslations.h"
 
 #include <storm/models/sparse/Pomdp.h>
+#include <storm/models/sparse/Smg.h>
 #include <storm/utility/builder.h>
 #include <storm/exceptions/NotSupportedException.h>
 #include <storm/exceptions/InvalidModelException.h>
@@ -23,6 +24,11 @@ storm::storage::sparse::ModelComponents<ValueType> componentsFromModel(
         components.observabilityClasses = pomdp.getObservations();
         components.observationValuations = pomdp.getOptionalObservationValuations();
     }
+    if (model.getType() == storm::models::ModelType::Smg) {
+        auto smg = static_cast<storm::models::sparse::Smg<ValueType> const&>(model);
+        components.statePlayerIndications = smg.getStatePlayerIndications();
+        // skipping playerNameToIndexMap since Smg does not directly exposes those
+    }
     return components;
 }