sp
/
tempest
1
0
Fork 0
Code Issues Pull Requests Projects Releases Wiki Activity
Browse Source

Parsing labels works now.

tempestpy_adaptions
dehnert 12 years ago
parent
6a33f84512
commit
f52201466c
9 changed files with 155 additions and 62 deletions
Whitespace
Show all changes Ignore whitespace when comparing lines Ignore changes in amount of whitespace Ignore changes in whitespace at EOL
Split View
Diff Options
Show Stats Download Patch File Download Diff File
  1. 31
      CMakeLists.txt
  2. 3
      src/ir/Command.h
  3. 1
      src/ir/IntegerVariable.h
  4. 12
      src/ir/Module.h
  5. 28
      src/ir/Program.h
  6. 2
      src/ir/Update.h
  7. 6
      src/ir/expressions/VariableExpression.h
  8. 126
      src/parser/PrismParser.h
  9. 8
      test.input

31
CMakeLists.txt
View File

@ -48,6 +48,10 @@ message(STATUS "GMMXX_INCLUDE_DIR is ${GMMXX_INCLUDE_DIR}")
option(DEBUG "Sets whether the DEBUG mode is used" ON)
option(USE_POPCNT "Sets whether the popcnt instruction is going to be used." ON)
option(USE_BOOST_STATIC_LIBRARIES "Sets whether the Boost libraries should be linked statically." ON)
option(LINK_LIBCXXABI "Sets whether libc++abi should be linked" OFF)
set(ADDITIONAL_INCLUDE_DIRS "" CACHE STRING "Additional directories added to the include directories.")
set(ADDITIONAL_LINK_DIRS "" CACHE STRING "Additional directories added to the link directories.")
set(CUSTOM_BOOST_ROOT "" CACHE STRING "A custom path to the Boost root directory.")
# If the DEBUG option was turned on, we will target a debug version and a release version otherwise
if (DEBUG)
@ -74,9 +78,12 @@ elseif(MSVC)
# required for GMM to compile, ugly error directive in their code
add_definitions(/D_SCL_SECURE_NO_DEPRECATE)
else(CLANG)
# As CLANG is not set as a variable, we need to set it in case we have not matched another compiler.
set (CLANG ON)
# Set standard flags for clang
set(CMAKE_CXX_FLAGS_RELEASE "${CMAKE_CXX_FLAGS_RELEASE} -funroll-loops")
set (CMAKE_CXX_FLAGS "-std=c++11 -stdlib=libc++ -Wall -Werror -pedantic -Wno-unused-variable -DBOOST_RESULT_OF_USE_TR1 -DBOOST_NO_DECLTYPE")
# TODO: activate -Werror asap
set (CMAKE_CXX_FLAGS "-std=c++11 -stdlib=libc++ -Wall -pedantic -Wno-unused-variable -DBOOST_RESULT_OF_USE_TR1 -DBOOST_NO_DECLTYPE")
# Turn on popcnt instruction if desired (yes by default)
if (USE_POPCNT)
@ -118,6 +125,11 @@ find_package(Doxygen REQUIRED)
set(Boost_USE_STATIC_LIBS ON)
set(Boost_USE_MULTITHREADED ON)
set(Boost_USE_STATIC_RUNTIME OFF)
# If a custom boost root directory was specified, we set the corresponding hint for the script to find it.
if(CUSTOM_BOOST_ROOT)
set(BOOST_ROOT "${CUSTOM_BOOST_ROOT}")
endif(CUSTOM_BOOST_ROOT)
find_package(Boost REQUIRED COMPONENTS program_options)
if(Boost_FOUND)
@ -138,6 +150,16 @@ include_directories(${EIGEN3_INCLUDE_DIR})
# Add GMMXX to the included directories
include_directories(${GMMXX_INCLUDE_DIR})
# Add custom additional include or link directories
if (ADDITIONAL_INCLUDE_DIRS)
message(STATUS "Using additional include directories ${ADDITIONAL_INCLUDE_DIRS}")
include_directories(${ADDITIONAL_INCLUDE_DIRS})
endif(ADDITIONAL_INCLUDE_DIRS)
if (ADDITIONAL_LINK_DIRS)
message(STATUS "Using additional link directories ${ADDITIONAL_LINK_DIRS}")
link_directories(${ADDITIONAL_LINK_DIRS})
endif(ADDITIONAL_LINK_DIRS)
# Add the executables
# Must be created *after* Boost was added because of LINK_DIRECTORIES
add_executable(storm ${STORM_SOURCES} ${STORM_HEADERS})
@ -147,6 +169,13 @@ add_executable(storm-tests ${STORM_TEST_SOURCES} ${STORM_TEST_HEADERS})
target_link_libraries(storm ${Boost_LIBRARIES})
target_link_libraries(storm-tests ${Boost_LIBRARIES})
# Link against libc++abi if requested. May be needed to build on Linux systems using clang.
if (LINK_LIBCXXABI)
message (STATUS "Linking against libc++abi.")
target_link_libraries(storm "c++abi")
target_link_libraries(storm-tests "c++abi")
endif(LINK_LIBCXXABI)
# Add a target to generate API documentation with Doxygen
if(DOXYGEN_FOUND)
set(CMAKE_DOXYGEN_OUTPUT_DIR "${CMAKE_CURRENT_BINARY_DIR}/doc")

3
src/ir/Command.h
View File

