Storm
A Modern Probabilistic Model Checker
All Classes Namespaces Files Functions Variables Typedefs Enumerations Enumerator Friends Macros Pages
ParallelComposition.h
Go to the documentation of this file.
1#pragma once
2
3#include <memory>
4#include <set>
5#include <string>
6#include <vector>
7
8#include <boost/optional.hpp>
9
10#include "Composition.h"
11
12namespace storm {
13namespace jani {
14
16 public:
17 SynchronizationVector(std::vector<std::string> const& input, std::string const& output);
18 SynchronizationVector(std::vector<std::string> const& input);
19
20 std::size_t size() const;
21 std::vector<std::string> const& getInput() const;
22 std::string const& getInput(uint64_t index) const;
23 std::string const& getOutput() const;
24
25 static bool isNoActionInput(std::string const& action);
26
31 boost::optional<std::string> getPrecedingParticipatingAction(uint64_t index) const;
32
37 boost::optional<uint64_t> getPositionOfPrecedingParticipatingAction(uint64_t index) const;
38
43
47 uint64_t getNumberOfActionInputs() const;
48
49 // A marker that can be used as one of the inputs. The semantics is that no action of the corresponding
50 // automaton takes part in the synchronization.
51 static const std::string NO_ACTION_INPUT;
52
53 private:
55 std::vector<std::string> input;
56
58 std::string output;
59};
60
61bool operator==(SynchronizationVector const& vector1, SynchronizationVector const& vector2);
62bool operator!=(SynchronizationVector const& vector1, SynchronizationVector const& vector2);
63
65 bool operator()(SynchronizationVector const& vector1, SynchronizationVector const& vector2) const;
66};
67
68std::ostream& operator<<(std::ostream& stream, SynchronizationVector const& synchronizationVector);
69
71 public:
75 ParallelComposition(std::shared_ptr<Composition> const& subcomposition, std::vector<SynchronizationVector> const& synchronizationVectors);
76
80 ParallelComposition(std::vector<std::shared_ptr<Composition>> const& subcompositions, std::vector<SynchronizationVector> const& synchronizationVectors);
81
85 ParallelComposition(std::vector<std::shared_ptr<Composition>> const& subcompositions, std::set<std::string> const& synchronizationAlphabet);
86
90 ParallelComposition(std::shared_ptr<Composition> const& leftSubcomposition, std::shared_ptr<Composition> const& rightSubcomposition,
91 std::set<std::string> const& synchronizationAlphabet);
92
93 virtual bool isParallelComposition() const override;
94
98 Composition const& getSubcomposition(uint64_t index) const;
99
103 std::vector<std::shared_ptr<Composition>> const& getSubcompositions() const;
104
108 uint64_t getNumberOfSubcompositions() const;
109
113 SynchronizationVector const& getSynchronizationVector(uint64_t index) const;
114
118 std::vector<SynchronizationVector> const& getSynchronizationVectors() const;
119
123 std::size_t getNumberOfSynchronizationVectors() const;
124
125 virtual boost::any accept(CompositionVisitor& visitor, boost::any const& data) const override;
126
127 virtual void write(std::ostream& stream) const override;
128
129 bool areActionsReused() const;
130
131 private:
135 void checkSynchronizationVectors() const;
136
138 std::vector<std::shared_ptr<Composition>> subcompositions;
139
141 std::vector<SynchronizationVector> synchronizationVectors;
142};
143
144} // namespace jani
145} // namespace storm
uint64_t getNumberOfSubcompositions() const
Retrieves the number of subcompositions of this parallel composition.
virtual void write(std::ostream &stream) const override
std::vector< SynchronizationVector > const & getSynchronizationVectors() const
Retrieves the synchronization vectors of the parallel composition.
std::size_t getNumberOfSynchronizationVectors() const
Retrieves the number of synchronization vectors.
SynchronizationVector const & getSynchronizationVector(uint64_t index) const
Retrieves the synchronization vector with the given index.
virtual bool isParallelComposition() const override
std::vector< std::shared_ptr< Composition > > const & getSubcompositions() const
Retrieves the subcompositions of the parallel composition.
virtual boost::any accept(CompositionVisitor &visitor, boost::any const &data) const override
Composition const & getSubcomposition(uint64_t index) const
Retrieves the subcomposition with the given index.
static const std::string NO_ACTION_INPUT
std::vector< std::string > const & getInput() const
uint64_t getPositionOfFirstParticipatingAction() const
Retrieves the position of the first participating action.
boost::optional< std::string > getPrecedingParticipatingAction(uint64_t index) const
Retrieves the action name that is the last participating action before the given input index.
boost::optional< uint64_t > getPositionOfPrecedingParticipatingAction(uint64_t index) const
Retrieves the position of the last participating action before the given input index.
static bool isNoActionInput(std::string const &action)
uint64_t getNumberOfActionInputs() const
Retrieves the number of action inputs, i.e.
std::string const & getOutput() const
bool operator!=(SynchronizationVector const &vector1, SynchronizationVector const &vector2)
bool operator==(SynchronizationVector const &vector1, SynchronizationVector const &vector2)
std::ostream & operator<<(std::ostream &stream, Assignment const &assignment)
LabParser.cpp.
Definition cli.cpp:18
bool operator()(SynchronizationVector const &vector1, SynchronizationVector const &vector2) const