Sebastian Junges
5 years ago
32 changed files with 1442 additions and 91 deletions
-
8.travis.yml
-
15CMakeLists.txt
-
56cmake/CMakeLists.txt
-
3cmake/config.py.in
-
3doc/source/advanced_topics.rst
-
1doc/source/api.rst
-
7doc/source/api/gspn.rst
-
84doc/source/doc/gspns.rst
-
28examples/analysis/04-analysis.py
-
21examples/gspns/01-gspns.py
-
53examples/gspns/02-gspns.py
-
4lib/stormpy/examples/files.py
-
130lib/stormpy/examples/files/gspn/gspn_simple.pnml
-
16lib/stormpy/examples/files/gspn/gspn_simple.pnpro
-
7lib/stormpy/gspn/__init__.py
-
65lib/stormpy/storage/__init__.py
-
21setup.py
-
1setup/config.py
-
2src/dft/dft.cpp
-
2src/gspn/common.h
-
251src/gspn/gspn.cpp
-
7src/gspn/gspn.h
-
14src/mod_gspn.cpp
-
68src/storage/matrix.cpp
-
112src/storage/prism.cpp
-
11tests/configurations.py
-
2tests/dft/test_io.py
-
4tests/gspn/conftest.py
-
252tests/gspn/test_gspn.py
-
282tests/storage/test_matrix_builder.py
-
2tests/storage/test_state_generation.py
-
1travis/build-helper.sh
@ -0,0 +1,7 @@ |
|||||
|
Stormpy.gspn |
||||
|
************************** |
||||
|
|
||||
|
.. automodule:: stormpy.gspn |
||||
|
:members: |
||||
|
:undoc-members: |
||||
|
:imported-members: |
||||
@ -0,0 +1,84 @@ |
|||||
|
********************************** |
||||
|
Generalized Stochastic Petri Nets |
||||
|
********************************** |
||||
|
|
||||
|
Loading GSPNs |
||||
|
============== |
||||
|
.. seealso:: `01-gspns.py <https://github.com/moves-rwth/stormpy/blob/master/examples/gspns/01-gspns.py>`_ |
||||
|
|
||||
|
|
||||
|
Generalized stochastic Petri nets can be given either in the PNPRO format or in the PNML format. |
||||
|
We start by loading a GSPN stored in the PNML format:: |
||||
|
|
||||
|
>>> import stormpy |
||||
|
>>> import stormpy.gspn |
||||
|
>>> import stormpy.examples |
||||
|
>>> import stormpy.examples.files |
||||
|
|
||||
|
>>> import_path = stormpy.examples.files.gspn_pnml_simple |
||||
|
>>> gspn_parser = stormpy.gspn.GSPNParser() |
||||
|
>>> gspn = gspn_parser.parse(import_path) |
||||
|
|
||||
|
After loading, we can display some properties of the GSPN:: |
||||
|
|
||||
|
>>> print("Name of GSPN: {}.".format(gspn.get_name())) |
||||
|
Name of GSPN: simple_gspn. |
||||
|
>>> print("Number of places: {}.".format(gspn.get_number_of_places())) |
||||
|
Number of places: 4. |
||||
|
>>> print("Number of immediate transitions: {}.".format(gspn.get_number_of_immediate_transitions())) |
||||
|
Number of immediate transitions: 3. |
||||
|
>>> print("Number of timed transitions: {}.".format(gspn.get_number_of_timed_transitions())) |
||||
|
Number of timed transitions: 2. |
||||
|
|
||||
|
Building GSPNs |
||||
|
============================= |
||||
|
.. seealso:: `02-gspns.py <https://github.com/moves-rwth/stormpy/blob/master/examples/gspns/02-gspns.py>`_ |
||||
|
|
||||
|
In the following, we describe how to construct GSPNs via the ``GSPNBuilder``. |
||||
|
First, we create an instance of the ``GSPNBuilder`` and set the name of the GSPN:: |
||||
|
|
||||
|
>>> builder = stormpy.gspn.GSPNBuilder() |
||||
|
>>> builder.set_name("my_gspn") |
||||
|
|
||||
|
In the next step, we add an immediate transition to the GSPN. |
||||
|
Additionally, we define the position of the transition by setting its layout information:: |
||||
|
|
||||
|
>>> it_1 = builder.add_immediate_transition(1, 0.0, "it_1") |
||||
|
>>> it_layout = stormpy.gspn.LayoutInfo(1.5, 2.0) |
||||
|
>>> builder.set_transition_layout_info(it_1, it_layout) |
||||
|
|
||||
|
We add a timed transition and set its layout information:: |
||||
|
|
||||
|
>>> tt_1 = builder.add_timed_transition(0, 0.4, "tt_1") |
||||
|
>>> tt_layout = stormpy.gspn.LayoutInfo(12.5, 2.0) |
||||
|
>>> builder.set_transition_layout_info(tt_1, tt_layout) |
||||
|
|
||||
|
Next, we add two places to the GSPN and set their layouts:: |
||||
|
|
||||
|
>>> place_1 = builder.add_place(1, 1, "place_1") |
||||
|
>>> p1_layout = stormpy.gspn.LayoutInfo(6.5, 2.0) |
||||
|
>>> builder.set_place_layout_info(place_1, p1_layout) |
||||
|
|
||||
|
>>> place_2 = builder.add_place(1, 0, "place_2") |
||||
|
>>> p2_layout = stormpy.gspn.LayoutInfo(18.5, 2.0) |
||||
|
>>> builder.set_place_layout_info(place_2, p2_layout) |
||||
|
|
||||
|
Places and transitions can be linked by input, output and inhibition arcs. |
||||
|
We add the arcs of our GSPN as follows:: |
||||
|
|
||||
|
>>> builder.add_output_arc(it_1, place_1) |
||||
|
>>> builder.add_inhibition_arc(place_1, it_1) |
||||
|
>>> builder.add_input_arc(place_1, tt_1) |
||||
|
>>> builder.add_output_arc(tt_1, place_2) |
||||
|
|
||||
|
We can now build the GSPN:: |
||||
|
|
||||
|
>>> gspn = builder.build_gspn() |
||||
|
|
||||
|
After building, we export the GSPN. |
||||
|
GSPNs can be saved in the PNPRO format via ``export_gspn_pnpro_file(path)`` and in the PNML format via ``export_gspn_pnml_file(path)``. |
||||
|
We export the GSPN into the PNPRO format:: |
||||
|
|
||||
|
>>> export_path = stormpy.examples.files.gspn_pnpro_simple |
||||
|
>>> gspn.export_gspn_pnpro_file(export_path) |
||||
|
|
||||
@ -0,0 +1,28 @@ |
|||||
|
import stormpy |
||||
|
import stormpy.core |
||||
|
|
||||
|
import stormpy.examples |
||||
|
import stormpy.examples.files |
||||
|
|
||||
|
|
||||
|
def example_analysis_04(): |
||||
|
path = stormpy.examples.files.prism_dtmc_die |
||||
|
prism_program = stormpy.parse_prism_program(path) |
||||
|
|
||||
|
formula_str = "P=? [F s=7 & d=2]" |
||||
|
properties = stormpy.parse_properties(formula_str, prism_program) |
||||
|
|
||||
|
options = stormpy.BuilderOptions([p.raw_formula for p in properties]) |
||||
|
options.set_build_state_valuations() |
||||
|
model = stormpy.build_sparse_model_with_options(prism_program, options) |
||||
|
|
||||
|
result = stormpy.model_checking(model, properties[0]) |
||||
|
|
||||
|
# Print the model checking result for all states |
||||
|
|
||||
|
print("Model checking results:") |
||||
|
for i in range(len(model.states)): |
||||
|
print("\tstate #{}\t {}:\t {}".format(i,model.state_valuations.get_state(i),result.at(i))) |
||||
|
|
||||
|
if __name__ == '__main__': |
||||
|
example_analysis_04() |
||||
@ -0,0 +1,21 @@ |
|||||
|
import stormpy |
||||
|
import stormpy.gspn |
||||
|
|
||||
|
import stormpy.examples |
||||
|
import stormpy.examples.files |
||||
|
|
||||
|
|
||||
|
def example_gspns_01(): |
||||
|
# Load a GSPN from file (PNML format) |
||||
|
import_path = stormpy.examples.files.gspn_pnml_simple |
||||
|
gspn_parser = stormpy.gspn.GSPNParser() |
||||
|
gspn = gspn_parser.parse(import_path) |
||||
|
|
||||
|
print("Name of GSPN: {}.".format(gspn.get_name())) |
||||
|
print("Number of places: {}.".format(gspn.get_number_of_places())) |
||||
|
print("Number of immediate transitions: {}.".format(gspn.get_number_of_immediate_transitions())) |
||||
|
print("Number of timed transitions: {}.".format(gspn.get_number_of_timed_transitions())) |
||||
|
|
||||
|
|
||||
|
if __name__ == '__main__': |
||||
|
example_gspns_01() |
||||
@ -0,0 +1,53 @@ |
|||||
|
import stormpy |
||||
|
import stormpy.gspn |
||||
|
|
||||
|
import stormpy.examples |
||||
|
import stormpy.examples.files |
||||
|
|
||||
|
|
||||
|
def example_gspns_02(): |
||||
|
# Use GSPNBuilder to construct a GSPN |
||||
|
builder = stormpy.gspn.GSPNBuilder() |
||||
|
builder.set_name("my_gspn") |
||||
|
|
||||
|
# Add immediate transition |
||||
|
it_1 = builder.add_immediate_transition(1, 0.0, "it_1") |
||||
|
it_layout = stormpy.gspn.LayoutInfo(1.5, 2.0) |
||||
|
builder.set_transition_layout_info(it_1, it_layout) |
||||
|
|
||||
|
# Add timed transition |
||||
|
tt_1 = builder.add_timed_transition(0, 0.4, "tt_1") |
||||
|
tt_layout = stormpy.gspn.LayoutInfo(12.5, 2.0) |
||||
|
builder.set_transition_layout_info(tt_1, tt_layout) |
||||
|
|
||||
|
# Add places |
||||
|
place_1 = builder.add_place(1, 1, "place_1") |
||||
|
p1_layout = stormpy.gspn.LayoutInfo(6.5, 2.0) |
||||
|
builder.set_place_layout_info(place_1, p1_layout) |
||||
|
|
||||
|
place_2 = builder.add_place(1, 0, "place_2") |
||||
|
p2_layout = stormpy.gspn.LayoutInfo(18.5, 2.0) |
||||
|
builder.set_place_layout_info(place_2, p2_layout) |
||||
|
|
||||
|
# Link places and transitions by arcs |
||||
|
builder.add_output_arc(it_1, place_1) |
||||
|
builder.add_inhibition_arc(place_1, it_1) |
||||
|
builder.add_input_arc(place_1, tt_1) |
||||
|
builder.add_output_arc(tt_1, place_2) |
||||
|
|
||||
|
# Build GSPN |
||||
|
gspn = builder.build_gspn() |
||||
|
|
||||
|
print("Name of GSPN: {}.".format(gspn.get_name())) |
||||
|
print("Number of places: {}.".format(gspn.get_number_of_places())) |
||||
|
print("Number of immediate transitions: {}.".format(gspn.get_number_of_immediate_transitions())) |
||||
|
print("Number of timed transitions: {}.".format(gspn.get_number_of_timed_transitions())) |
||||
|
|
||||
|
# Export to file (PNPRO format) |
||||
|
export_path = stormpy.examples.files.gspn_pnpro_simple |
||||
|
gspn.export_gspn_pnpro_file(export_path) |
||||
|
|
||||
|
|
||||
|
if __name__ == '__main__': |
||||
|
example_gspns_02() |
||||
|
|
||||
@ -0,0 +1,130 @@ |
|||||
|
<pnml> |
||||
|
<net id="simple_gspn"> |
||||
|
<place id="place_1"> |
||||
|
<initialMarking> |
||||
|
<value>Default,1</value> |
||||
|
</initialMarking> |
||||
|
<capacity> |
||||
|
<value>Default,1</value> |
||||
|
</capacity> |
||||
|
</place> |
||||
|
<place id="place_2"> |
||||
|
<initialMarking> |
||||
|
<value>Default,0</value> |
||||
|
</initialMarking> |
||||
|
<capacity> |
||||
|
<value>Default,1</value> |
||||
|
</capacity> |
||||
|
</place> |
||||
|
<place id="place_3"> |
||||
|
<initialMarking> |
||||
|
<value>Default,0</value> |
||||
|
</initialMarking> |
||||
|
<capacity> |
||||
|
<value>Default,1</value> |
||||
|
</capacity> |
||||
|
</place> |
||||
|
<place id="place_4"> |
||||
|
<initialMarking> |
||||
|
<value>Default,0</value> |
||||
|
</initialMarking> |
||||
|
<capacity> |
||||
|
<value>Default,1</value> |
||||
|
</capacity> |
||||
|
</place> |
||||
|
<transition id="it_1"> |
||||
|
<rate> |
||||
|
<value>1</value> |
||||
|
</rate> |
||||
|
<timed> |
||||
|
<value>false</value> |
||||
|
</timed> |
||||
|
</transition> |
||||
|
<transition id="it_2"> |
||||
|
<rate> |
||||
|
<value>1</value> |
||||
|
</rate> |
||||
|
<timed> |
||||
|
<value>false</value> |
||||
|
</timed> |
||||
|
</transition> |
||||
|
<transition id="it_3"> |
||||
|
<rate> |
||||
|
<value>1</value> |
||||
|
</rate> |
||||
|
<timed> |
||||
|
<value>false</value> |
||||
|
</timed> |
||||
|
</transition> |
||||
|
<transition id="tt_1"> |
||||
|
<rate> |
||||
|
<value>0.4</value> |
||||
|
</rate> |
||||
|
<timed> |
||||
|
<value>true</value> |
||||
|
</timed> |
||||
|
</transition> |
||||
|
<transition id="tt_2"> |
||||
|
<rate> |
||||
|
<value>0.4</value> |
||||
|
</rate> |
||||
|
<timed> |
||||
|
<value>true</value> |
||||
|
</timed> |
||||
|
</transition> |
||||
|
<arc id="arc0" source="place_1" target="it_1" > |
||||
|
<inscription> |
||||
|
<value>Default,1</value> |
||||
|
</inscription> |
||||
|
<type value="inhibition" /> |
||||
|
</arc> |
||||
|
<arc id="arc1" source="it_1" target="place_1" > |
||||
|
<inscription> |
||||
|
<value>Default,1</value> |
||||
|
</inscription> |
||||
|
<type value="normal" /> |
||||
|
</arc> |
||||
|
<arc id="arc2" source="place_2" target="it_2" > |
||||
|
<inscription> |
||||
|
<value>Default,1</value> |
||||
|
</inscription> |
||||
|
<type value="normal" /> |
||||
|
</arc> |
||||
|
<arc id="arc3" source="it_2" target="place_3" > |
||||
|
<inscription> |
||||
|
<value>Default,1</value> |
||||
|
</inscription> |
||||
|
<type value="normal" /> |
||||
|
</arc> |
||||
|
<arc id="arc4" source="place_4" target="it_3" > |
||||
|
<inscription> |
||||
|
<value>Default,1</value> |
||||
|
</inscription> |
||||
|
<type value="normal" /> |
||||
|
</arc> |
||||
|
<arc id="arc5" source="place_1" target="tt_1" > |
||||
|
<inscription> |
||||
|
<value>Default,1</value> |
||||
|
</inscription> |
||||
|
<type value="normal" /> |
||||
|
</arc> |
||||
|
<arc id="arc6" source="tt_1" target="place_2" > |
||||
|
<inscription> |
||||
|
<value>Default,1</value> |
||||
|
</inscription> |
||||
|
<type value="normal" /> |
||||
|
</arc> |
||||
|
<arc id="arc7" source="place_3" target="tt_2" > |
||||
|
<inscription> |
||||
|
<value>Default,1</value> |
||||
|
</inscription> |
||||
|
<type value="normal" /> |
||||
|
</arc> |
||||
|
<arc id="arc8" source="tt_2" target="place_4" > |
||||
|
<inscription> |
||||
|
<value>Default,1</value> |
||||
|
</inscription> |
||||
|
<type value="normal" /> |
||||
|
</arc> |
||||
|
</net> |
||||
|
</pnml> |
||||
@ -0,0 +1,16 @@ |
|||||
|
<project name="storm-export" version="121"> |
||||
|
<gspn name="my_gspn" > |
||||
|
<nodes> |
||||
|
<place marking="1" name ="place_1" x="6.5" y="2" /> |
||||
|
<place marking="0" name ="place_2" x="18.5" y="2" /> |
||||
|
<transition name="tt_1" type="EXP" nservers="1" delay="0.4000000000" x="12.50000000" y="2.000000000" /> |
||||
|
<transition name="it_1" type="IMM" priority="1" weight="1.000000000" x="1.500000000" y="2.000000000" /> |
||||
|
</nodes> |
||||
|
<edges> |
||||
|
<arc head="tt_1" tail="place_1" kind="INPUT" mult="1" /> |
||||
|
<arc head="place_2" tail="tt_1" kind="OUTPUT" mult="1" /> |
||||
|
<arc head="it_1" tail="place_1" kind="INHIBITOR" mult="1" /> |
||||
|
<arc head="place_1" tail="it_1" kind="OUTPUT" mult="1" /> |
||||
|
</edges> |
||||
|
</gspn> |
||||
|
</project> |
||||
@ -0,0 +1,7 @@ |
|||||
|
from . import _config |
||||
|
|
||||
|
if not _config.storm_with_gspn: |
||||
|
raise ImportError("No support for GSPNs was built in Storm.") |
||||
|
|
||||
|
from . import gspn |
||||
|
from .gspn import * |
||||
@ -1,4 +1,67 @@ |
|||||
|
|
||||
import stormpy.utility |
import stormpy.utility |
||||
from . import storage |
from . import storage |
||||
from .storage import * |
from .storage import * |
||||
|
|
||||
|
|
||||
|
def build_sparse_matrix(array, row_group_indices=[]): |
||||
|
""" |
||||
|
Build a sparse matrix from numpy array. |
||||
|
|
||||
|
:param numpy array: The array. |
||||
|
:param List[double] row_group_indices: List containing the starting row of each row group in ascending order. |
||||
|
:return: Sparse matrix. |
||||
|
""" |
||||
|
|
||||
|
num_row = array.shape[0] |
||||
|
num_col = array.shape[1] |
||||
|
|
||||
|
len_group_indices = len(row_group_indices) |
||||
|
if len_group_indices > 0: |
||||
|
builder = storage.SparseMatrixBuilder(rows=num_row, columns=num_col, has_custom_row_grouping=True, |
||||
|
row_groups=len_group_indices) |
||||
|
else: |
||||
|
builder = storage.SparseMatrixBuilder(rows=num_row, columns=num_col) |
||||
|
|
||||
|
row_group_index = 0 |
||||
|
for r in range(num_row): |
||||
|
# check whether to start a custom row group |
||||
|
if row_group_index < len_group_indices and r == row_group_indices[row_group_index]: |
||||
|
builder.new_row_group(r) |
||||
|
row_group_index += 1 |
||||
|
# insert values of the current row |
||||
|
for c in range(num_col): |
||||
|
builder.add_next_value(r, c, array[r, c]) |
||||
|
|
||||
|
return builder.build() |
||||
|
|
||||
|
def build_parametric_sparse_matrix(array, row_group_indices=[]): |
||||
|
""" |
||||
|
Build a sparse matrix from numpy array. |
||||
|
|
||||
|
:param numpy array: The array. |
||||
|
:param List[double] row_group_indices: List containing the starting row of each row group in ascending order. |
||||
|
:return: Parametric sparse matrix. |
||||
|
""" |
||||
|
|
||||
|
num_row = array.shape[0] |
||||
|
num_col = array.shape[1] |
||||
|
|
||||
|
len_group_indices = len(row_group_indices) |
||||
|
if len_group_indices > 0: |
||||
|
builder = storage.ParametricSparseMatrixBuilder(rows=num_row, columns=num_col, has_custom_row_grouping=True, |
||||
|
row_groups=len_group_indices) |
||||
|
else: |
||||
|
builder = storage.ParametricSparseMatrixBuilder(rows=num_row, columns=num_col) |
||||
|
|
||||
|
row_group_index = 0 |
||||
|
for r in range(num_row): |
||||
|
# check whether to start a custom row group |
||||
|
if row_group_index < len_group_indices and r == row_group_indices[row_group_index]: |
||||
|
builder.new_row_group(r) |
||||
|
row_group_index += 1 |
||||
|
# insert values of the current row |
||||
|
for c in range(num_col): |
||||
|
builder.add_next_value(r, c, array[r, c]) |
||||
|
|
||||
|
return builder.build() |
||||
|
|
||||
@ -0,0 +1,2 @@ |
|||||
|
#include "src/common.h" |
||||
|
#include "storm-gspn/api/storm-gspn.h" |
||||
@ -0,0 +1,251 @@ |
|||||
|
#include "gspn.h"
|
||||
|
#include "src/helpers.h"
|
||||
|
#include "storm-gspn/storage/gspn/GSPN.h"
|
||||
|
#include "storm-gspn/storage/gspn/GspnBuilder.h"
|
||||
|
#include "storm/settings/SettingsManager.h"
|
||||
|
|
||||
|
#include "storm-gspn/parser/GspnParser.h"
|
||||
|
#include "storm/utility/file.h"
|
||||
|
|
||||
|
using GSPN = storm::gspn::GSPN; |
||||
|
using GSPNBuilder = storm::gspn::GspnBuilder; |
||||
|
using LayoutInfo = storm::gspn::LayoutInfo; |
||||
|
using Place = storm::gspn::Place; |
||||
|
using TimedTransition = storm::gspn::TimedTransition<GSPN::RateType>; |
||||
|
using ImmediateTransition = storm::gspn::ImmediateTransition<GSPN::WeightType>; |
||||
|
using Transition = storm::gspn::Transition; |
||||
|
using TransitionPartition = storm::gspn::TransitionPartition; |
||||
|
using GSPNParser = storm::parser::GspnParser; |
||||
|
|
||||
|
|
||||
|
void gspnToFile(GSPN const& gspn, std::string const& filepath, bool toPnpro) { |
||||
|
std::ofstream fs; |
||||
|
storm::utility::openFile(filepath, fs); |
||||
|
|
||||
|
if(toPnpro) { |
||||
|
gspn.toPnpro(fs); |
||||
|
} |
||||
|
else { |
||||
|
gspn.toPnml(fs); |
||||
|
} |
||||
|
storm::utility::closeFile(fs); |
||||
|
} |
||||
|
|
||||
|
|
||||
|
void define_gspn(py::module& m) { |
||||
|
|
||||
|
// GSPN_Builder class
|
||||
|
py::class_<GSPNBuilder, std::shared_ptr<GSPNBuilder>>(m, "GSPNBuilder", "Generalized Stochastic Petri Net Builder") |
||||
|
.def(py::init(), "Constructor") |
||||
|
.def("set_name", &GSPNBuilder::setGspnName, "Set name of GSPN", "name"_a) |
||||
|
|
||||
|
.def("add_place", &GSPNBuilder::addPlace, "Add a place to the GSPN", py::arg("capacity") = 1, py::arg("initial_tokens") = 0, py::arg("name") = "") |
||||
|
.def("set_place_layout_info", &GSPNBuilder::setPlaceLayoutInfo, py::arg("place_id"), py::arg("layout_info"), R"doc( |
||||
|
Set place layout information. |
||||
|
|
||||
|
:param uint64_t id: The ID of the place. |
||||
|
:param stormpy.LayoutInfo layout_info: The layout information. |
||||
|
)doc") |
||||
|
|
||||
|
.def("add_immediate_transition", &GSPNBuilder::addImmediateTransition, "Add an immediate transition to the GSPN", "priority"_a = 0, "weight"_a = 0, "name"_a = "") |
||||
|
.def("add_timed_transition", py::overload_cast<uint_fast64_t const&, double const& , std::string const&>(&GSPNBuilder::addTimedTransition), "Add a timed transition to the GSPN", "priority"_a, "rate"_a, "name"_a = "") |
||||
|
.def("add_timed_transition", py::overload_cast<uint_fast64_t const&, double const& , boost::optional<uint64_t> const&, std::string const&>(&GSPNBuilder::addTimedTransition), "priority"_a, "rate"_a, "num_servers"_a, "name"_a = "") |
||||
|
.def("set_transition_layout_info", &GSPNBuilder::setTransitionLayoutInfo, "transition_id"_a, "layout_info"_a, R"doc( |
||||
|
Set transition layout information. |
||||
|
|
||||
|
:param uint64_t id: The ID of the transition. |
||||
|
:param stormpy.LayoutInfo layout_info: The layout information. |
||||
|
)doc") |
||||
|
|
||||
|
.def("add_input_arc", py::overload_cast<uint_fast64_t const&, uint_fast64_t const&, uint_fast64_t const&>(&GSPNBuilder::addInputArc), "from"_a , "to"_a, "multiplicity"_a = 1, R"doc( |
||||
|
Add a new input arc from a place to a transition |
||||
|
|
||||
|
:param from: The ID or name of the place from which the arc is originating. |
||||
|
:type from: uint_64_t or str |
||||
|
:param uint_64_t to: The ID or name of the transition to which the arc goes to. |
||||
|
:type from: uint_64_t or str |
||||
|
:param uint64_t multiplicity: The multiplicity of the arc, default = 1. |
||||
|
)doc") |
||||
|
.def("add_input_arc", py::overload_cast<std::string const&, std::string const&, uint64_t>(&GSPNBuilder::addInputArc), "from"_a, "to"_a, "multiplicity"_a = 1) |
||||
|
.def("add_inhibition_arc", py::overload_cast<uint_fast64_t const&, uint_fast64_t const&, uint_fast64_t const&>(&GSPNBuilder::addInhibitionArc), "from"_a, "to"_a, "multiplicity"_a = 1, R"doc( |
||||
|
Add an new inhibition arc from a place to a transition. |
||||
|
|
||||
|
:param from: The ID or name of the place from which the arc is originating. |
||||
|
:type from: uint_64_t or str |
||||
|
:param to: The ID or name of the transition to which the arc goes to. |
||||
|
:type to: uint_64_t or str |
||||
|
:param uint64_t multiplicity: The multiplicity of the arc, default = 1. |
||||
|
)doc") |
||||
|
.def("add_inhibition_arc", py::overload_cast<std::string const&, std::string const&, uint64_t>(&GSPNBuilder::addInhibitionArc), "from"_a, "to"_a, "multiplicity"_a = 1) |
||||
|
.def("add_output_arc", py::overload_cast<uint_fast64_t const&, uint_fast64_t const&, uint_fast64_t const&>(&GSPNBuilder::addOutputArc), "from"_a, "to"_a, "multiplicity"_a = 1, R"doc( |
||||
|
Add an new output arc from a transition to a place. |
||||
|
|
||||
|
:param from: The ID or name of the transition from which the arc is originating. |
||||
|
:type from: uint_64_t or str |
||||
|
:param to: The ID or name of the place to which the arc goes to. |
||||
|
:type to: uint_64_t or str |
||||
|
:param uint64_t multiplicity: The multiplicity of the arc, default = 1. |
||||
|
)doc") |
||||
|
.def("add_output_arc", py::overload_cast<std::string const&, std::string const&, uint64_t>(&GSPNBuilder::addOutputArc), "from"_a, "to"_a, "multiplicity"_a) |
||||
|
.def("add_normal_arc", &GSPNBuilder::addNormalArc, "from"_a, "to"_a, "multiplicity"_a = 1, R"doc( |
||||
|
Add an arc from a named element to a named element. |
||||
|
Can be both input or output arc, but not an inhibition arc. |
||||
|
Convenience function for textual format parsers. |
||||
|
|
||||
|
:param str from: Source element in the GSPN from where this arc starts. |
||||
|
:param str to: Target element in the GSPN where this arc ends. |
||||
|
:param uint64_t multiplicity: Multiplicity of the arc, default = 1. |
||||
|
)doc") |
||||
|
|
||||
|
.def("build_gspn", &GSPNBuilder::buildGspn, "Construct GSPN", "expression_manager"_a = nullptr, "constants_substitution"_a = std::map<storm::expressions::Variable, storm::expressions::Expression>()) |
||||
|
; |
||||
|
|
||||
|
// GspnParser class
|
||||
|
py::class_<GSPNParser, std::shared_ptr<GSPNParser>>(m, "GSPNParser") |
||||
|
.def(py::init<>()) |
||||
|
.def("parse", [](GSPNParser& p, std::string const& filename, std::string const& constantDefinitions) -> GSPN& {return *(p.parse(filename,constantDefinitions)); }, "filename"_a, "constant_definitions"_a = "") |
||||
|
; |
||||
|
|
||||
|
// GSPN class
|
||||
|
py::class_<GSPN, std::shared_ptr<GSPN>>(m, "GSPN", "Generalized Stochastic Petri Net") |
||||
|
// Constructor
|
||||
|
.def(py::init<std::string const&, std::vector<Place> const&, std::vector<ImmediateTransition> const&, |
||||
|
std::vector<TimedTransition> const&, std::vector<TransitionPartition> const&, std::shared_ptr<storm::expressions::ExpressionManager> const&, std::map<storm::expressions::Variable, |
||||
|
storm::expressions::Expression> const&>(), "name"_a, "places"_a, "immediate_transitions"_a, "timed_transitions"_a, "partitions"_a, "expression_manager"_a, "constants_substitution"_a = std::map<storm::expressions::Variable, storm::expressions::Expression>()) |
||||
|
|
||||
|
.def("get_name", &GSPN::getName, "Get name of GSPN") |
||||
|
.def("set_name", &GSPN::setName, "Set name of GSPN") |
||||
|
|
||||
|
.def("get_number_of_places", &GSPN::getNumberOfPlaces, "Get the number of places in this GSPN") |
||||
|
.def("get_number_of_immediate_transitions", &GSPN::getNumberOfImmediateTransitions, "Get the number of immediate transitions in this GSPN") |
||||
|
.def("get_number_of_timed_transitions", &GSPN::getNumberOfTimedTransitions, "Get the number of timed transitions in this GSPN") |
||||
|
|
||||
|
.def("get_place", [](GSPN const& g, uint64_t id) -> const Place& {return *(g.getPlace(id)); }, "id"_a, R"doc( |
||||
|
Returns the place with the corresponding id. |
||||
|
|
||||
|
:param uint64_t id: The ID of the place. |
||||
|
:rtype: stormpy.Place |
||||
|
)doc") |
||||
|
.def("get_place", [](GSPN const& g, std::string const& name) -> const Place& {return *(g.getPlace(name)); }, "name"_a) |
||||
|
.def("get_timed_transition", [](GSPN const& g, std::string const& name) -> const TimedTransition& {return *(g.getTimedTransition(name)); }, "name"_a, "Returns the timed transition with the corresponding name") |
||||
|
.def("get_immediate_transition", [](GSPN const& g, std::string const& name) -> const ImmediateTransition& {return *(g.getImmediateTransition(name)); }, "name"_a, "Returns the immediate transition with the corresponding name") |
||||
|
.def("get_transition",[](GSPN const& g, std::string const& name) -> const Transition& {return *(g.getTransition(name)); }, "name"_a, "Returns the transition with the corresponding name") |
||||
|
|
||||
|
.def("get_partitions", &GSPN::getPartitions, "Get the partitions of this GSPN") |
||||
|
.def("get_places", &GSPN::getPlaces, R"doc( |
||||
|
Returns a vector of the places of this GSPN. |
||||
|
|
||||
|
:rtype: list[stormpy.Place] |
||||
|
)doc") |
||||
|
.def("get_timed_transitions", &GSPN::getTimedTransitions, R"doc( |
||||
|
Returns a vector of the timed transitions of this GSPN. |
||||
|
|
||||
|
:rtype: list[stormpy.TimedTransition] |
||||
|
)doc") |
||||
|
.def("get_immediate_transitions", &GSPN::getImmediateTransitions, R"doc( |
||||
|
Returns the immediate transitions of this GSPN. |
||||
|
|
||||
|
:rtype: list[stormpy.ImmediateTransition] |
||||
|
)doc") |
||||
|
.def("get_initial_marking", &GSPN::getInitialMarking, "Computes the initial marking of this GSPN") |
||||
|
|
||||
|
.def("is_valid", &GSPN::isValid, "Perform some checks") |
||||
|
|
||||
|
// GSPN export
|
||||
|
.def("export_gspn_pnpro_file", [](GSPN& g, std::string const& filepath) -> void { gspnToFile(g, filepath, true); }, "filepath"_a, "Export GSPN to PNPRO file") |
||||
|
.def("export_gspn_pnml_file", [](GSPN& g, std::string const& filepath) -> void { gspnToFile(g, filepath, false); }, "filepath"_a, "Export GSPN to PNML file") |
||||
|
|
||||
|
.def_static("timed_transition_id_to_transition_id", &GSPN::timedTransitionIdToTransitionId) |
||||
|
.def_static("immediate_transition_id_to_transition_id", &GSPN::immediateTransitionIdToTransitionId) |
||||
|
.def_static("transition_id_to_timed_transition_id", &GSPN::transitionIdToTimedTransitionId) |
||||
|
.def_static("transition_id_to_immediate_transition_id", &GSPN::transitionIdToImmediateTransitionId) |
||||
|
; |
||||
|
|
||||
|
|
||||
|
// LayoutInfo class
|
||||
|
py::class_<LayoutInfo>(m, "LayoutInfo") |
||||
|
.def(py::init<>()) |
||||
|
.def(py::init<double, double, double>(), "x"_a, "y"_a, "rotation"_a = 0.0) |
||||
|
.def_readwrite("x", &LayoutInfo::x) |
||||
|
.def_readwrite("y", &LayoutInfo::y) |
||||
|
.def_readwrite("rotation", &LayoutInfo::rotation) |
||||
|
; |
||||
|
|
||||
|
// Place class
|
||||
|
py::class_<Place, std::shared_ptr<Place>>(m, "Place", "Place in a GSPN") |
||||
|
.def(py::init<uint64_t>(), "id"_a) |
||||
|
.def("get_name", &Place::getName, "Get name of this place") |
||||
|
.def("set_name", &Place::setName, "name"_a, "Set name of this place") |
||||
|
.def("get_id", &Place::getID, "Get the id of this place") |
||||
|
.def("set_number_of_initial_tokens", &Place::setNumberOfInitialTokens, "tokens"_a, "Set the number of initial tokens of this place") |
||||
|
.def("get_number_of_initial_tokens", &Place::getNumberOfInitialTokens, "Get the number of initial tokens of this place") |
||||
|
.def("set_capacity", &Place::setCapacity, "cap"_a, "Set the capacity of tokens of this place") // problem: boost or lambda [](..
|
||||
|
.def("get_capacity", &Place::getCapacity, "Get the capacity of tokens of this place") |
||||
|
.def("has_restricted_capacity", &Place::hasRestrictedCapacity, "Is capacity of this place restricted") |
||||
|
; |
||||
|
|
||||
|
// Transition class
|
||||
|
py::class_<Transition, std::shared_ptr<Transition>>(m, "Transition", "Transition in a GSPN") |
||||
|
.def(py::init<>()) |
||||
|
.def("get_id", &Transition::getID, "Get id of this transition") |
||||
|
.def("set_name", &Transition::setName, "name"_a, "Set name of this transition") |
||||
|
.def("get_name", &Transition::getName, "Get name of this transition") |
||||
|
.def("set_priority", &Transition::setPriority, "priority"_a, "Set priority of this transition") |
||||
|
.def("get_priority", &Transition::getPriority, "Get priority of this transition") |
||||
|
|
||||
|
.def("set_input_arc_multiplicity", &Transition::setInputArcMultiplicity, "place"_a, "multiplicity"_a, "Set the multiplicity of the input arc originating from the place.") |
||||
|
.def("remove_input_arc", &Transition::removeInputArc, "place"_a, "Remove an input arc connected to a given place.") |
||||
|
.def("exists_input_arc", &Transition::existsInputArc, "place"_a, "Check whether the given place is connected to this transition via an input arc.") |
||||
|
|
||||
|
.def("set_output_arc_multiplicity", &Transition::setOutputArcMultiplicity, "place"_a, "multiplicity"_a, "Set the multiplicity of the output arc going to the place.") |
||||
|
.def("remove_output_arc", &Transition::removeOutputArc, "place"_a, "Remove an output arc connected to a given place.") |
||||
|
.def("exists_output_arc", &Transition::existsOutputArc, "place"_a, "Check whether the given place is connected to this transition via an output arc.") |
||||
|
|
||||
|
.def("set_inhibition_arc_multiplicity", &Transition::setInhibitionArcMultiplicity, "place"_a, "multiplicity"_a, "Set the multiplicity of the inhibition arc originating from the place.") |
||||
|
.def("remove_inhibition_arc", &Transition::removeInhibitionArc, "place"_a, "Remove an inhibition arc connected to a given place.") |
||||
|
.def("exists_inhibition_arc", &Transition::existsInhibitionArc, "place"_a, "Check whether the given place is connected to this transition via an inhibition arc.") |
||||
|
|
||||
|
.def("get_input_places", &Transition::getInputPlaces) |
||||
|
.def("get_output_places", &Transition::getOutputPlaces) |
||||
|
.def("get_inhibition_places", &Transition::getInhibitionPlaces) |
||||
|
|
||||
|
.def("get_input_arc_multiplicity", &Transition::getInputArcMultiplicity, "place"_a, "Returns the corresponding multiplicity.") |
||||
|
.def("get_inhibition_arc_multiplicity", &Transition::getInhibitionArcMultiplicity, "place"_a, "Returns the corresponding multiplicity.") |
||||
|
.def("get_output_arc_multiplicity", &Transition::getOutputArcMultiplicity, "place"_a, "Returns the corresponding multiplicity.") |
||||
|
|
||||
|
.def("is_enabled", &Transition::isEnabled, "marking"_a, "Check if the given marking enables the transition.") |
||||
|
.def("fire", &Transition::fire, "marking"_a, "Fire the transition if possible.") |
||||
|
|
||||
|
; |
||||
|
|
||||
|
// TimedTransition class
|
||||
|
py::class_<TimedTransition, Transition, std::shared_ptr<TimedTransition>>(m, "TimedTransition", "TimedTransition in a GSPN") |
||||
|
.def(py::init<>()) |
||||
|
.def("get_rate", &TimedTransition::getRate, "Get rate of this transition") |
||||
|
.def("set_rate", &TimedTransition::setRate, "rate"_a, "Set rate of this transition") |
||||
|
.def("set_k_server_semantics", &TimedTransition::setKServerSemantics, "k"_a, "Set semantics of this transition") |
||||
|
.def("set_single_server_semantics", &TimedTransition::setSingleServerSemantics, "Set semantics of this transition") |
||||
|
.def("set_infinite_server_semantics", &TimedTransition::setInfiniteServerSemantics, "Set semantics of this transition") |
||||
|
.def("has_k_server_semantics", &TimedTransition::hasKServerSemantics, "Get semantics of this transition") |
||||
|
.def("has_single_server_semantics", &TimedTransition::hasSingleServerSemantics, "Get semantics of this transition") |
||||
|
.def("has_infinite_server_semantics", &TimedTransition::hasInfiniteServerSemantics, "Get semantics of this transition") |
||||
|
.def("get_number_of_servers", &TimedTransition::getNumberOfServers, "Get number of servers") |
||||
|
; |
||||
|
|
||||
|
// ImmediateTransition class
|
||||
|
py::class_<ImmediateTransition, Transition, std::shared_ptr<ImmediateTransition>>(m, "ImmediateTransition", "ImmediateTransition in a GSPN") |
||||
|
.def(py::init<>()) |
||||
|
.def("get_weight", &ImmediateTransition::getWeight, "Get weight of this transition") |
||||
|
.def("set_weight", &ImmediateTransition::setWeight, "weight"_a, "Set weight of this transition") |
||||
|
.def("no_weight_attached", &ImmediateTransition::noWeightAttached, "True iff no weight is attached") |
||||
|
; |
||||
|
|
||||
|
// TransitionPartition class
|
||||
|
py::class_<TransitionPartition>(m, "TransitionPartition") |
||||
|
.def(py::init<>()) |
||||
|
.def_readwrite("priority", &TransitionPartition::priority) |
||||
|
.def_readwrite("transitions", &TransitionPartition::transitions) |
||||
|
.def("nr_transitions", &TransitionPartition::nrTransitions, "Get number of transitions") |
||||
|
; |
||||
|
|
||||
|
} |
||||
@ -0,0 +1,7 @@ |
|||||
|
#pragma once |
||||
|
|
||||
|
#include "common.h" |
||||
|
|
||||
|
void define_gspn(py::module& m); |
||||
|
|
||||
|
|
||||
@ -0,0 +1,14 @@ |
|||||
|
#include "common.h"
|
||||
|
|
||||
|
#include "gspn/gspn.h"
|
||||
|
|
||||
|
PYBIND11_MODULE(gspn, m) { |
||||
|
m.doc() = "Support for GSPNs"; |
||||
|
|
||||
|
#ifdef STORMPY_DISABLE_SIGNATURE_DOC
|
||||
|
py::options options; |
||||
|
options.disable_function_signatures(); |
||||
|
#endif
|
||||
|
|
||||
|
define_gspn(m); |
||||
|
} |
||||
@ -0,0 +1,4 @@ |
|||||
|
from configurations import has_gspn |
||||
|
|
||||
|
if has_gspn: |
||||
|
import stormpy.gspn |
||||
@ -0,0 +1,252 @@ |
|||||
|
import os |
||||
|
|
||||
|
import stormpy |
||||
|
|
||||
|
from configurations import gspn |
||||
|
|
||||
|
|
||||
|
@gspn |
||||
|
class TestGSPNBuilder: |
||||
|
def test_layout_info(self): |
||||
|
layout = stormpy.gspn.LayoutInfo() |
||||
|
assert layout.x == 0 |
||||
|
assert layout.y == 0 |
||||
|
assert layout.rotation == 0 |
||||
|
layout.x = 1 |
||||
|
assert layout.x == 1 |
||||
|
|
||||
|
layout_xy = stormpy.gspn.LayoutInfo(2, 3) |
||||
|
assert layout_xy.x == 2 |
||||
|
assert layout_xy.rotation == 0 |
||||
|
|
||||
|
layout_xyr = stormpy.gspn.LayoutInfo(2, 3, 4) |
||||
|
assert layout_xyr.rotation == 4 |
||||
|
|
||||
|
def test_place(self): |
||||
|
p_id = 4 |
||||
|
place = stormpy.gspn.Place(id=p_id) |
||||
|
assert p_id == place.get_id() |
||||
|
|
||||
|
assert not place.has_restricted_capacity() |
||||
|
place.set_capacity(cap=5) |
||||
|
assert place.has_restricted_capacity() |
||||
|
assert place.get_capacity() == 5 |
||||
|
|
||||
|
p_name = "P_0" |
||||
|
place.set_name(name=p_name) |
||||
|
assert place.get_name() == p_name |
||||
|
|
||||
|
p_tokens = 2 |
||||
|
place.set_number_of_initial_tokens(p_tokens) |
||||
|
assert place.get_number_of_initial_tokens() == p_tokens |
||||
|
|
||||
|
def test_transition(self): |
||||
|
# test TimedTransition |
||||
|
tt = stormpy.gspn.TimedTransition() |
||||
|
tt_name = " tt" |
||||
|
tt.set_name(tt_name) |
||||
|
assert tt_name == tt.get_name() |
||||
|
tt_rate = 0.2 |
||||
|
tt.set_rate(tt_rate) |
||||
|
assert tt_rate == tt.get_rate() |
||||
|
|
||||
|
# connect a place to this transition and test arcs |
||||
|
place = stormpy.gspn.Place(0) |
||||
|
# test input arcs |
||||
|
assert not tt.exists_input_arc(place) |
||||
|
tt.set_input_arc_multiplicity(place, 2) |
||||
|
assert tt.exists_input_arc(place) |
||||
|
assert tt.get_input_arc_multiplicity(place) == 2 |
||||
|
tt.remove_input_arc(place) |
||||
|
assert not tt.exists_input_arc(place) |
||||
|
# test output arcs |
||||
|
assert not tt.exists_output_arc(place) |
||||
|
tt.set_output_arc_multiplicity(place, 3) |
||||
|
assert tt.exists_output_arc(place) |
||||
|
assert tt.get_output_arc_multiplicity(place) == 3 |
||||
|
tt.remove_output_arc(place) |
||||
|
assert not tt.exists_output_arc(place) |
||||
|
# test inhibition arcs |
||||
|
assert not tt.exists_inhibition_arc(place) |
||||
|
tt.set_inhibition_arc_multiplicity(place, 5) |
||||
|
assert tt.exists_inhibition_arc(place) |
||||
|
assert tt.get_inhibition_arc_multiplicity(place) == 5 |
||||
|
tt.remove_inhibition_arc(place) |
||||
|
assert not tt.exists_inhibition_arc(place) |
||||
|
|
||||
|
# test ImmediateTransition |
||||
|
ti = stormpy.gspn.ImmediateTransition() |
||||
|
ti_name = " ti" |
||||
|
ti.set_name(ti_name) |
||||
|
assert ti_name == ti.get_name() |
||||
|
assert ti.no_weight_attached() |
||||
|
ti_weight = 0.2 |
||||
|
ti.set_weight(ti_weight) |
||||
|
assert ti_weight == ti.get_weight() |
||||
|
assert not ti.no_weight_attached() |
||||
|
|
||||
|
def test_build_gspn(self): |
||||
|
gspn_name = "gspn_test" |
||||
|
builder = stormpy.gspn.GSPNBuilder() |
||||
|
|
||||
|
id_p_0 = builder.add_place() |
||||
|
id_p_1 = builder.add_place(initial_tokens=1) |
||||
|
id_p_2 = builder.add_place(initial_tokens=0, name="place_2") |
||||
|
id_p_3 = builder.add_place(capacity=2, initial_tokens=3, name="place_3") |
||||
|
p_layout = stormpy.gspn.LayoutInfo(1, 2) |
||||
|
builder.set_place_layout_info(id_p_0, p_layout) |
||||
|
|
||||
|
id_ti_0 = builder.add_immediate_transition(priority=1, weight=0.5, name="ti_0") |
||||
|
id_ti_1 = builder.add_immediate_transition() |
||||
|
|
||||
|
id_tt_0 = builder.add_timed_transition(priority=2, rate=0.4, name="tt_0") |
||||
|
id_tt_1 = builder.add_timed_transition(priority=0, rate=0.5, num_servers=2, name="tt_1") |
||||
|
|
||||
|
t_layout = stormpy.gspn.LayoutInfo(1, 2) |
||||
|
builder.set_transition_layout_info(id_ti_0, t_layout) |
||||
|
|
||||
|
# add arcs |
||||
|
builder.add_input_arc(id_p_0, id_ti_1, multiplicity=2) |
||||
|
builder.add_input_arc("place_2", "ti_0", multiplicity=2) |
||||
|
|
||||
|
builder.add_output_arc(id_ti_1, id_p_2, multiplicity=2) |
||||
|
builder.add_output_arc("tt_0", "place_3", multiplicity=2) |
||||
|
|
||||
|
builder.add_inhibition_arc(id_p_2, id_tt_0, multiplicity=2) |
||||
|
builder.add_inhibition_arc("place_3", "tt_0", multiplicity=2) |
||||
|
|
||||
|
builder.add_normal_arc("place_3", "tt_0", multiplicity=2) |
||||
|
builder.add_normal_arc("tt_0", "place_3", multiplicity=2) |
||||
|
|
||||
|
# test gspn composition |
||||
|
builder.set_name(gspn_name) |
||||
|
gspn = builder.build_gspn() |
||||
|
|
||||
|
assert gspn.get_name() == gspn_name |
||||
|
assert gspn.is_valid() |
||||
|
assert gspn.get_number_of_immediate_transitions() == 2 |
||||
|
assert gspn.get_number_of_timed_transitions() == 2 |
||||
|
assert gspn.get_number_of_places() == 4 |
||||
|
|
||||
|
assert len(gspn.get_places()) == 4 |
||||
|
assert len(gspn.get_immediate_transitions()) == 2 |
||||
|
assert len(gspn.get_timed_transitions()) == 2 |
||||
|
|
||||
|
# test places |
||||
|
p_0 = gspn.get_place(id_p_0) |
||||
|
assert p_0.get_id() == id_p_0 |
||||
|
|
||||
|
p_1 = gspn.get_place(id_p_1) |
||||
|
assert p_1.get_id() == id_p_1 |
||||
|
assert p_1.get_number_of_initial_tokens() == 1 |
||||
|
|
||||
|
p_2 = gspn.get_place(id_p_2) |
||||
|
assert p_2.get_id() == id_p_2 |
||||
|
assert p_2.get_name() == "place_2" |
||||
|
|
||||
|
p_3 = gspn.get_place(id_p_3) |
||||
|
assert p_3.get_name() == "place_3" |
||||
|
assert p_3.get_capacity() == 2 |
||||
|
assert p_3.get_number_of_initial_tokens() == 3 |
||||
|
assert p_3.has_restricted_capacity() |
||||
|
|
||||
|
# test transitions |
||||
|
ti_0 = gspn.get_immediate_transition("ti_0") |
||||
|
assert ti_0.get_id() == id_ti_0 |
||||
|
assert ti_0.get_weight() == 0.5 |
||||
|
assert ti_0.get_priority() == 1 |
||||
|
|
||||
|
tt_0 = gspn.get_timed_transition("tt_0") |
||||
|
assert tt_0.get_id() == id_tt_0 |
||||
|
assert tt_0.get_rate() == 0.4 |
||||
|
assert tt_0.get_priority() == 2 |
||||
|
|
||||
|
tt_1 = gspn.get_timed_transition("tt_1") |
||||
|
assert tt_1.get_id() == id_tt_1 |
||||
|
assert tt_1.get_number_of_servers() == 2 |
||||
|
|
||||
|
# test new name |
||||
|
gspn_new_name = "new_name" |
||||
|
gspn.set_name(gspn_new_name) |
||||
|
assert gspn.get_name() == gspn_new_name |
||||
|
|
||||
|
def test_export_to_pnpro(self, tmpdir): |
||||
|
builder = stormpy.gspn.GSPNBuilder() |
||||
|
builder.set_name("gspn_test") |
||||
|
|
||||
|
# add places and transitions |
||||
|
id_p_0 = builder.add_place() |
||||
|
id_p_1 = builder.add_place(initial_tokens=3, name="place_1", capacity=2) |
||||
|
id_ti_0 = builder.add_immediate_transition(priority=0, weight=0.5, name="ti_0") |
||||
|
id_tt_0 = builder.add_timed_transition(priority=0, rate=0.5, num_servers=2, name="tt_0") |
||||
|
|
||||
|
gspn = builder.build_gspn() |
||||
|
|
||||
|
export_file = os.path.join(str(tmpdir), "gspn.pnpro") |
||||
|
|
||||
|
# export gspn to pnml |
||||
|
gspn.export_gspn_pnpro_file(export_file) |
||||
|
|
||||
|
# import gspn |
||||
|
gspn_parser = stormpy.gspn.GSPNParser() |
||||
|
gspn_import = gspn_parser.parse(export_file) |
||||
|
|
||||
|
# test imported gspn |
||||
|
assert gspn_import.get_name() == gspn.get_name() |
||||
|
assert gspn_import.get_number_of_timed_transitions() == gspn.get_number_of_timed_transitions() |
||||
|
assert gspn_import.get_number_of_immediate_transitions() == gspn.get_number_of_immediate_transitions() |
||||
|
assert gspn_import.get_number_of_places() == gspn.get_number_of_places() |
||||
|
|
||||
|
p_0 = gspn_import.get_place(id_p_0) |
||||
|
assert p_0.get_id() == id_p_0 |
||||
|
p_1 = gspn_import.get_place(id_p_1) |
||||
|
assert p_1.get_name() == "place_1" |
||||
|
# todo capacity info lost |
||||
|
# assert p_1.get_capacity() == 2 |
||||
|
# assert p_1.has_restricted_capacity() == True |
||||
|
assert p_1.get_number_of_initial_tokens() == 3 |
||||
|
|
||||
|
ti_0 = gspn_import.get_immediate_transition("ti_0") |
||||
|
assert ti_0.get_id() == id_ti_0 |
||||
|
tt_0 = gspn_import.get_timed_transition("tt_0") |
||||
|
assert tt_0.get_id() == id_tt_0 |
||||
|
|
||||
|
def test_export_to_pnml(self, tmpdir): |
||||
|
builder = stormpy.gspn.GSPNBuilder() |
||||
|
builder.set_name("gspn_test") |
||||
|
|
||||
|
# add places and transitions |
||||
|
id_p_0 = builder.add_place() |
||||
|
id_p_1 = builder.add_place(initial_tokens=3, name="place_1", capacity=2) |
||||
|
id_ti_0 = builder.add_immediate_transition(priority=0, weight=0.5, name="ti_0") |
||||
|
id_tt_0 = builder.add_timed_transition(priority=0, rate=0.5, num_servers=2, name="tt_0") |
||||
|
|
||||
|
gspn = builder.build_gspn() |
||||
|
|
||||
|
export_file = os.path.join(str(tmpdir), "gspn.pnml") |
||||
|
|
||||
|
# export gspn to pnml |
||||
|
gspn.export_gspn_pnml_file(export_file) |
||||
|
|
||||
|
# import gspn |
||||
|
gspn_parser = stormpy.gspn.GSPNParser() |
||||
|
gspn_import = gspn_parser.parse(export_file) |
||||
|
|
||||
|
# test imported gspn |
||||
|
assert gspn_import.get_name() == gspn.get_name() |
||||
|
assert gspn_import.get_number_of_timed_transitions() == gspn.get_number_of_timed_transitions() |
||||
|
assert gspn_import.get_number_of_immediate_transitions() == gspn.get_number_of_immediate_transitions() |
||||
|
assert gspn_import.get_number_of_places() == gspn.get_number_of_places() |
||||
|
|
||||
|
p_0 = gspn_import.get_place(id_p_0) |
||||
|
assert p_0.get_id() == id_p_0 |
||||
|
p_1 = gspn_import.get_place(id_p_1) |
||||
|
assert p_1.get_name() == "place_1" |
||||
|
assert p_1.get_capacity() == 2 |
||||
|
assert p_1.get_number_of_initial_tokens() == 3 |
||||
|
assert p_1.has_restricted_capacity() |
||||
|
|
||||
|
ti_0 = gspn_import.get_immediate_transition("ti_0") |
||||
|
assert ti_0.get_id() == id_ti_0 |
||||
|
tt_0 = gspn_import.get_timed_transition("tt_0") |
||||
|
assert tt_0.get_id() == id_tt_0 |
||||
@ -0,0 +1,282 @@ |
|||||
|
import stormpy |
||||
|
|
||||
|
from configurations import numpy_avail |
||||
|
|
||||
|
|
||||
|
class TestMatrixBuilder: |
||||
|
def test_matrix_builder(self): |
||||
|
builder = stormpy.SparseMatrixBuilder(force_dimensions=True) |
||||
|
matrix = builder.build() |
||||
|
assert matrix.nr_columns == 0 |
||||
|
assert matrix.nr_rows == 0 |
||||
|
assert matrix.nr_entries == 0 |
||||
|
|
||||
|
builder_5x5 = stormpy.SparseMatrixBuilder(5, 5, force_dimensions=False) |
||||
|
|
||||
|
builder_5x5.add_next_value(0, 0, 0) |
||||
|
builder_5x5.add_next_value(0, 1, 0.1) |
||||
|
builder_5x5.add_next_value(2, 2, 22) |
||||
|
builder_5x5.add_next_value(2, 3, 23) |
||||
|
|
||||
|
assert builder_5x5.get_last_column() == 3 |
||||
|
assert builder_5x5.get_last_row() == 2 |
||||
|
|
||||
|
builder_5x5.add_next_value(3, 2, 32) |
||||
|
builder_5x5.add_next_value(3, 4, 34) |
||||
|
builder_5x5.add_next_value(4, 3, 43) |
||||
|
|
||||
|
matrix_5x5 = builder_5x5.build() |
||||
|
|
||||
|
assert matrix_5x5.nr_columns == 5 |
||||
|
assert matrix_5x5.nr_rows == 5 |
||||
|
assert matrix_5x5.nr_entries == 7 |
||||
|
|
||||
|
for e in matrix_5x5: |
||||
|
assert (e.value() == 0.1 and e.column == 1) or e.value() == 0 or (e.value() > 20 and e.column > 1) |
||||
|
|
||||
|
def test_parametric_matrix_builder(self): |
||||
|
builder = stormpy.ParametricSparseMatrixBuilder(force_dimensions=True) |
||||
|
matrix = builder.build() |
||||
|
assert matrix.nr_columns == 0 |
||||
|
assert matrix.nr_rows == 0 |
||||
|
assert matrix.nr_entries == 0 |
||||
|
|
||||
|
builder_5x5 = stormpy.ParametricSparseMatrixBuilder(5, 5, force_dimensions=False) |
||||
|
|
||||
|
one_pol = stormpy.RationalRF(1) |
||||
|
one_pol = stormpy.FactorizedPolynomial(one_pol) |
||||
|
first_val = stormpy.FactorizedRationalFunction(one_pol) |
||||
|
|
||||
|
two_pol = stormpy.RationalRF(2) |
||||
|
two_pol = stormpy.FactorizedPolynomial(two_pol) |
||||
|
sec_val = stormpy.FactorizedRationalFunction(two_pol) |
||||
|
|
||||
|
builder_5x5.add_next_value(0, 0, first_val) |
||||
|
builder_5x5.add_next_value(0, 1, first_val) |
||||
|
builder_5x5.add_next_value(2, 2, sec_val) |
||||
|
builder_5x5.add_next_value(2, 3, sec_val) |
||||
|
|
||||
|
assert builder_5x5.get_last_column() == 3 |
||||
|
assert builder_5x5.get_last_row() == 2 |
||||
|
|
||||
|
builder_5x5.add_next_value(3, 2, sec_val) |
||||
|
builder_5x5.add_next_value(3, 4, sec_val) |
||||
|
builder_5x5.add_next_value(4, 3, sec_val) |
||||
|
|
||||
|
matrix_5x5 = builder_5x5.build() |
||||
|
|
||||
|
assert matrix_5x5.nr_columns == 5 |
||||
|
assert matrix_5x5.nr_rows == 5 |
||||
|
assert matrix_5x5.nr_entries == 7 |
||||
|
|
||||
|
for e in matrix_5x5: |
||||
|
assert (e.value() == first_val and e.column < 2) or (e.value() == sec_val and e.column > 1) |
||||
|
|
||||
|
def test_matrix_replace_columns(self): |
||||
|
builder = stormpy.SparseMatrixBuilder(3, 4, force_dimensions=False) |
||||
|
|
||||
|
builder.add_next_value(0, 0, 0) |
||||
|
builder.add_next_value(0, 1, 1) |
||||
|
builder.add_next_value(0, 2, 2) |
||||
|
builder.add_next_value(0, 3, 3) |
||||
|
|
||||
|
builder.add_next_value(1, 1, 1) |
||||
|
builder.add_next_value(1, 2, 2) |
||||
|
builder.add_next_value(1, 3, 3) |
||||
|
|
||||
|
builder.add_next_value(2, 1, 1) |
||||
|
builder.add_next_value(2, 2, 2) |
||||
|
builder.add_next_value(2, 3, 3) |
||||
|
|
||||
|
# replace rows |
||||
|
builder.replace_columns([3, 2, 1], 1) |
||||
|
matrix = builder.build() |
||||
|
|
||||
|
assert matrix.nr_entries == 10 |
||||
|
|
||||
|
# Check if columns where replaced |
||||
|
for e in matrix: |
||||
|
assert (e.value() == 0 and e.column == 0) or (e.value() == 3 and e.column == 1) or ( |
||||
|
e.value() == 2 and e.column == 2) or (e.value() == 1 and e.column == 3) |
||||
|
|
||||
|
def test_parametric_matrix_replace_columns(self): |
||||
|
builder = stormpy.ParametricSparseMatrixBuilder(3, 4, force_dimensions=False) |
||||
|
|
||||
|
one_pol = stormpy.RationalRF(1) |
||||
|
one_pol = stormpy.FactorizedPolynomial(one_pol) |
||||
|
first_val = stormpy.FactorizedRationalFunction(one_pol, one_pol) |
||||
|
two_pol = stormpy.RationalRF(2) |
||||
|
two_pol = stormpy.FactorizedPolynomial(two_pol) |
||||
|
sec_val = stormpy.FactorizedRationalFunction(two_pol, two_pol) |
||||
|
third_val = stormpy.FactorizedRationalFunction(one_pol, two_pol) |
||||
|
|
||||
|
builder.add_next_value(0, 1, first_val) |
||||
|
builder.add_next_value(0, 2, sec_val) |
||||
|
builder.add_next_value(0, 3, third_val) |
||||
|
|
||||
|
builder.add_next_value(1, 1, first_val) |
||||
|
builder.add_next_value(1, 2, sec_val) |
||||
|
builder.add_next_value(1, 3, third_val) |
||||
|
|
||||
|
builder.add_next_value(2, 1, first_val) |
||||
|
builder.add_next_value(2, 2, sec_val) |
||||
|
builder.add_next_value(2, 3, third_val) |
||||
|
|
||||
|
# replace rows |
||||
|
builder.replace_columns([3, 2], 2) |
||||
|
matrix = builder.build() |
||||
|
|
||||
|
assert matrix.nr_entries == 9 |
||||
|
|
||||
|
# Check if columns where replaced |
||||
|
for e in matrix: |
||||
|
assert (e.value() == first_val and e.column == 1) or (e.value() == third_val and e.column == 2) or ( |
||||
|
e.value() == sec_val and e.column == 3) |
||||
|
|
||||
|
def test_matrix_builder_row_grouping(self): |
||||
|
num_rows = 5 |
||||
|
builder = stormpy.SparseMatrixBuilder(num_rows, 6, has_custom_row_grouping=True, row_groups=2) |
||||
|
|
||||
|
builder.new_row_group(1) |
||||
|
assert builder.get_current_row_group_count() == 1 |
||||
|
|
||||
|
builder.new_row_group(4) |
||||
|
assert builder.get_current_row_group_count() == 2 |
||||
|
matrix = builder.build() |
||||
|
|
||||
|
assert matrix.get_row_group_start(0) == 1 |
||||
|
assert matrix.get_row_group_end(0) == 4 |
||||
|
|
||||
|
assert matrix.get_row_group_start(1) == 4 |
||||
|
assert matrix.get_row_group_end(1) == 5 |
||||
|
|
||||
|
def test_parametric_matrix_builder_row_grouping(self): |
||||
|
num_rows = 5 |
||||
|
builder = stormpy.ParametricSparseMatrixBuilder(num_rows, 6, has_custom_row_grouping=True, row_groups=2) |
||||
|
|
||||
|
builder.new_row_group(1) |
||||
|
assert builder.get_current_row_group_count() == 1 |
||||
|
|
||||
|
builder.new_row_group(4) |
||||
|
assert builder.get_current_row_group_count() == 2 |
||||
|
matrix = builder.build() |
||||
|
|
||||
|
assert matrix.get_row_group_start(0) == 1 |
||||
|
assert matrix.get_row_group_end(0) == 4 |
||||
|
|
||||
|
assert matrix.get_row_group_start(1) == 4 |
||||
|
assert matrix.get_row_group_end(1) == 5 |
||||
|
|
||||
|
@numpy_avail |
||||
|
def test_matrix_from_numpy(self): |
||||
|
import numpy as np |
||||
|
array = np.array([[0, 2], |
||||
|
[3, 4], |
||||
|
[0.1, 24], |
||||
|
[-0.3, -4]], dtype='float64') |
||||
|
|
||||
|
matrix = stormpy.build_sparse_matrix(array) |
||||
|
|
||||
|
# Check matrix dimension |
||||
|
assert matrix.nr_rows == array.shape[0] |
||||
|
assert matrix.nr_columns == array.shape[1] |
||||
|
assert matrix.nr_entries == 8 |
||||
|
|
||||
|
# Check matrix values |
||||
|
for r in range(array.shape[1]): |
||||
|
row = matrix.get_row(r) |
||||
|
for e in row: |
||||
|
assert (e.value() == array[r, e.column]) |
||||
|
|
||||
|
@numpy_avail |
||||
|
def test_parametric_matrix_from_numpy(self): |
||||
|
import numpy as np |
||||
|
one_pol = stormpy.RationalRF(1) |
||||
|
one_pol = stormpy.FactorizedPolynomial(one_pol) |
||||
|
first_val = stormpy.FactorizedRationalFunction(one_pol, one_pol) |
||||
|
two_pol = stormpy.RationalRF(2) |
||||
|
two_pol = stormpy.FactorizedPolynomial(two_pol) |
||||
|
sec_val = stormpy.FactorizedRationalFunction(two_pol, two_pol) |
||||
|
third_val = stormpy.FactorizedRationalFunction(one_pol, two_pol) |
||||
|
|
||||
|
array = np.array([[sec_val, first_val], |
||||
|
[first_val, sec_val], |
||||
|
[sec_val, sec_val], |
||||
|
[third_val, third_val]]) |
||||
|
|
||||
|
matrix = stormpy.build_parametric_sparse_matrix(array) |
||||
|
|
||||
|
# Check matrix dimension |
||||
|
assert matrix.nr_rows == array.shape[0] |
||||
|
assert matrix.nr_columns == array.shape[1] |
||||
|
assert matrix.nr_entries == 8 |
||||
|
|
||||
|
# Check matrix values |
||||
|
for r in range(array.shape[1]): |
||||
|
row = matrix.get_row(r) |
||||
|
for e in row: |
||||
|
assert (e.value() == array[r, e.column]) |
||||
|
|
||||
|
@numpy_avail |
||||
|
def test_matrix_from_numpy_row_grouping(self): |
||||
|
import numpy as np |
||||
|
array = np.array([[0, 2], |
||||
|
[3, 4], |
||||
|
[0.1, 24], |
||||
|
[-0.3, -4]], dtype='float64') |
||||
|
|
||||
|
matrix = stormpy.build_sparse_matrix(array, row_group_indices=[1, 3]) |
||||
|
|
||||
|
# Check matrix dimension |
||||
|
assert matrix.nr_rows == array.shape[0] |
||||
|
assert matrix.nr_columns == array.shape[1] |
||||
|
assert matrix.nr_entries == 8 |
||||
|
|
||||
|
# Check matrix values |
||||
|
for r in range(array.shape[1]): |
||||
|
row = matrix.get_row(r) |
||||
|
for e in row: |
||||
|
assert (e.value() == array[r, e.column]) |
||||
|
|
||||
|
# Check row groups |
||||
|
assert matrix.get_row_group_start(0) == 1 |
||||
|
assert matrix.get_row_group_end(0) == 3 |
||||
|
|
||||
|
assert matrix.get_row_group_start(1) == 3 |
||||
|
assert matrix.get_row_group_end(1) == 4 |
||||
|
|
||||
|
@numpy_avail |
||||
|
def test_parametric_matrix_from_numpy_row_grouping(self): |
||||
|
import numpy as np |
||||
|
one_pol = stormpy.RationalRF(1) |
||||
|
one_pol = stormpy.FactorizedPolynomial(one_pol) |
||||
|
first_val = stormpy.FactorizedRationalFunction(one_pol, one_pol) |
||||
|
two_pol = stormpy.RationalRF(2) |
||||
|
two_pol = stormpy.FactorizedPolynomial(two_pol) |
||||
|
sec_val = stormpy.FactorizedRationalFunction(two_pol, two_pol) |
||||
|
third_val = stormpy.FactorizedRationalFunction(one_pol, two_pol) |
||||
|
|
||||
|
array = np.array([[sec_val, first_val], |
||||
|
[first_val, sec_val], |
||||
|
[sec_val, sec_val], |
||||
|
[third_val, third_val]]) |
||||
|
|
||||
|
matrix = stormpy.build_parametric_sparse_matrix(array, row_group_indices=[1, 3]) |
||||
|
|
||||
|
# Check matrix dimension |
||||
|
assert matrix.nr_rows == array.shape[0] |
||||
|
assert matrix.nr_columns == array.shape[1] |
||||
|
assert matrix.nr_entries == 8 |
||||
|
|
||||
|
# Check matrix values |
||||
|
for r in range(array.shape[1]): |
||||
|
row = matrix.get_row(r) |
||||
|
for e in row: |
||||
|
assert (e.value() == array[r, e.column]) |
||||
|
|
||||
|
# Check row groups |
||||
|
assert matrix.get_row_group_start(0) == 1 |
||||
|
assert matrix.get_row_group_end(0) == 3 |
||||
|
|
||||
|
assert matrix.get_row_group_start(1) == 3 |
||||
|
assert matrix.get_row_group_end(1) == 4 |
||||
Write
Preview
Loading…
Cancel
Save
Reference in new issue