diff --git a/src/formula/actions/RangeAction.h b/src/formula/actions/RangeAction.h index 85cf7c4af..ccb66fe00 100644 --- a/src/formula/actions/RangeAction.h +++ b/src/formula/actions/RangeAction.h @@ -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]]); } diff --git a/src/formula/actions/SortAction.h b/src/formula/actions/SortAction.h index d75e32fd7..35bc31026 100644 --- a/src/formula/actions/SortAction.h +++ b/src/formula/actions/SortAction.h @@ -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; diff --git a/test/functional/parser/ActionTest.cpp b/test/functional/parser/ActionTest.cpp index 5454c5787..647d8464f 100644 --- a/test/functional/parser/ActionTest.cpp +++ b/test/functional/parser/ActionTest.cpp @@ -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 pathResult = mc.checkEventually(storm::property::prctl::Eventually(std::make_shared>("a")), false); + storm::storage::BitVector stateResult = mc.checkAp(storm::property::prctl::Ap("c")); std::vector 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(std::make_shared>(storm::property::LESS, 0.5, std::make_shared>(std::make_shared>("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(); + 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 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 mc(model, new storm::solver::GmmxxLinearEquationSolver()); + + // Build the filter input. + // Basically the modelchecking result of "F a" on the used DTMC. + std::vector pathResult = mc.checkEventually(storm::property::prctl::Eventually(std::make_shared>("a")), false); + std::vector 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 action(std::shared_ptr>(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 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 mc(model, new storm::solver::GmmxxLinearEquationSolver()); + + // Build the filter input. + // Basically the modelchecking result of "F a" on the used DTMC. + std::vector pathResult = mc.checkEventually(storm::property::prctl::Eventually(std::make_shared>("a")), false); + storm::storage::BitVector stateResult = mc.checkAp(storm::property::prctl::Ap("c")); + std::vector 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 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 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 mc(model, new storm::solver::GmmxxLinearEquationSolver()); + + // Build the filter input. + // Basically the modelchecking result of "F a" on the used DTMC. + std::vector pathResult = mc.checkEventually(storm::property::prctl::Eventually(std::make_shared>("a")), false); + storm::storage::BitVector stateResult = mc.checkAp(storm::property::prctl::Ap("c")); + std::vector 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 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(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 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 mc(model, new storm::solver::GmmxxLinearEquationSolver()); + + // Build the filter input. + // Basically the modelchecking result of "F a" on the used DTMC. + std::vector pathResult = mc.checkEventually(storm::property::prctl::Eventually(std::make_shared>("a")), false); + storm::storage::BitVector stateResult = mc.checkAp(storm::property::prctl::Ap("c")); + std::vector 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 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(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(3,1), storm::exceptions::IllegalArgumentValueException); +} + +TEST(ActionTest, SortActionFunctionality){ + // Setup the modelchecker. + storm::models::Dtmc 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 mc(model, new storm::solver::GmmxxLinearEquationSolver()); + + // Build the filter input. + // Basically the modelchecking result of "F a" on the used DTMC. + std::vector pathResult = mc.checkEventually(storm::property::prctl::Eventually(std::make_shared>("a")), false); + storm::storage::BitVector stateResult = mc.checkAp(storm::property::prctl::Ap("c")); + std::vector 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 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(storm::property::action::SortAction::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(storm::property::action::SortAction::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(storm::property::action::SortAction::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(); + input.stateResult = stateResult; + + action = storm::property::action::SortAction(storm::property::action::SortAction::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(storm::property::action::SortAction::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(storm::property::action::SortAction::INDEX); + ASSERT_NO_THROW(input = action.evaluate(input, mc)); + action = storm::property::action::SortAction(storm::property::action::SortAction::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 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 mc(model, new storm::solver::GmmxxLinearEquationSolver()); + + // Build the filter input. + // Basically the modelchecking result of "F a" on the used DTMC. + std::vector pathResult = mc.checkEventually(storm::property::prctl::Eventually(std::make_shared>("a")), false); + storm::storage::BitVector stateResult = mc.checkAp(storm::property::prctl::Ap("c")); + std::vector 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 action(storm::property::action::SortAction::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]); }