@ -8,7 +8,8 @@
#ifndef COMMAND_H_
#define COMMAND_H_
#include "IR.h"
#include "expressions/BaseExpression.h"
#include "Update.h"
namespace storm {

1
src/ir/IntegerVariable.h
View File

@ -9,6 +9,7 @@
#define INTEGERVARIABLE_H_
#include "Variable.h"
#include "expressions/BaseExpression.h"
namespace storm {

12
src/ir/Module.h
View File

@ -8,7 +8,9 @@
#ifndef MODULE_H_
#define MODULE_H_
#include "IR.h"
#include "BooleanVariable.h"
#include "IntegerVariable.h"
#include "Command.h"
namespace storm {
@ -44,14 +46,6 @@ public:
return result;
}
void addBooleanVariable(storm::ir::BooleanVariable variable) {
booleanVariables.push_back(variable);
}
void addIntegerVariable(storm::ir::IntegerVariable variable) {
integerVariables.push_back(variable);
}
private:
std::string moduleName;

28
src/ir/Program.h
View File

@ -8,12 +8,13 @@
#ifndef PROGRAM_H_
#define PROGRAM_H_
#include "src/ir/expressions/ConstantExpression.h"
#include "expressions/BaseExpression.h"
#include "expressions/BooleanConstantExpression.h"
#include "expressions/IntegerConstantExpression.h"
#include "expressions/DoubleConstantExpression.h"
#include "Module.h"
#include "RewardModel.h"
#include <iostream>
namespace storm {
namespace ir {
@ -27,8 +28,8 @@ public:
}
Program(ModelType modelType, std::map<std::string, std::shared_ptr<storm::ir::expressions::BooleanConstantExpression>> booleanUndefinedConstantExpressions, std::map<std::string, std::shared_ptr<storm::ir::expressions::IntegerConstantExpression>> integerUndefinedConstantExpressions, std::map<std::string, std::shared_ptr<storm::ir::expressions::DoubleConstantExpression>> doubleUndefinedConstantExpressions, std::vector<storm::ir::Module> modules, std::map<std::string, storm::ir::RewardModel> rewards)
: modelType(modelType), booleanUndefinedConstantExpressions(booleanUndefinedConstantExpressions), integerUndefinedConstantExpressions(integerUndefinedConstantExpressions), doubleUndefinedConstantExpressions(doubleUndefinedConstantExpressions), modules(modules), rewards(rewards) {
Program(ModelType modelType, std::map<std::string, std::shared_ptr<storm::ir::expressions::BooleanConstantExpression>> booleanUndefinedConstantExpressions, std::map<std::string, std::shared_ptr<storm::ir::expressions::IntegerConstantExpression>> integerUndefinedConstantExpressions, std::map<std::string, std::shared_ptr<storm::ir::expressions::DoubleConstantExpression>> doubleUndefinedConstantExpressions, std::vector<storm::ir::Module> modules, std::map<std::string, storm::ir::RewardModel> rewards, std::map<std::string, std::shared_ptr<storm::ir::expressions::BaseExpression>> labels)
: modelType(modelType), booleanUndefinedConstantExpressions(booleanUndefinedConstantExpressions), integerUndefinedConstantExpressions(integerUndefinedConstantExpressions), doubleUndefinedConstantExpressions(doubleUndefinedConstantExpressions), modules(modules), rewards(rewards), labels(labels) {
}
@ -71,19 +72,11 @@ public:
result +="\n";
}
return result;
}
void addBooleanUndefinedConstantExpression(std::string constantName, std::shared_ptr<storm::ir::expressions::BooleanConstantExpression> constantExpression) {
booleanUndefinedConstantExpressions[constantName] = constantExpression;
}
void addIntegerUndefinedConstantExpression(std::string constantName, std::shared_ptr<storm::ir::expressions::IntegerConstantExpression> constantExpression) {
integerUndefinedConstantExpressions[constantName] = constantExpression;
}
for (auto label : labels) {
result += "label " + label.first + " = " + label.second->toString() + ";\n";
}
void addDoubleUndefinedConstantExpression(std::string constantName, std::shared_ptr<storm::ir::expressions::DoubleConstantExpression> constantExpression) {
doubleUndefinedConstantExpressions[constantName] = constantExpression;
return result;
}
private:
@ -93,6 +86,7 @@ private:
std::map<std::string, std::shared_ptr<storm::ir::expressions::DoubleConstantExpression>> doubleUndefinedConstantExpressions;
std::vector<storm::ir::Module> modules;
std::map<std::string, storm::ir::RewardModel> rewards;
std::map<std::string, std::shared_ptr<storm::ir::expressions::BaseExpression>> labels;
};
}

2
src/ir/Update.h
View File

