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

Finished unit tests for the actions. 

Next up: Update the parser tests.


Former-commit-id: c0db7bd1d4
tempestpy_adaptions
masawei 11 years ago
parent
ee1ebdf91d
commit
2c59dd6f32
3 changed files with 369 additions and 10 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. 6
      src/formula/actions/RangeAction.h
  2. 8
      src/formula/actions/SortAction.h
  3. 365
      test/functional/parser/ActionTest.cpp

6
src/formula/actions/RangeAction.h
View File

@ -26,11 +26,11 @@ public:
}
/*!
* Excluding the state with position to.
* Including the state with position to.
*/
RangeAction(uint_fast64_t from, uint_fast64_t to) : from(from), to(to) {
if(from > to) {
throw storm::exceptions::IllegalArgumentException() << "The end of the range is lower than its beginning";
throw storm::exceptions::IllegalArgumentValueException() << "The end of the range is lower than its beginning";
}
}
@ -103,7 +103,7 @@ private:
}
//Fill the output vector.
for(uint_fast64_t i=0; i < end; i++) {
for(uint_fast64_t i=0; i <= end; i++) {
out.set(result.stateMap[from + i], result.selection[result.stateMap[from + i]]);
}

8
src/formula/actions/SortAction.h
View File

@ -137,9 +137,9 @@ private:
// Sort the state map.
if(ascending) {
std::sort(outMap.begin(), outMap.end(), [&] (uint_fast64_t a, uint_fast64_t b) -> bool { return values[a] <= values[b]; });
std::sort(outMap.begin(), outMap.end(), [&] (uint_fast64_t a, uint_fast64_t b) -> bool { return values[a] == values[b] ? a < b : values[a] < values[b]; });
} else {
std::sort(outMap.begin(), outMap.end(), [&] (uint_fast64_t a, uint_fast64_t b) -> bool { return values[a] >= values[b]; });
std::sort(outMap.begin(), outMap.end(), [&] (uint_fast64_t a, uint_fast64_t b) -> bool { return values[a] == values[b] ? a < b : values[a] > values[b]; });
}
return outMap;
@ -155,9 +155,9 @@ private:
// Sort the state map.
if(ascending) {
std::sort(outMap.begin(), outMap.end(), [&] (uint_fast64_t a, uint_fast64_t b) -> bool { return values[a] <= values[b]; });
std::sort(outMap.begin(), outMap.end(), [&] (uint_fast64_t a, uint_fast64_t b) -> bool { return values[a] == values[b] ? a < b : values[a] < values[b]; });
} else {
std::sort(outMap.begin(), outMap.end(), [&] (uint_fast64_t a, uint_fast64_t b) -> bool { return values[a] >= values[b]; });
std::sort(outMap.begin(), outMap.end(), [&] (uint_fast64_t a, uint_fast64_t b) -> bool { return values[a] == values[b] ? a < b : values[a] > values[b]; });
}
return outMap;

365
test/functional/parser/ActionTest.cpp
View File

@ -10,6 +10,9 @@
#include "src/formula/actions/BoundAction.h"
#include "src/formula/actions/FormulaAction.h"
#include "src/formula/actions/InvertAction.h"
#include "src/formula/actions/RangeAction.h"
#include "src/formula/actions/SortAction.h"
#include "src/parser/MarkovAutomatonParser.h"
#include "src/parser/DeterministicModelParser.h"
@ -175,6 +178,7 @@ TEST(ActionTest, FormulaActionFunctionality) {
// Build the filter input.
// Basically the modelchecking result of "F a" on the used DTMC.
std::vector<double> pathResult = mc.checkEventually(storm::property::prctl::Eventually<double>(std::make_shared<storm::property::prctl::Ap<double>>("a")), false);
storm::storage::BitVector stateResult = mc.checkAp(storm::property::prctl::Ap<double>("c"));
std::vector<uint_fast64_t> stateMap(pathResult.size());
for(uint_fast64_t i = 0; i < pathResult.size(); i++) {
stateMap[i] = i;
@ -193,13 +197,13 @@ TEST(ActionTest, FormulaActionFunctionality) {
} else {
ASSERT_FALSE(result.selection[i]);
}
ASSERT_EQ(i, stateMap[i]);
ASSERT_EQ(input.pathResult, result.pathResult);
ASSERT_EQ(i, result.stateMap[i]);
ASSERT_EQ(input.pathResult[i], result.pathResult[i]);
}
ASSERT_TRUE(result.stateResult.size() == 0);
input.selection.set(0,true);
// Now test the general functionality for both results of path and state formulas.
// Now test the general functionality.
action = storm::property::action::FormulaAction<double>(std::make_shared<storm::property::prctl::ProbabilisticBoundOperator<double>>(storm::property::LESS, 0.5, std::make_shared<storm::property::prctl::Eventually<double>>(std::make_shared<storm::property::prctl::Ap<double>>("b"))));
ASSERT_NO_THROW(result = action.evaluate(input, mc));
ASSERT_TRUE(result.selection[0]);
@ -211,4 +215,359 @@ TEST(ActionTest, FormulaActionFunctionality) {
ASSERT_FALSE(result.selection[6]);
ASSERT_FALSE(result.selection[7]);
// Check that the actual modelchecking results are not touched.
ASSERT_EQ(input.stateResult.size(), result.stateResult.size());
ASSERT_EQ(input.pathResult.size(), result.pathResult.size());
for(uint_fast64_t i = 0; i < input.pathResult.size(); i++) {
ASSERT_EQ(input.pathResult[i], result.pathResult[i]);
}
// Do the same but this time using a state result instead of a path result.
input.pathResult = std::vector<double>();
input.stateResult = stateResult;
ASSERT_NO_THROW(result = action.evaluate(input, mc));
ASSERT_TRUE(result.selection[0]);
ASSERT_TRUE(result.selection[1]);
ASSERT_TRUE(result.selection[2]);
ASSERT_FALSE(result.selection[3]);
ASSERT_FALSE(result.selection[4]);
ASSERT_TRUE(result.selection[5]);
ASSERT_FALSE(result.selection[6]);
ASSERT_FALSE(result.selection[7]);
ASSERT_EQ(input.stateResult.size(), result.stateResult.size());
ASSERT_EQ(input.pathResult.size(), result.pathResult.size());
for(uint_fast64_t i = 0; i < input.stateResult.size(); i++) {
ASSERT_EQ(input.stateResult[i], result.stateResult[i]);
}
}
TEST(ActionTest, FormulaActionSafety){
// Setup the modelchecker.
storm::models::Dtmc<double> model = storm::parser::DeterministicModelParser::parseDtmc(STORM_CPP_TESTS_BASE_PATH "/functional/parser/tra_files/dtmc_actionTest.tra", STORM_CPP_TESTS_BASE_PATH "/functional/parser/lab_files/dtmc_actionTest.lab");
storm::modelchecker::prctl::SparseDtmcPrctlModelChecker<double> mc(model, new storm::solver::GmmxxLinearEquationSolver<double>());
// Build the filter input.
// Basically the modelchecking result of "F a" on the used DTMC.
std::vector<double> pathResult = mc.checkEventually(storm::property::prctl::Eventually<double>(std::make_shared<storm::property::prctl::Ap<double>>("a")), false);
std::vector<uint_fast64_t> stateMap(pathResult.size());
for(uint_fast64_t i = 0; i < pathResult.size(); i++) {
stateMap[i] = i;
}
Result input(storm::storage::BitVector(pathResult.size(), true), stateMap, pathResult, storm::storage::BitVector());
Result result;
// Check that constructing the action using a nullptr and using an empty constructor leads to the same behavior.
storm::property::action::FormulaAction<double> action(std::shared_ptr<storm::property::csl::AbstractStateFormula<double>>(nullptr));
input.selection.set(0,false);
ASSERT_NO_THROW(result = action.evaluate(input, mc));
for(uint_fast64_t i = 0; i < pathResult.size(); i++) {
if(i != 0) {
ASSERT_TRUE(result.selection[i]);
} else {
ASSERT_FALSE(result.selection[i]);
}
ASSERT_EQ(i, result.stateMap[i]);
ASSERT_EQ(input.pathResult[i], result.pathResult[i]);
}
ASSERT_TRUE(result.stateResult.size() == 0);
input.selection.set(0,true);
ASSERT_NO_THROW(action.toString());
}
TEST(ActionTest, InvertActionFunctionality){
// Setup the modelchecker.
storm::models::Dtmc<double> model = storm::parser::DeterministicModelParser::parseDtmc(STORM_CPP_TESTS_BASE_PATH "/functional/parser/tra_files/dtmc_actionTest.tra", STORM_CPP_TESTS_BASE_PATH "/functional/parser/lab_files/dtmc_actionTest.lab");
storm::modelchecker::prctl::SparseDtmcPrctlModelChecker<double> mc(model, new storm::solver::GmmxxLinearEquationSolver<double>());
// Build the filter input.
// Basically the modelchecking result of "F a" on the used DTMC.
std::vector<double> pathResult = mc.checkEventually(storm::property::prctl::Eventually<double>(std::make_shared<storm::property::prctl::Ap<double>>("a")), false);
storm::storage::BitVector stateResult = mc.checkAp(storm::property::prctl::Ap<double>("c"));
std::vector<uint_fast64_t> stateMap(pathResult.size());
for(uint_fast64_t i = 0; i < pathResult.size(); i++) {
stateMap[i] = pathResult.size()-i-1;
}
Result input(storm::storage::BitVector(pathResult.size(), true), stateMap, pathResult, storm::storage::BitVector());
Result result;
// Check whether the selection becomes inverted while the rest stays the same.
storm::property::action::InvertAction<double> action;
input.selection.set(0,false);
ASSERT_NO_THROW(result = action.evaluate(input, mc));
for(uint_fast64_t i = 0; i < pathResult.size(); i++) {
if(i != 0) {
ASSERT_FALSE(result.selection[i]);
} else {
ASSERT_TRUE(result.selection[i]);
}
ASSERT_EQ(pathResult.size()-i-1, result.stateMap[i]);
ASSERT_EQ(input.pathResult[i], result.pathResult[i]);
}
ASSERT_TRUE(result.stateResult.size() == 0);
input.selection.set(0,true);
ASSERT_NO_THROW(action.toString());
}
TEST(ActionTest, RangeActionFunctionality){
// Setup the modelchecker.
storm::models::Dtmc<double> model = storm::parser::DeterministicModelParser::parseDtmc(STORM_CPP_TESTS_BASE_PATH "/functional/parser/tra_files/dtmc_actionTest.tra", STORM_CPP_TESTS_BASE_PATH "/functional/parser/lab_files/dtmc_actionTest.lab");
storm::modelchecker::prctl::SparseDtmcPrctlModelChecker<double> mc(model, new storm::solver::GmmxxLinearEquationSolver<double>());
// Build the filter input.
// Basically the modelchecking result of "F a" on the used DTMC.
std::vector<double> pathResult = mc.checkEventually(storm::property::prctl::Eventually<double>(std::make_shared<storm::property::prctl::Ap<double>>("a")), false);
storm::storage::BitVector stateResult = mc.checkAp(storm::property::prctl::Ap<double>("c"));
std::vector<uint_fast64_t> stateMap(pathResult.size());
for(uint_fast64_t i = 0; i < pathResult.size(); i++) {
stateMap[i] = i;
}
Result input(storm::storage::BitVector(pathResult.size(), true), stateMap, pathResult, storm::storage::BitVector());
Result result;
// Test if the action selects the first 3 states in relation to the order given by the stateMap.
// First in index order.
storm::property::action::RangeAction<double> action(0,2);
ASSERT_NO_THROW(result = action.evaluate(input, mc));
for(uint_fast64_t i = 0; i < result.selection.size(); i++) {
ASSERT_EQ(input.stateMap[i], result.stateMap[i]);
}
for(uint_fast64_t i = 0; i < 3; i++) {
ASSERT_TRUE(result.selection[i]);
}
for(uint_fast64_t i = 3; i < result.selection.size(); i++) {
ASSERT_FALSE(result.selection[i]);
}
input.selection.clear();
input.selection.complement();
// Now against index order.
for(uint_fast64_t i = 0; i < input.pathResult.size(); i++) {
input.stateMap[i] = input.pathResult.size()-i-1;
}
ASSERT_NO_THROW(result = action.evaluate(input, mc));
for(uint_fast64_t i = 0; i < result.selection.size(); i++) {
ASSERT_EQ(input.stateMap[i], result.stateMap[i]);
}
for(uint_fast64_t i = 0; i < 3; i++) {
ASSERT_TRUE(result.selection[result.selection.size()-i-1]);
}
for(uint_fast64_t i = 3; i < result.selection.size(); i++) {
ASSERT_FALSE(result.selection[result.selection.size()-i-1]);
}
input.selection.clear();
input.selection.complement();
// Finally test a random order.
std::srand(time(nullptr));
uint_fast64_t pos1, pos2, temp;
for(uint_fast64_t i = 0; i < 100; i++) {
// Randomly select two positions.
pos1 = rand() % result.selection.size();
pos2 = rand() % result.selection.size();
// Swap the values there.
temp = input.stateMap[pos1];
input.stateMap[pos1] = input.stateMap[pos2];
input.stateMap[pos2] = temp;
}
ASSERT_NO_THROW(result = action.evaluate(input, mc));
for(uint_fast64_t i = 0; i < 8; i++) {
ASSERT_EQ(input.stateMap[i], result.stateMap[i]);
}
for(uint_fast64_t i = 0; i < 3; i++) {
ASSERT_TRUE(result.selection[result.stateMap[i]]);
}
for(uint_fast64_t i = 3; i < result.selection.size(); i++) {
ASSERT_FALSE(result.selection[result.stateMap[i]]);
}
// Test that specifying and interval of (i,i) selects only state i.
for(uint_fast64_t i = 0; i < input.selection.size(); i++) {
action = storm::property::action::RangeAction<double>(i,i);
ASSERT_NO_THROW(result = action.evaluate(input, mc));
ASSERT_EQ(1, result.selection.getNumberOfSetBits());
ASSERT_TRUE(result.selection[result.stateMap[i]]);
}
}
TEST(ActionTest, RangeActionSafety){
// Setup the modelchecker.
storm::models::Dtmc<double> model = storm::parser::DeterministicModelParser::parseDtmc(STORM_CPP_TESTS_BASE_PATH "/functional/parser/tra_files/dtmc_actionTest.tra", STORM_CPP_TESTS_BASE_PATH "/functional/parser/lab_files/dtmc_actionTest.lab");
storm::modelchecker::prctl::SparseDtmcPrctlModelChecker<double> mc(model, new storm::solver::GmmxxLinearEquationSolver<double>());
// Build the filter input.
// Basically the modelchecking result of "F a" on the used DTMC.
std::vector<double> pathResult = mc.checkEventually(storm::property::prctl::Eventually<double>(std::make_shared<storm::property::prctl::Ap<double>>("a")), false);
storm::storage::BitVector stateResult = mc.checkAp(storm::property::prctl::Ap<double>("c"));
std::vector<uint_fast64_t> stateMap(pathResult.size());
for(uint_fast64_t i = 0; i < pathResult.size(); i++) {
stateMap[i] = i;
}
Result input(storm::storage::BitVector(pathResult.size(), true), stateMap, pathResult, storm::storage::BitVector());
Result result;
// Test invalid ranges.
// To capture the warning, redirect cout and test the written buffer content.
std::stringstream buffer;
std::streambuf * sbuf = std::cout.rdbuf();
std::cout.rdbuf(buffer.rdbuf());
storm::property::action::RangeAction<double> action(0,42);
ASSERT_NO_THROW(result = action.evaluate(input, mc));
ASSERT_TRUE(result.selection.full());
ASSERT_FALSE(buffer.str().empty());
buffer.str("");
action = storm::property::action::RangeAction<double>(42,98);
ASSERT_NO_THROW(result = action.evaluate(input, mc));
ASSERT_TRUE(result.selection.empty());
ASSERT_FALSE(buffer.str().empty());
std::cout.rdbuf(sbuf);
ASSERT_THROW(storm::property::action::RangeAction<double>(3,1), storm::exceptions::IllegalArgumentValueException);
}
TEST(ActionTest, SortActionFunctionality){
// Setup the modelchecker.
storm::models::Dtmc<double> model = storm::parser::DeterministicModelParser::parseDtmc(STORM_CPP_TESTS_BASE_PATH "/functional/parser/tra_files/dtmc_actionTest.tra", STORM_CPP_TESTS_BASE_PATH "/functional/parser/lab_files/dtmc_actionTest.lab");
storm::modelchecker::prctl::SparseDtmcPrctlModelChecker<double> mc(model, new storm::solver::GmmxxLinearEquationSolver<double>());
// Build the filter input.
// Basically the modelchecking result of "F a" on the used DTMC.
std::vector<double> pathResult = mc.checkEventually(storm::property::prctl::Eventually<double>(std::make_shared<storm::property::prctl::Ap<double>>("a")), false);
storm::storage::BitVector stateResult = mc.checkAp(storm::property::prctl::Ap<double>("c"));
std::vector<uint_fast64_t> stateMap(pathResult.size());
for(uint_fast64_t i = 0; i < pathResult.size(); i++) {
stateMap[i] = pathResult.size()-i-1;
}
Result input(storm::storage::BitVector(pathResult.size(), true), stateMap, pathResult, storm::storage::BitVector());
Result result;
// Test that sorting preserves everything except the state map.
storm::property::action::SortAction<double> action;
ASSERT_NO_THROW(action.toString());
input.selection.set(0,false);
ASSERT_NO_THROW(result = action.evaluate(input, mc));
for(uint_fast64_t i = 0; i < pathResult.size(); i++) {
if(i != 0) {
ASSERT_TRUE(result.selection[i]);
} else {
ASSERT_FALSE(result.selection[i]);
}
ASSERT_EQ(i, result.stateMap[i]);
ASSERT_EQ(input.pathResult[i], result.pathResult[i]);
}
ASSERT_TRUE(result.stateResult.size() == 0);
input.selection.set(0,true);
// Test sorting cases. Note that the input selection should be irrelevant for the resulting state order.
// 1) index, ascending -> see above
// 2) index descending
input.selection.set(3,false);
action = storm::property::action::SortAction<double>(storm::property::action::SortAction<double>::INDEX, false);
ASSERT_NO_THROW(result = action.evaluate(input, mc));
for(uint_fast64_t i = 0; i < pathResult.size(); i++) {
ASSERT_EQ(pathResult.size()-i-1, result.stateMap[i]);
}
// 3) value, ascending
action = storm::property::action::SortAction<double>(storm::property::action::SortAction<double>::VALUE);
ASSERT_NO_THROW(result = action.evaluate(input, mc));
ASSERT_EQ(6, result.stateMap[0]);
ASSERT_EQ(7, result.stateMap[1]);
ASSERT_EQ(3, result.stateMap[2]);
ASSERT_EQ(4, result.stateMap[3]);
ASSERT_EQ(1, result.stateMap[4]);
ASSERT_EQ(0, result.stateMap[5]);
ASSERT_EQ(2, result.stateMap[6]);
ASSERT_EQ(5, result.stateMap[7]);
// 3) value, decending
action = storm::property::action::SortAction<double>(storm::property::action::SortAction<double>::VALUE, false);
ASSERT_NO_THROW(result = action.evaluate(input, mc));
ASSERT_EQ(5, result.stateMap[0]);
ASSERT_EQ(2, result.stateMap[1]);
ASSERT_EQ(0, result.stateMap[2]);
ASSERT_EQ(1, result.stateMap[3]);
ASSERT_EQ(4, result.stateMap[4]);
ASSERT_EQ(3, result.stateMap[5]);
ASSERT_EQ(6, result.stateMap[6]);
ASSERT_EQ(7, result.stateMap[7]);
// Check that this also works for state results instead.
input.pathResult = std::vector<double>();
input.stateResult = stateResult;
action = storm::property::action::SortAction<double>(storm::property::action::SortAction<double>::VALUE);
ASSERT_NO_THROW(result = action.evaluate(input, mc));
ASSERT_EQ(5, result.stateMap[0]);
ASSERT_EQ(6, result.stateMap[1]);
ASSERT_EQ(7, result.stateMap[2]);
ASSERT_EQ(0, result.stateMap[3]);
ASSERT_EQ(1, result.stateMap[4]);
ASSERT_EQ(2, result.stateMap[5]);
ASSERT_EQ(3, result.stateMap[6]);
ASSERT_EQ(4, result.stateMap[7]);
action = storm::property::action::SortAction<double>(storm::property::action::SortAction<double>::VALUE, false);
ASSERT_NO_THROW(result = action.evaluate(input, mc));
ASSERT_EQ(0, result.stateMap[0]);
ASSERT_EQ(1, result.stateMap[1]);
ASSERT_EQ(2, result.stateMap[2]);
ASSERT_EQ(3, result.stateMap[3]);
ASSERT_EQ(4, result.stateMap[4]);
ASSERT_EQ(5, result.stateMap[5]);
ASSERT_EQ(6, result.stateMap[6]);
ASSERT_EQ(7, result.stateMap[7]);
// Test if the resulting order does not depend on the input order.
input.stateResult = storm::storage::BitVector();
input.pathResult = pathResult;
action = storm::property::action::SortAction<double>(storm::property::action::SortAction<double>::INDEX);
ASSERT_NO_THROW(input = action.evaluate(input, mc));
action = storm::property::action::SortAction<double>(storm::property::action::SortAction<double>::VALUE);
ASSERT_NO_THROW(result = action.evaluate(input, mc));
ASSERT_EQ(6, result.stateMap[0]);
ASSERT_EQ(7, result.stateMap[1]);
ASSERT_EQ(3, result.stateMap[2]);
ASSERT_EQ(4, result.stateMap[3]);
ASSERT_EQ(1, result.stateMap[4]);
ASSERT_EQ(0, result.stateMap[5]);
ASSERT_EQ(2, result.stateMap[6]);
ASSERT_EQ(5, result.stateMap[7]);
}
TEST(ActionTest, SortActionSafety){
// Check that the path result has priority over the state result if for some erronous reason both are given.
// Setup the modelchecker.
storm::models::Dtmc<double> model = storm::parser::DeterministicModelParser::parseDtmc(STORM_CPP_TESTS_BASE_PATH "/functional/parser/tra_files/dtmc_actionTest.tra", STORM_CPP_TESTS_BASE_PATH "/functional/parser/lab_files/dtmc_actionTest.lab");
storm::modelchecker::prctl::SparseDtmcPrctlModelChecker<double> mc(model, new storm::solver::GmmxxLinearEquationSolver<double>());
// Build the filter input.
// Basically the modelchecking result of "F a" on the used DTMC.
std::vector<double> pathResult = mc.checkEventually(storm::property::prctl::Eventually<double>(std::make_shared<storm::property::prctl::Ap<double>>("a")), false);
storm::storage::BitVector stateResult = mc.checkAp(storm::property::prctl::Ap<double>("c"));
std::vector<uint_fast64_t> stateMap(pathResult.size());
for(uint_fast64_t i = 0; i < pathResult.size(); i++) {
stateMap[i] = pathResult.size()-i-1;
}
Result input(storm::storage::BitVector(pathResult.size(), true), stateMap, pathResult, stateResult);
Result result;
storm::property::action::SortAction<double> action(storm::property::action::SortAction<double>::VALUE);
ASSERT_NO_THROW(result = action.evaluate(input, mc));
ASSERT_EQ(6, result.stateMap[0]);
ASSERT_EQ(7, result.stateMap[1]);
ASSERT_EQ(3, result.stateMap[2]);
ASSERT_EQ(4, result.stateMap[3]);
ASSERT_EQ(1, result.stateMap[4]);
ASSERT_EQ(0, result.stateMap[5]);
ASSERT_EQ(2, result.stateMap[6]);
ASSERT_EQ(5, result.stateMap[7]);
}
Write Preview
Loading…
Cancel
Save