ParallelComposition.h

Go to the documentation of this file.

#pragma once
 
#include <cstdint>
#include <memory>
#include <set>
#include <string>
#include <vector>
 
#include <boost/optional.hpp>
 
#include "Composition.h"
 
namespace storm {
namespace jani {
 
class SynchronizationVector {
   public:
    SynchronizationVector(std::vector<std::string> const& input, std::string const& output);
    SynchronizationVector(std::vector<std::string> const& input);
 
    std::size_t size() const;
    std::vector<std::string> const& getInput() const;
    std::string const& getInput(uint64_t index) const;
    std::string const& getOutput() const;
 
    static bool isNoActionInput(std::string const& action);

    boost::optional<std::string> getPrecedingParticipatingAction(uint64_t index) const;

    boost::optional<uint64_t> getPositionOfPrecedingParticipatingAction(uint64_t index) const;

    uint64_t getPositionOfFirstParticipatingAction() const;

    uint64_t getNumberOfActionInputs() const;
 
    // A marker that can be used as one of the inputs. The semantics is that no action of the corresponding
    // automaton takes part in the synchronization.
    static const std::string NO_ACTION_INPUT;
 
   private:
    std::vector<std::string> input;

    std::string output;
};
 
bool operator==(SynchronizationVector const& vector1, SynchronizationVector const& vector2);
bool operator!=(SynchronizationVector const& vector1, SynchronizationVector const& vector2);
 
struct SynchronizationVectorLexicographicalLess {
    bool operator()(SynchronizationVector const& vector1, SynchronizationVector const& vector2) const;
};
 
std::ostream& operator<<(std::ostream& stream, SynchronizationVector const& synchronizationVector);
 
class ParallelComposition : public Composition {
   public:
    ParallelComposition(std::shared_ptr<Composition> const& subcomposition, std::vector<SynchronizationVector> const& synchronizationVectors);

    ParallelComposition(std::vector<std::shared_ptr<Composition>> const& subcompositions, std::vector<SynchronizationVector> const& synchronizationVectors);

    ParallelComposition(std::vector<std::shared_ptr<Composition>> const& subcompositions, std::set<std::string> const& synchronizationAlphabet);

    ParallelComposition(std::shared_ptr<Composition> const& leftSubcomposition, std::shared_ptr<Composition> const& rightSubcomposition,
                        std::set<std::string> const& synchronizationAlphabet);
 
    virtual bool isParallelComposition() const override;

    Composition const& getSubcomposition(uint64_t index) const;

    std::vector<std::shared_ptr<Composition>> const& getSubcompositions() const;

    uint64_t getNumberOfSubcompositions() const;

    SynchronizationVector const& getSynchronizationVector(uint64_t index) const;

    std::vector<SynchronizationVector> const& getSynchronizationVectors() const;

    std::size_t getNumberOfSynchronizationVectors() const;
 
    virtual boost::any accept(CompositionVisitor& visitor, boost::any const& data) const override;
 
    virtual void write(std::ostream& stream) const override;
 
    bool areActionsReused() const;
 
   private:
    void checkSynchronizationVectors() const;

    std::vector<std::shared_ptr<Composition>> subcompositions;

    std::vector<SynchronizationVector> synchronizationVectors;
};
 
}  // namespace jani
}  // namespace storm