Browse Source

Further work on adapting classes that store a PRISM program to the new expressions. Commit to switch workplace.

Former-commit-id: 00c1b1324d
main
dehnert 11 years ago
parent
commit
0110758e3e
  1. 80
      src/storage/prism/Command.cpp
  2. 80
      src/storage/prism/Command.h

80
src/storage/prism/Command.cpp

@ -1,75 +1,39 @@
/*
* Command.cpp
*
* Created on: 12.01.2013
* Author: Christian Dehnert
*/
#include <sstream>
#include <iostream>
#include "Command.h"
#include "src/parser/prismparser/VariableState.h"
namespace storm {
namespace ir {
Command::Command() : actionName(), guardExpression(), updates(), globalIndex() {
// Nothing to do here.
}
Command::Command(uint_fast64_t globalIndex, std::string const& actionName, std::unique_ptr<storm::ir::expressions::BaseExpression>&& guardExpression, std::vector<storm::ir::Update> const& updates)
: actionName(actionName), guardExpression(std::move(guardExpression)), updates(updates), globalIndex(globalIndex) {
namespace prism {
Command::Command(uint_fast64_t globalIndex, std::string const& actionName, storm::expressions::Expression const& guardExpression, std::vector<storm::prism::Update> const& updates) : actionName(actionName), guardExpression(guardExpression), updates(updates), globalIndex(globalIndex) {
// Nothing to do here.
}
Command::Command(Command const& oldCommand, uint_fast64_t newGlobalIndex, std::map<std::string, std::string> const& renaming, storm::parser::prism::VariableState& variableState)
: actionName(oldCommand.getActionName()), guardExpression(oldCommand.guardExpression->clone(renaming, variableState)), globalIndex(newGlobalIndex) {
auto renamingPair = renaming.find(this->actionName);
if (renamingPair != renaming.end()) {
this->actionName = renamingPair->second;
Command::Command(Command const& oldCommand, uint_fast64_t newGlobalIndex, std::map<std::string, std::string> const& renaming) : actionName(oldCommand.getActionName()), guardExpression(oldCommand.getGuardExpression().substitute<std::map>(renaming)), globalIndex(newGlobalIndex) {
auto const& namePair = renaming.find(this->actionName);
if (namePair != renaming.end()) {
this->actionName = namePair->second;
}
this->updates.reserve(oldCommand.getNumberOfUpdates());
for (Update const& update : oldCommand.updates) {
this->updates.emplace_back(update, variableState.getNextGlobalUpdateIndex(), renaming, variableState);
variableState.nextGlobalUpdateIndex++;
for (Update const& update : oldCommand.getUpdates()) {
this->updates.emplace_back(update, update.getGlobalIndex(), renaming);
}
}
Command::Command(Command const& otherCommand) : actionName(otherCommand.actionName), guardExpression(), updates(otherCommand.updates), globalIndex(otherCommand.globalIndex) {
if (otherCommand.guardExpression != nullptr) {
guardExpression = otherCommand.guardExpression->clone();
}
}
Command& Command::operator=(Command const& otherCommand) {
if (this != &otherCommand) {
this->actionName = otherCommand.actionName;
this->guardExpression = otherCommand.guardExpression->clone();
this->updates = otherCommand.updates;
this->globalIndex = otherCommand.globalIndex;
}
return *this;
}
std::string const& Command::getActionName() const {
return this->actionName;
}
std::unique_ptr<storm::ir::expressions::BaseExpression> const& Command::getGuard() const {
storm::expressions::Expression const& Command::getGuardExpression() const {
return guardExpression;
}
uint_fast64_t Command::getNumberOfUpdates() const {
std::size_t Command::getNumberOfUpdates() const {
return this->updates.size();
}
storm::ir::Update const& Command::getUpdate(uint_fast64_t index) const {
storm::prism::Update const& Command::getUpdate(uint_fast64_t index) const {
return this->updates[index];
}
std::vector<storm::ir::Update> const& Command::getUpdates() const {
std::vector<storm::prism::Update> const& Command::getUpdates() const {
return this->updates;
}
@ -77,18 +41,16 @@ namespace storm {
return this->globalIndex;
}
std::string Command::toString() const {
std::stringstream result;
result << "[" << actionName << "] " << guardExpression->toString() << " -> ";
for (uint_fast64_t i = 0; i < updates.size(); ++i) {
result << updates[i].toString();
if (i < updates.size() - 1) {
result << " + ";
std::ostream& operator<<(std::ostream& stream, Command const& command) {
stream << "[" << command.getActionName() << "] " << command.getGuardExpression() << " -> ";
for (uint_fast64_t i = 0; i < command.getUpdates().size(); ++i) {
stream << command.getUpdate(i);
if (i < command.getUpdates().size() - 1) {
stream << " + ";
}
}
result << ";";
return result.str();
stream << ";";
return stream;
}
} // namespace ir
} // namespace storm

80
src/storage/prism/Command.h

@ -1,69 +1,42 @@
/*
* Command.h
*
* Created on: 06.01.2013
* Author: Christian Dehnert
*/
#ifndef STORM_IR_COMMAND_H_
#define STORM_IR_COMMAND_H_
#ifndef STORM_STORAGE_PRISM_COMMAND_H_
#define STORM_STORAGE_PRISM_COMMAND_H_
#include <vector>
#include <string>
#include <map>
#include "expressions/BaseExpression.h"
#include "Update.h"
#include "src/storage/expressions/Expression.h"
#include "src/storage/prism/Update.h"
namespace storm {
namespace parser {
namespace prism {
class VariableState;
} // namespace prismparser
} // namespace parser
namespace ir {
/*!
* A class representing a command.
*/
namespace prism {
class Command {
public:
/*!
* Default constructor. Creates a a command without name, guard and updates.
*/
Command();
/*!
* Creates a command with the given name, guard and updates.
* Creates a command with the given action name, guard and updates.
*
* @param globalIndex The global index of the command.
* @param actionName The action name of the command.
* @param guardExpression the expression that defines the guard of the command.
* @param updates A list of updates that is associated with this command.
*/
Command(uint_fast64_t globalIndex, std::string const& actionName, std::unique_ptr<storm::ir::expressions::BaseExpression>&& guardExpression, std::vector<storm::ir::Update> const& updates);
Command(uint_fast64_t globalIndex, std::string const& actionName, storm::expressions::Expression const& guardExpression, std::vector<storm::prism::Update> const& updates);
/*!
* Creates a copy of the given command and performs the provided renaming.
*
* @param oldCommand The command to copy.
* @param newGlobalIndex The global index of the copy of the command.
* @param renaming A mapping from names that are to be renamed to the names they are to be
* replaced with.
* @param variableState An object knowing about the variables in the system.
*/
Command(Command const& oldCommand, uint_fast64_t newGlobalIndex, std::map<std::string, std::string> const& renaming, storm::parser::prism::VariableState& variableState);
/*!
* Performs a deep-copy of the given command.
*
* @param otherCommand The command to copy.
* @param renaming A mapping from names that are to be renamed to the names they are to be replaced with.
*/
Command(Command const& otherCommand);
Command(Command const& oldCommand, uint_fast64_t newGlobalIndex, std::map<std::string, std::string> const& renaming);
Command& operator=(Command const& otherCommand);
// Create default implementations of constructors/assignment.
Command() = default;
Command(Command const& otherVariable) = default;
Command& operator=(Command const& otherVariable)= default;
Command(Command&& otherVariable) = default;
Command& operator=(Command&& otherVariable) = default;
/*!
* Retrieves the action name of this command.
@ -77,28 +50,28 @@ namespace storm {
*
* @return A reference to the guard of the command.
*/
std::unique_ptr<storm::ir::expressions::BaseExpression> const& getGuard() const;
storm::expressions::Expression const& getGuardExpression() const;
/*!
* Retrieves the number of updates associated with this command.
*
* @return The number of updates associated with this command.
*/
uint_fast64_t getNumberOfUpdates() const;
std::size_t getNumberOfUpdates() const;
/*!
* Retrieves a reference to the update with the given index.
*
* @return A reference to the update with the given index.
*/
storm::ir::Update const& getUpdate(uint_fast64_t index) const;
storm::prism::Update const& getUpdate(uint_fast64_t index) const;
/*!
* Retrieves a vector of all updates associated with this command.
*
* @return A vector of updates associated with this command.
*/
std::vector<storm::ir::Update> const& getUpdates() const;
std::vector<storm::prism::Update> const& getUpdates() const;
/*!
* Retrieves the global index of the command, that is, a unique index over all modules.
@ -107,28 +80,23 @@ namespace storm {
*/
uint_fast64_t getGlobalIndex() const;
/*!
* Retrieves a string representation of this command.
*
* @return A string representation of this command.
*/
std::string toString() const;
friend std::ostream& operator<<(std::ostream& stream, Command const& command);
private:
// The name of the command.
std::string actionName;
// The expression that defines the guard of the command.
std::unique_ptr<storm::ir::expressions::BaseExpression> guardExpression;
storm::expressions::Expression guardExpression;
// The list of updates of the command.
std::vector<storm::ir::Update> updates;
std::vector<storm::prism::Update> updates;
// The global index of the command.
uint_fast64_t globalIndex;
};
} // namespace ir
} // namespace prism
} // namespace storm
#endif /* STORM_IR_COMMAND_H_ */
#endif /* STORM_STORAGE_PRISM_COMMAND_H_ */
Loading…
Cancel
Save