diff --git a/src/logic/formulae.cpp b/src/logic/formulae.cpp
index 5b73050..9294c00 100644
--- a/src/logic/formulae.cpp
+++ b/src/logic/formulae.cpp
@@ -1,6 +1,8 @@
 #include "formulae.h"
 #include "storm/logic/Formulas.h"
 #include "storm/logic/CloneVisitor.h"
+#include "storm/logic/LabelSubstitutionVisitor.h"
+
 
 
 void define_formulae(py::module& m) {
@@ -15,6 +17,7 @@ void define_formulae(py::module& m) {
     py::class_<storm::logic::Formula, std::shared_ptr<storm::logic::Formula>> formula(m, "Formula", "Generic Storm Formula");
     formula.def("__str__", &storm::logic::Formula::toString)
         .def("clone", [](storm::logic::Formula const& f) { storm::logic::CloneVisitor cv; return cv.clone(f);})
+        .def("substitute_labels_by_labels", [](storm::logic::Formula const& f, std::map<std::string, std::string> const& labelSubs) {storm::logic::LabelSubstitutionVisitor lsv(labelSubs); return lsv.substitute(f);}, "substitute label occurences", py::arg("replacements"))
     ;
 
     // Path Formulae
diff --git a/src/storage/expressions.cpp b/src/storage/expressions.cpp
index 00799ec..f3f78b4 100644
--- a/src/storage/expressions.cpp
+++ b/src/storage/expressions.cpp
@@ -40,7 +40,8 @@ void define_expressions(py::module& m) {
     py::class_<storm::expressions::Expression, std::shared_ptr<storm::expressions::Expression>>(m, "Expression", "Holds an expression")
         .def("contains_variables", &storm::expressions::Expression::containsVariables, "Check if the expression contains variables.")
         .def("contains_variable", &storm::expressions::Expression::containsVariable, "Check if the expression contains any of the given variables.", py::arg("variables"))
-        .def("is_literal", &storm::expressions::Expression::isLiteral, "Check if the expression is a literal")
+        .def("get_variables" , &storm::expressions::Expression::getVariables, "Get the variables")
+            .def("is_literal", &storm::expressions::Expression::isLiteral, "Check if the expression is a literal")
         .def("has_boolean_type", &storm::expressions::Expression::hasBooleanType, "Check if the expression is a boolean")
         .def("has_integer_type", &storm::expressions::Expression::hasIntegerType, "Check if the expression is an integer")
         .def("has_rational_type", &storm::expressions::Expression::hasRationalType, "Check if the expression is a rational")
diff --git a/src/storage/jani.cpp b/src/storage/jani.cpp
index 3574a35..192f680 100644
--- a/src/storage/jani.cpp
+++ b/src/storage/jani.cpp
@@ -1,6 +1,7 @@
 #include "jani.h"
 #include <storm/storage/jani/Model.h>
 #include <storm/storage/jani/JSONExporter.h>
+#include <storm/storage/expressions/ExpressionManager.h>
 #include "src/helpers.h"
 
 using namespace storm::jani;
@@ -14,10 +15,16 @@ std::string janiToString(Model const& m) {
 void define_jani(py::module& m) {
     py::class_<Model, std::shared_ptr<Model>> md(m, "JaniModel", "A Jani Model");
     md.def_property_readonly("name", &Model::getName, "model name")
+     .def_property_readonly("model_type", &storm::jani::Model::getModelType, "Model type")
             .def_property_readonly("automata", [](const Model& model) {return model.getAutomata();}, "get automata")
             .def_property_readonly("constants", [](const Model& model) {return model.getConstants();}, "get constants")
             .def("restrict_edges", &Model::restrictEdges, "restrict model to edges given by set", py::arg("edge_set"))
+            .def_property_readonly("expression_manager", &Model::getExpressionManager, "get expression manager", pybind11::return_value_policy::reference_internal)
+            .def_property_readonly("has_undefined_constants", &Model::hasUndefinedConstants, "Flag if program has undefined constants")
+            .def_property_readonly("undefined_constants_are_graph_preserving", &Model::undefinedConstantsAreGraphPreserving, "Flag if the undefined constants do not change the graph structure")
             .def("__str__", &janiToString)
+            .def("define_constants", &Model::defineUndefinedConstants, "define constants with a mapping from the corresponding expression variables to expressions", py::arg("map"))
+            .def("substitute_constants", &Model::substituteConstants, "substitute constants")
             .def("get_automaton_index", &Model::getAutomatonIndex, "get index for automaton name")
             .def_static("encode_edge_and_automaton_index", &Model::encodeAutomatonAndEdgeIndices, "get edge/automaton-index")
             .def_static("decode_edge_and_automaton_index", &Model::decodeAutomatonAndEdgeIndices, "get edge and automaton from edge/automaton index")
diff --git a/src/storage/prism.cpp b/src/storage/prism.cpp
index 01338ea..1f52288 100644
--- a/src/storage/prism.cpp
+++ b/src/storage/prism.cpp
@@ -20,7 +20,7 @@ void define_prism(py::module& m) {
             .def("simplify", &Program::simplify, "Simplify")
             .def("used_constants",&Program::usedConstants, "Compute Used Constants")
             .def_property_readonly("expression_manager", &Program::getManager, "Get the expression manager for expressions in this program")
-            .def("to_jani", &Program::toJani, "Transform to Jani program", py::arg("all_variables_global")=false)
+            .def("to_jani", &Program::toJaniWithLabelRenaming, "Transform to Jani program", py::arg("all_variables_global")=false, py::arg("suffix") = "")
             .def("__str__", &streamToString<storm::prism::Program>);
 
     py::class_<Module> module(m, "PrismModule", "A module in a Prism program");
@@ -57,7 +57,7 @@ void define_prism(py::module& m) {
     constant.def_property_readonly("name", &Constant::getName, "Constant name")
             .def_property_readonly("defined", &Constant::isDefined, "Is the constant defined?")
             .def_property_readonly("type", &Constant::getType, "The type of the constant")
-            .def_property_readonly("variable", &Constant::getExpressionVariable, "Expression variable")
+            .def_property_readonly("expression_variable", &Constant::getExpressionVariable, "Expression variable")
             ;