@ -8,7 +8,7 @@
#ifndef UPDATE_H_
#define UPDATE_H_
#include "IR.h"
#include "expressions/BaseExpression.h"
namespace storm {

6
src/ir/expressions/VariableExpression.h
View File

@ -10,6 +10,8 @@
#include "src/ir/expressions/BaseExpression.h"
#include <iostream>
namespace storm {
namespace ir {
@ -20,8 +22,8 @@ class VariableExpression : public BaseExpression {
public:
std::string variableName;
VariableExpression(std::string variableName) {
this->variableName = variableName;
VariableExpression(std::string variableName) : variableName(variableName) {
}
virtual ~VariableExpression() {

126
src/parser/PrismParser.h
View File

@ -30,6 +30,10 @@ namespace qi = boost::spirit::qi;
namespace ascii = boost::spirit::ascii;
namespace phoenix = boost::phoenix;
typedef std::istreambuf_iterator<char> base_iterator_type;
typedef boost::spirit::multi_pass<base_iterator_type> forward_iterator_type;
typedef boost::spirit::classic::position_iterator2<forward_iterator_type> pos_iterator_type;
class PrismParser {
public:
@ -40,14 +44,11 @@ public:
}
void getProgram(std::istream& inputStream, std::string const& fileName) {
typedef std::istreambuf_iterator<char> base_iterator_type;
base_iterator_type in_begin(inputStream);
typedef boost::spirit::multi_pass<base_iterator_type> forward_iterator_type;
forward_iterator_type fwd_begin = boost::spirit::make_default_multi_pass(in_begin);
forward_iterator_type fwd_end;
typedef boost::spirit::classic::position_iterator2<forward_iterator_type> pos_iterator_type;
pos_iterator_type position_begin(fwd_begin, fwd_end, fileName);
pos_iterator_type position_end;
@ -58,8 +59,17 @@ public:
} catch(const qi::expectation_failure<pos_iterator_type>& e) {
const boost::spirit::classic::file_position_base<std::string>& pos = e.first.get_position();
std::stringstream msg;
msg << "parse error at file '" << pos.file << "' line " << pos.line << " column " << pos.column << std::endl << "'" << e.first.get_currentline() << "'" << std::endl << std::setw(pos.column + 1) << " " << "^------- here";
std::cout << msg.str() << std::endl;
msg << pos.file << ", line " << pos.line << ", column " << pos.column << ": parse error: expected " << e.what_ << std::endl << "\t" << e.first.get_currentline() << std::endl << "\t";
int i = 0;
for (i = 0; i < pos.column; ++i) {
msg << "-";
}
msg << "^";
for (; i < 80; ++i) {
msg << "-";
}
msg << std::endl;
std::cout << msg.str();
throw storm::exceptions::WrongFileFormatException() << msg.str();
}
@ -68,104 +78,174 @@ public:
private:
template<typename Iterator, typename Skipper>
struct prismGrammar : qi::grammar<Iterator, storm::ir::Program(), qi::locals<std::map<std::string, std::shared_ptr<storm::ir::expressions::BooleanConstantExpression>>, std::map<std::string, std::shared_ptr<storm::ir::expressions::IntegerConstantExpression>>, std::map<std::string, std::shared_ptr<storm::ir::expressions::DoubleConstantExpression>>, std::map<std::string, storm::ir::RewardModel>>, Skipper> {
struct prismGrammar : qi::grammar<Iterator, storm::ir::Program(), qi::locals<std::map<std::string, std::shared_ptr<storm::ir::expressions::BooleanConstantExpression>>, std::map<std::string, std::shared_ptr<storm::ir::expressions::IntegerConstantExpression>>, std::map<std::string, std::shared_ptr<storm::ir::expressions::DoubleConstantExpression>>, std::map<std::string, storm::ir::RewardModel>, std::map<std::string, std::shared_ptr<storm::ir::expressions::BaseExpression>>>, Skipper> {
prismGrammar() : prismGrammar::base_type(start) {
freeIdentifierName %= qi::lexeme[qi::alpha >> *(qi::alnum | qi::char_('_'))] - allVariables_ - allConstants_;
freeIdentifierName %= qi::raw[qi::lexeme[((qi::alpha | qi::char_('_')) >> *(qi::alnum | qi::char_('_'))) - booleanVariables_ - integerVariables_ - allConstants_]];
freeIdentifierName.name("unused identifier");
booleanLiteralExpression = qi::bool_[qi::_val = phoenix::construct<std::shared_ptr<storm::ir::expressions::BaseExpression>>(phoenix::new_<storm::ir::expressions::BooleanLiteral>(qi::_1))];
booleanLiteralExpression.name("boolean literal");
integerLiteralExpression = qi::int_[qi::_val = phoenix::construct<std::shared_ptr<storm::ir::expressions::BaseExpression>>(phoenix::new_<storm::ir::expressions::IntegerLiteral>(qi::_1))];
integerLiteralExpression.name("integer literal");
doubleLiteralExpression = qi::double_[qi::_val = phoenix::construct<std::shared_ptr<storm::ir::expressions::BaseExpression>>(phoenix::new_<storm::ir::expressions::DoubleLiteral>(qi::_1))];
doubleLiteralExpression.name("double literal");
literalExpression %= (booleanLiteralExpression | integerLiteralExpression | doubleLiteralExpression);
literalExpression.name("literal");
integerVariableExpression = integerVariables_;
booleanVariableExpression = booleanVariables_;
variableExpression = (integerVariableExpression | booleanVariableExpression);
integerVariableExpression %= integerVariables_;
integerVariableExpression.name("integer variable");
booleanVariableExpression %= booleanVariables_;
booleanVariableExpression.name("boolean variable");
variableExpression %= (integerVariableExpression | booleanVariableExpression);
variableExpression.name("variable");
booleanConstantExpression %= (booleanConstants_ | booleanLiteralExpression);
booleanConstantExpression.name("boolean constant or literal");
integerConstantExpression %= (integerConstants_ | integerLiteralExpression);
integerConstantExpression.name("integer constant or literal");
doubleConstantExpression %= (doubleConstants_ | doubleLiteralExpression);
doubleConstantExpression.name("double constant or literal");
constantExpression %= (booleanConstantExpression | integerConstantExpression | doubleConstantExpression);
constantExpression.name("constant or literal");
atomicIntegerExpression %= (integerVariableExpression | qi::lit("(") >> integerExpression >> qi::lit(")") | integerConstantExpression);
atomicIntegerExpression.name("integer expression");
integerMultExpression %= atomicIntegerExpression[qi::_val = qi::_1] >> *(qi::lit("*") >> atomicIntegerExpression)[qi::_val = phoenix::construct<std::shared_ptr<storm::ir::expressions::BaseExpression>>(phoenix::new_<storm::ir::expressions::BinaryNumericalFunctionExpression>(qi::_val, qi::_1, storm::ir::expressions::BinaryNumericalFunctionExpression::TIMES))];
integerMultExpression.name("integer expression");
integerPlusExpression = integerMultExpression[qi::_val = qi::_1] >> *(qi::lit("+") >> integerMultExpression)[qi::_val = phoenix::construct<std::shared_ptr<storm::ir::expressions::BaseExpression>>(phoenix::new_<storm::ir::expressions::BinaryNumericalFunctionExpression>(qi::_val, qi::_1, storm::ir::expressions::BinaryNumericalFunctionExpression::PLUS))];
integerPlusExpression.name("integer expression");
integerExpression %= integerPlusExpression;
integerExpression.name("integer expression");
constantAtomicIntegerExpression %= (qi::lit("(") >> constantIntegerExpression >> qi::lit(")") | integerConstantExpression);
constantAtomicIntegerExpression.name("constant integer expression");
constantIntegerMultExpression %= constantAtomicIntegerExpression[qi::_val = qi::_1] >> *(qi::lit("*") >> constantAtomicIntegerExpression)[qi::_val = phoenix::construct<std::shared_ptr<storm::ir::expressions::BaseExpression>>(phoenix::new_<storm::ir::expressions::BinaryNumericalFunctionExpression>(qi::_val, qi::_1, storm::ir::expressions::BinaryNumericalFunctionExpression::TIMES))];
constantIntegerMultExpression.name("constant integer expression");
constantIntegerPlusExpression = constantIntegerMultExpression[qi::_val = qi::_1] >> *(qi::lit("+") >> constantIntegerMultExpression)[qi::_val = phoenix::construct<std::shared_ptr<storm::ir::expressions::BaseExpression>>(phoenix::new_<storm::ir::expressions::BinaryNumericalFunctionExpression>(qi::_val, qi::_1, storm::ir::expressions::BinaryNumericalFunctionExpression::PLUS))];
constantIntegerPlusExpression.name("constant integer expression");
constantIntegerExpression %= constantIntegerPlusExpression;
constantIntegerExpression.name("constant integer expression");
// This block defines all expressions of type double that are by syntax constant. That is, they are evaluable given the values for all constants.
constantAtomicDoubleExpression %= (qi::lit("(") >> constantDoubleExpression >> qi::lit(")") | doubleConstantExpression);
constantAtomicDoubleExpression.name("constant double expression");
constantDoubleMultExpression %= constantAtomicDoubleExpression[qi::_val = qi::_1] >> *(qi::lit("*") >> constantAtomicDoubleExpression)[qi::_val = phoenix::construct<std::shared_ptr<storm::ir::expressions::BaseExpression>>(phoenix::new_<storm::ir::expressions::BinaryNumericalFunctionExpression>(qi::_val, qi::_1, storm::ir::expressions::BinaryNumericalFunctionExpression::TIMES))];
constantDoubleMultExpression.name("constant double expression");
constantDoublePlusExpression %= constantDoubleMultExpression[qi::_val = qi::_1] >> *(qi::lit("+") >> constantDoubleMultExpression)[qi::_val = phoenix::construct<std::shared_ptr<storm::ir::expressions::BaseExpression>>(phoenix::new_<storm::ir::expressions::BinaryNumericalFunctionExpression>(qi::_val, qi::_1, storm::ir::expressions::BinaryNumericalFunctionExpression::PLUS))];
constantDoublePlusExpression.name("constant double expression");
constantDoubleExpression %= constantDoublePlusExpression;
constantDoubleExpression.name("constant double expression");
// This block defines all expressions of type boolean.
relativeExpression = (integerExpression >> relations_ >> integerExpression)[qi::_val = phoenix::construct<std::shared_ptr<storm::ir::expressions::BaseExpression>>(phoenix::new_<storm::ir::expressions::BinaryRelationExpression>(qi::_1, qi::_3, qi::_2))];
relativeExpression.name("boolean expression");
atomicBooleanExpression %= (relativeExpression | booleanVariableExpression | qi::lit("(") >> booleanExpression >> qi::lit(")") | booleanConstantExpression);
atomicBooleanExpression.name("boolean expression");
notExpression = atomicBooleanExpression[qi::_val = qi::_1] | (qi::lit("!") >> atomicBooleanExpression)[qi::_val = phoenix::construct<std::shared_ptr<storm::ir::expressions::UnaryBooleanFunctionExpression>>(phoenix::new_<storm::ir::expressions::UnaryBooleanFunctionExpression>(qi::_1, storm::ir::expressions::UnaryBooleanFunctionExpression::FunctorType::NOT))];
notExpression.name("boolean expression");
andExpression = notExpression[qi::_val = qi::_1] >> *(qi::lit("&") >> notExpression)[qi::_val = phoenix::construct<std::shared_ptr<storm::ir::expressions::BaseExpression>>(phoenix::new_<storm::ir::expressions::BinaryBooleanFunctionExpression>(qi::_val, qi::_1, storm::ir::expressions::BinaryBooleanFunctionExpression::AND))];
andExpression.name("boolean expression");
orExpression = andExpression[qi::_val = qi::_1] >> *(qi::lit("|") >> andExpression)[qi::_val = phoenix::construct<std::shared_ptr<storm::ir::expressions::BaseExpression>>(phoenix::new_<storm::ir::expressions::BinaryBooleanFunctionExpression>(qi::_val, qi::_1, storm::ir::expressions::BinaryBooleanFunctionExpression::OR))];
orExpression.name("boolean expression");
booleanExpression %= orExpression;
booleanExpression.name("boolean expression");
// This block defines all expressions of type boolean that are by syntax constant. That is, they are evaluable given the values for all constants.
constantRelativeExpression = (constantIntegerExpression >> relations_ >> constantIntegerExpression)[qi::_val = phoenix::construct<std::shared_ptr<storm::ir::expressions::BaseExpression>>(phoenix::new_<storm::ir::expressions::BinaryRelationExpression>(qi::_1, qi::_3, qi::_2))];
constantRelativeExpression.name("constant boolean expression");
constantAtomicBooleanExpression %= (constantRelativeExpression | qi::lit("(") >> constantBooleanExpression >> qi::lit(")") | booleanLiteralExpression | booleanConstantExpression);
constantAtomicBooleanExpression.name("constant boolean expression");
constantNotExpression = constantAtomicBooleanExpression[qi::_val = qi::_1] | (qi::lit("!") >> constantAtomicBooleanExpression)[qi::_val = phoenix::construct<std::shared_ptr<storm::ir::expressions::UnaryBooleanFunctionExpression>>(phoenix::new_<storm::ir::expressions::UnaryBooleanFunctionExpression>(qi::_1, storm::ir::expressions::UnaryBooleanFunctionExpression::FunctorType::NOT))];
constantNotExpression.name("constant boolean expression");
constantAndExpression = constantNotExpression[qi::_val = qi::_1] >> *(qi::lit("&") >> constantNotExpression)[qi::_val = phoenix::construct<std::shared_ptr<storm::ir::expressions::BaseExpression>>(phoenix::new_<storm::ir::expressions::BinaryBooleanFunctionExpression>(qi::_val, qi::_1, storm::ir::expressions::BinaryBooleanFunctionExpression::AND))];
constantAndExpression.name("constant boolean expression");
constantOrExpression = constantAndExpression[qi::_val = qi::_1] >> *(qi::lit("|") >> constantAndExpression)[qi::_val = phoenix::construct<std::shared_ptr<storm::ir::expressions::BaseExpression>>(phoenix::new_<storm::ir::expressions::BinaryBooleanFunctionExpression>(qi::_val, qi::_1, storm::ir::expressions::BinaryBooleanFunctionExpression::OR))];
constantOrExpression.name("constant boolean expression");
constantBooleanExpression %= constantOrExpression;
constantBooleanExpression.name("constant boolean expression");
// This block defines the general root of all expressions. Most of the time, however, you may want to start with a more specialized rule.
expression %= (booleanExpression | integerExpression | constantDoubleExpression);
expression.name("expression");
// This block defines all entities that are needed for parsing labels.
labelDefinition = (qi::lit("label") >> freeIdentifierName >> qi::lit("=") >> booleanExpression >> qi::lit(";"))[phoenix::insert(qi::_r1, phoenix::construct<std::pair<std::string, std::shared_ptr<storm::ir::expressions::BaseExpression>>>(qi::_1, qi::_2))];
labelDefinitionList %= *labelDefinition(qi::_r1);
// This block defines all entities that are needed for parsing a reward model.
stateRewardDefinition = (booleanExpression > qi::lit(":") > constantDoubleExpression >> qi::lit(";"))[qi::_val = phoenix::construct<storm::ir::StateReward>(qi::_1, qi::_2)];
stateRewardDefinition.name("state reward definition");
transitionRewardDefinition = (qi::lit("[") > -(commandName[qi::_a = qi::_1]) > qi::lit("]") > booleanExpression > qi::lit(":") > constantDoubleExpression > qi::lit(";"))[qi::_val = phoenix::construct<storm::ir::TransitionReward>(qi::_a, qi::_2, qi::_3)];
rewardDefinition = (qi::lit("rewards") > qi::lit("\"") > freeIdentifierName > qi::lit("\"") > +(stateRewardDefinition[phoenix::push_back(qi::_a, qi::_1)] | transitionRewardDefinition[phoenix::push_back(qi::_b, qi::_1)]) > qi::lit("endrewards"))[phoenix::insert(qi::_r1, phoenix::construct<std::pair<std::string, storm::ir::RewardModel>>(qi::_1, phoenix::construct<storm::ir::RewardModel>(qi::_1, qi::_a, qi::_b)))];
transitionRewardDefinition.name("transition reward definition");
rewardDefinition = (qi::lit("rewards") > qi::lit("\"") > freeIdentifierName > qi::lit("\"") > +(stateRewardDefinition[phoenix::push_back(qi::_a, qi::_1)] | transitionRewardDefinition[phoenix::push_back(qi::_b, qi::_1)]) >> qi::lit("endrewards"))[phoenix::insert(qi::_r1, phoenix::construct<std::pair<std::string, storm::ir::RewardModel>>(qi::_1, phoenix::construct<storm::ir::RewardModel>(qi::_1, qi::_a, qi::_b)))];
rewardDefinition.name("reward definition");
rewardDefinitionList = *rewardDefinition(qi::_r1);
rewardDefinitionList.name("reward definition list");
// This block defines auxiliary entities that are used to check whether a certain variable exist.
integerVariableName %= integerVariableNames_;
booleanVariableName %= booleanVariableNames_;
booleanVariableName.name("boolean variable");
integerVariableName %= integerVariableNames_;
integerVariableName.name("integer variable");
commandName %= commandNames_;
commandName.name("command name");
// This block defines all entities that are needed for parsing a single command.
assignmentDefinition = (qi::lit("(") >> integerVariableName > qi::lit("'") > qi::lit("=") > integerExpression > qi::lit(")"))[qi::_val = phoenix::construct<storm::ir::Assignment>(qi::_1, qi::_2)] | (qi::lit("(") > booleanVariableName > qi::lit("'") > qi::lit("=") > booleanExpression > qi::lit(")"))[qi::_val = phoenix::construct<storm::ir::Assignment>(qi::_1, qi::_2)];
assignmentDefinition.name("assignment");
assignmentDefinitionList %= assignmentDefinition % "&";
assignmentDefinitionList.name("assignment list");
updateDefinition = (constantDoubleExpression > qi::lit(":") > assignmentDefinitionList)[qi::_val = phoenix::construct<storm::ir::Update>(qi::_1, qi::_2)];
updateDefinition.name("update");
updateListDefinition = +updateDefinition % "+";
updateListDefinition.name("update list");
commandDefinition = (qi::lit("[") > -((freeIdentifierName[phoenix::bind(commandNames_.add, qi::_1, qi::_1)] | commandName)[qi::_a = qi::_1]) > qi::lit("]") > booleanExpression > qi::lit("->") > updateListDefinition > qi::lit(";"))[qi::_val = phoenix::construct<storm::ir::Command>(qi::_a, qi::_2, qi::_3)];
commandDefinition.name("command");
// This block defines all entities that are neede for parsing variable definitions.
booleanVariableDefinition = (freeIdentifierName >> qi::lit(":") >> qi::lit("bool") > -(qi::lit("init") > constantBooleanExpression[qi::_b = phoenix::construct<std::shared_ptr<storm::ir::expressions::BaseExpression>>(qi::_1)]) > qi::lit(";"))[qi::_val = phoenix::construct<storm::ir::BooleanVariable>(qi::_1, qi::_b), qi::_a = phoenix::construct<std::shared_ptr<storm::ir::expressions::VariableExpression>>(phoenix::new_<storm::ir::expressions::VariableExpression>(qi::_1)), phoenix::bind(booleanVariables_.add, qi::_1, qi::_a), phoenix::bind(booleanVariableNames_.add, qi::_1, qi::_1), phoenix::bind(allVariables_.add, qi::_1, qi::_a), phoenix::bind(booleanVariableInfo_.add, qi::_1, qi::_val)];
integerVariableDefinition = (freeIdentifierName > qi::lit(":") > qi::lit("[") > constantIntegerExpression > qi::lit("..") > constantIntegerExpression > qi::lit("]") > -(qi::lit("init") > constantIntegerExpression[qi::_b = phoenix::construct<std::shared_ptr<storm::ir::expressions::BaseExpression>>(qi::_1)]) > qi::lit(";"))[qi::_val = phoenix::construct<storm::ir::IntegerVariable>(qi::_1, qi::_2, qi::_3, qi::_b), qi::_a = phoenix::construct<std::shared_ptr<storm::ir::expressions::VariableExpression>>(phoenix::new_<storm::ir::expressions::VariableExpression>(qi::_1)), phoenix::bind(integerVariables_.add, qi::_1, qi::_a), phoenix::bind(integerVariableNames_.add, qi::_1, qi::_1), phoenix::bind(allVariables_.add, qi::_1, qi::_a), phoenix::bind(integerVariableInfo_.add, qi::_1, qi::_val)];
booleanVariableDefinition = (freeIdentifierName >> qi::lit(":") >> qi::lit("bool") > -(qi::lit("init") > constantBooleanExpression[qi::_b = phoenix::construct<std::shared_ptr<storm::ir::expressions::BaseExpression>>(qi::_1)]) > qi::lit(";"))[qi::_val = phoenix::construct<storm::ir::BooleanVariable>(phoenix::val("hallo"), qi::_b), qi::_a = phoenix::construct<std::shared_ptr<storm::ir::expressions::VariableExpression>>(phoenix::new_<storm::ir::expressions::VariableExpression>(qi::_1)), std::cout << phoenix::val("here!"), phoenix::bind(booleanVariables_.add, qi::_1, qi::_a), phoenix::bind(booleanVariableNames_.add, qi::_1, qi::_1)];
booleanVariableDefinition.name("boolean variable declaration");
integerVariableDefinition = (freeIdentifierName > qi::lit(":") > qi::lit("[") > constantIntegerExpression > qi::lit("..") > constantIntegerExpression > qi::lit("]") > -(qi::lit("init") > constantIntegerExpression[qi::_b = phoenix::construct<std::shared_ptr<storm::ir::expressions::BaseExpression>>(qi::_1)]) > qi::lit(";"))[qi::_val = phoenix::construct<storm::ir::IntegerVariable>(qi::_1, qi::_2, qi::_3, qi::_b), qi::_a = phoenix::construct<std::shared_ptr<storm::ir::expressions::VariableExpression>>(phoenix::new_<storm::ir::expressions::VariableExpression>(qi::_1)), phoenix::bind(integerVariables_.add, qi::_1, qi::_a), phoenix::bind(integerVariableNames_.add, qi::_1, qi::_1)];
integerVariableDefinition.name("integer variable declaration");
variableDefinition = (booleanVariableDefinition | integerVariableDefinition);
variableDefinition.name("variable declaration");
// This block defines all entities that are needed for parsing a module.
moduleDefinition = (qi::lit("module") > freeIdentifierName > *(booleanVariableDefinition[phoenix::push_back(qi::_a, qi::_1)] | integerVariableDefinition[phoenix::push_back(qi::_b, qi::_1)]) > +commandDefinition > qi::lit("endmodule"))[qi::_val = phoenix::construct<storm::ir::Module>(qi::_1, qi::_a, qi::_b, qi::_3)];
moduleDefinition.name("module");
moduleDefinitionList %= +moduleDefinition;
moduleDefinitionList.name("module list");
// This block defines all entities that are needed for parsing constant definitions.
definedBooleanConstantDefinition = (qi::lit("const") >> qi::lit("bool") >> freeIdentifierName >> qi::lit("=") > booleanLiteralExpression > qi::lit(";"))[phoenix::bind(booleanConstants_.add, qi::_1, qi::_2), phoenix::bind(allConstants_.add, qi::_1, qi::_2), qi::_val = qi::_2];
definedBooleanConstantDefinition.name("defined boolean constant declaration");
definedIntegerConstantDefinition = (qi::lit("const") >> qi::lit("int") >> freeIdentifierName >> qi::lit("=") > integerLiteralExpression > qi::lit(";"))[phoenix::bind(integerConstants_.add, qi::_1, qi::_2), phoenix::bind(allConstants_.add, qi::_1, qi::_2), qi::_val = qi::_2];
definedIntegerConstantDefinition.name("defined integer constant declaration");
definedDoubleConstantDefinition = (qi::lit("const") >> qi::lit("double") >> freeIdentifierName >> qi::lit("=") > doubleLiteralExpression > qi::lit(";"))[phoenix::bind(doubleConstants_.add, qi::_1, qi::_2), phoenix::bind(allConstants_.add, qi::_1, qi::_2), qi::_val = qi::_2];
definedDoubleConstantDefinition.name("defined double constant declaration");
undefinedBooleanConstantDefinition = (qi::lit("const") >> qi::lit("bool") > freeIdentifierName > qi::lit(";"))[qi::_a = phoenix::construct<std::shared_ptr<storm::ir::expressions::BooleanConstantExpression>>(phoenix::new_<storm::ir::expressions::BooleanConstantExpression>(qi::_1)), phoenix::insert(qi::_r1, phoenix::construct<std::pair<std::string, std::shared_ptr<storm::ir::expressions::BooleanConstantExpression>>>(qi::_1, qi::_a)), phoenix::bind(booleanConstantInfo_.add, qi::_1, qi::_a), phoenix::bind(booleanConstants_.add, qi::_1, qi::_a), phoenix::bind(allConstants_.add, qi::_1, qi::_a)];
undefinedBooleanConstantDefinition.name("undefined boolean constant declaration");
undefinedIntegerConstantDefinition = (qi::lit("const") >> qi::lit("int") > freeIdentifierName > qi::lit(";"))[qi::_a = phoenix::construct<std::shared_ptr<storm::ir::expressions::IntegerConstantExpression>>(phoenix::new_<storm::ir::expressions::IntegerConstantExpression>(qi::_1)), phoenix::insert(qi::_r1, phoenix::construct<std::pair<std::string, std::shared_ptr<storm::ir::expressions::IntegerConstantExpression>>>(qi::_1, qi::_a)), phoenix::bind(integerConstantInfo_.add, qi::_1, qi::_a), phoenix::bind(integerConstants_.add, qi::_1, qi::_a), phoenix::bind(allConstants_.add, qi::_1, qi::_a)];
undefinedIntegerConstantDefinition.name("undefined integer constant declaration");
undefinedDoubleConstantDefinition = (qi::lit("const") >> qi::lit("double") > freeIdentifierName > qi::lit(";"))[qi::_a = phoenix::construct<std::shared_ptr<storm::ir::expressions::DoubleConstantExpression>>(phoenix::new_<storm::ir::expressions::DoubleConstantExpression>(qi::_1)), phoenix::insert(qi::_r1, phoenix::construct<std::pair<std::string, std::shared_ptr<storm::ir::expressions::DoubleConstantExpression>>>(qi::_1, qi::_a)), phoenix::bind(doubleConstantInfo_.add, qi::_1, qi::_a), phoenix::bind(doubleConstants_.add, qi::_1, qi::_a), phoenix::bind(allConstants_.add, qi::_1, qi::_a)];
undefinedDoubleConstantDefinition.name("undefined double constant declaration");
definedConstantDefinition %= (definedBooleanConstantDefinition | definedIntegerConstantDefinition | definedDoubleConstantDefinition);
definedConstantDefinition.name("defined constant declaration");
undefinedConstantDefinition = (undefinedBooleanConstantDefinition(qi::_r1) | undefinedIntegerConstantDefinition(qi::_r2) | undefinedDoubleConstantDefinition(qi::_r3));
undefinedConstantDefinition.name("undefined constant declaration");
constantDefinitionList = *(definedConstantDefinition | undefinedConstantDefinition(qi::_r1, qi::_r2, qi::_r3));
constantDefinitionList.name("constant declaration list");
// This block defines all entities that are needed for parsing a program.
modelTypeDefinition = modelType_;
start = (modelTypeDefinition > constantDefinitionList(qi::_a, qi::_b, qi::_c) > moduleDefinitionList > rewardDefinitionList(qi::_d))[qi::_val = phoenix::construct<storm::ir::Program>(qi::_1, qi::_a, qi::_b, qi::_c, qi::_2, qi::_d)];
modelTypeDefinition.name("model type");
start = (modelTypeDefinition > constantDefinitionList(qi::_a, qi::_b, qi::_c) > moduleDefinitionList > rewardDefinitionList(qi::_d) > labelDefinitionList(qi::_e))[qi::_val = phoenix::construct<storm::ir::Program>(qi::_1, qi::_a, qi::_b, qi::_c, qi::_2, qi::_d, qi::_e)];
start.name("probabilistic program declaration");
}
// The starting point of the grammar.
qi::rule<Iterator, storm::ir::Program(), qi::locals<std::map<std::string, std::shared_ptr<storm::ir::expressions::BooleanConstantExpression>>, std::map<std::string, std::shared_ptr<storm::ir::expressions::IntegerConstantExpression>>, std::map<std::string, std::shared_ptr<storm::ir::expressions::DoubleConstantExpression>>, std::map<std::string, storm::ir::RewardModel>>, Skipper> start;
qi::rule<Iterator, storm::ir::Program(), qi::locals<std::map<std::string, std::shared_ptr<storm::ir::expressions::BooleanConstantExpression>>, std::map<std::string, std::shared_ptr<storm::ir::expressions::IntegerConstantExpression>>, std::map<std::string, std::shared_ptr<storm::ir::expressions::DoubleConstantExpression>>, std::map<std::string, storm::ir::RewardModel>, std::map<std::string, std::shared_ptr<storm::ir::expressions::BaseExpression>>>, Skipper> start;
qi::rule<Iterator, storm::ir::Program::ModelType(), Skipper> modelTypeDefinition;
qi::rule<Iterator, qi::unused_type(std::map<std::string, std::shared_ptr<storm::ir::expressions::BooleanConstantExpression>>&, std::map<std::string, std::shared_ptr<storm::ir::expressions::IntegerConstantExpression>>&, std::map<std::string, std::shared_ptr<storm::ir::expressions::DoubleConstantExpression>>&), Skipper> constantDefinitionList;
qi::rule<Iterator, std::vector<storm::ir::Module>(), Skipper> moduleDefinitionList;
@ -192,6 +272,9 @@ private:
qi::rule<Iterator, storm::ir::StateReward(), Skipper> stateRewardDefinition;
qi::rule<Iterator, storm::ir::TransitionReward(), qi::locals<std::string>, Skipper> transitionRewardDefinition;
qi::rule<Iterator, qi::unused_type(std::map<std::string, std::shared_ptr<storm::ir::expressions::BaseExpression>>&), Skipper> labelDefinitionList;
qi::rule<Iterator, qi::unused_type(std::map<std::string, std::shared_ptr<storm::ir::expressions::BaseExpression>>&), Skipper> labelDefinition;
qi::rule<Iterator, std::shared_ptr<storm::ir::expressions::BaseExpression>(), Skipper> constantDefinition;
qi::rule<Iterator, qi::unused_type(std::map<std::string, std::shared_ptr<storm::ir::expressions::BooleanConstantExpression>>&, std::map<std::string, std::shared_ptr<storm::ir::expressions::IntegerConstantExpression>>&, std::map<std::string, std::shared_ptr<storm::ir::expressions::DoubleConstantExpression>>&), Skipper> undefinedConstantDefinition;
qi::rule<Iterator, std::shared_ptr<storm::ir::expressions::BaseExpression>(), Skipper> definedConstantDefinition;
@ -203,6 +286,7 @@ private:
qi::rule<Iterator, std::shared_ptr<storm::ir::expressions::BaseExpression>(), Skipper> definedDoubleConstantDefinition;
qi::rule<Iterator, std::string(), Skipper> freeIdentifierName;
qi::rule<Iterator, std::string(), Skipper> identifierName;
// The starting point for arbitrary expressions.
qi::rule<Iterator, std::shared_ptr<storm::ir::expressions::BaseExpression>(), Skipper> expression;
@ -299,20 +383,12 @@ private:
struct variablesStruct : qi::symbols<char, std::shared_ptr<storm::ir::expressions::BaseExpression>> {
// Intentionally left empty. This map is filled during parsing.
} integerVariables_, booleanVariables_, allVariables_;
} integerVariables_, booleanVariables_;
struct entityNamesStruct : qi::symbols<char, std::string> {
// Intentionally left empty. This map is filled during parsing.
} integerVariableNames_, booleanVariableNames_, commandNames_;
struct booleanVariableTypesStruct : qi::symbols<char, storm::ir::BooleanVariable> {
// Intentionally left empty. This map is filled during parsing.
} booleanVariableInfo_;
struct integerVariableTypesStruct : qi::symbols<char, storm::ir::IntegerVariable> {
// Intentionally left empty. This map is filled during parsing.
} integerVariableInfo_;
struct constantsStruct : qi::symbols<char, std::shared_ptr<storm::ir::expressions::BaseExpression>> {
// Intentionally left empty. This map is filled during parsing.
} integerConstants_, booleanConstants_, doubleConstants_, allConstants_;

8
test.input
View File

@ -1,11 +1,6 @@
dtmc
const bool sic;
const int i;
const double e;
module die
// local state
s : [0..7] init 0;
// value of the dice
@ -19,10 +14,11 @@ d : [0..6] init 0;
[] s=5 -> 0.5 : (s'=7) & (d'=4) + 0.5 : (s'=7) & (d'=5);
[] s=6 -> 0.5 : (s'=2) + 0.5 : (s'=7) & (d'=6);
[] s=7 -> 1 : (s'=7);
endmodule
rewards "coin_flips"
[] s<7 : 1;
s>3 : 1;
endrewards
label test = s>2;
Write Preview
Loading…
Cancel
Save