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

added parser tests for mdp shields MdpShieldingParserTest.cpp

main
Lukas Posch 4 years ago
committed by Stefan Pranger
parent
45e660fe9b
commit
cdc0fd2873
1 changed files with 72 additions and 0 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. 72
      src/test/storm/parser/MdpShieldingParserTest.cpp

72
src/test/storm/parser/MdpShieldingParserTest.cpp
View File

@ -0,0 +1,72 @@
#include "test/storm_gtest.h"
#include "storm-parsers/parser/FormulaParser.h"
#include "storm/logic/FragmentSpecification.h"
#include "storm/storage/expressions/ExpressionManager.h"
TEST(MdpShieldingParserTest, PreSafetyShieldTest) {
storm::parser::FormulaParser formulaParser;
std::string filename = "preSafetyShieldFileName";
std::string value = "0.6667";
std::string input = "<" + filename + ", PreSafety, gamma=" + value + "> Pmax=? [F \"label\"]";
std::shared_ptr<storm::logic::Formula const> formula(nullptr);
std::vector<storm::jani::Property> property;
ASSERT_NO_THROW(property = formulaParser.parseFromString(input));
EXPECT_TRUE(property.at(0).isShieldingProperty());
std::shared_ptr<storm::logic::ShieldExpression const> shieldExpression(nullptr);
ASSERT_NO_THROW(shieldExpression = property.at(0).getShieldingExpression());
EXPECT_TRUE(shieldExpression->isPreSafetyShield());
EXPECT_FALSE(shieldExpression->isPostSafetyShield());
EXPECT_FALSE(shieldExpression->isOptimalShield());
EXPECT_FALSE(shieldExpression->isRelative());
EXPECT_EQ(std::stod(value), shieldExpression->getValue());
EXPECT_EQ(filename, shieldExpression->getFilename());
}
TEST(MdpShieldingParserTest, PostSafetyShieldTest) {
storm::parser::FormulaParser formulaParser;
std::string filename = "postSafetyShieldFileName";
std::string value = "0.95";
std::string input = "<" + filename + ", PostSafety, lambda=" + value + "> Pmin=? [X !\"label\"]";
std::shared_ptr<storm::logic::Formula const> formula(nullptr);
std::vector<storm::jani::Property> property;
ASSERT_NO_THROW(property = formulaParser.parseFromString(input));
EXPECT_TRUE(property.at(0).isShieldingProperty());
std::shared_ptr<storm::logic::ShieldExpression const> shieldExpression(nullptr);
ASSERT_NO_THROW(shieldExpression = property.at(0).getShieldingExpression());
EXPECT_FALSE(shieldExpression->isPreSafetyShield());
EXPECT_TRUE(shieldExpression->isPostSafetyShield());
EXPECT_FALSE(shieldExpression->isOptimalShield());
EXPECT_TRUE(shieldExpression->isRelative());
EXPECT_EQ(std::stod(value), shieldExpression->getValue());
EXPECT_EQ(filename, shieldExpression->getFilename());
}
TEST(MdpShieldingParserTest, OptimalShieldTest) {
std::shared_ptr<storm::expressions::ExpressionManager> manager(new storm::expressions::ExpressionManager());
manager->declareBooleanVariable("a");
manager->declareIntegerVariable("x");
storm::parser::FormulaParser formulaParser(manager);
std::string filename = "optimalShieldFileName";
std::string input = "<" + filename + ", Optimal> Pmax=? [G (a|x>3)]";
std::shared_ptr<storm::logic::Formula const> formula(nullptr);
std::vector<storm::jani::Property> property;
ASSERT_NO_THROW(property = formulaParser.parseFromString(input));
EXPECT_TRUE(property.at(0).isShieldingProperty());
std::shared_ptr<storm::logic::ShieldExpression const> shieldExpression(nullptr);
ASSERT_NO_THROW(shieldExpression = property.at(0).getShieldingExpression());
EXPECT_FALSE(shieldExpression->isPreSafetyShield());
EXPECT_FALSE(shieldExpression->isPostSafetyShield());
EXPECT_TRUE(shieldExpression->isOptimalShield());
EXPECT_FALSE(shieldExpression->isRelative());
EXPECT_EQ(filename, shieldExpression->getFilename());
}
Write Preview
Loading…
Cancel
Save