Skip to content

Commit

Permalink
Colored reductions (TAPAAL#58)
Browse files Browse the repository at this point in the history
* rule-i fix inconsistencies

* Generalize Rule C

* minor fixes to detection etc

Co-authored-by: MathiasMehl <[email protected]>
Co-authored-by: NicEastvillage <[email protected]>
Co-authored-by: srba <[email protected]>
  • Loading branch information
4 people authored Apr 29, 2022
1 parent 9d3a0a6 commit b6899cc
Show file tree
Hide file tree
Showing 7 changed files with 139 additions and 172 deletions.
5 changes: 3 additions & 2 deletions boost_tests/color_test.cpp
Original file line number Diff line number Diff line change
Expand Up @@ -104,6 +104,7 @@ BOOST_AUTO_TEST_CASE(PhilosophersDynCOL03, * utf::timeout(60)) {
{
for(auto approx : {false, true})
{
if(approx && reduce) continue;
std::cerr << "\t" << model << ", " << query << std::boolalpha << " reduce=" << reduce << " partition=" << partition << " sym=" << symmetry << " cfp=" << cfp << " approx=" << approx << std::endl;
try {
auto [pn, conditions, qstrings] = load_pn(model.c_str(),
Expand All @@ -116,8 +117,8 @@ BOOST_AUTO_TEST_CASE(PhilosophersDynCOL03, * utf::timeout(60)) {
std::vector<Condition_ptr> vec{c2};
std::vector<Reachability::ResultPrinter::Result> results{Reachability::ResultPrinter::Unknown};
strategy.reachable(vec, results, Strategy::DFS, false, false, false, false, 0);
BOOST_REQUIRE(!approx);
BOOST_REQUIRE_EQUAL(expected[i], results[0]);
if(!approx) // if it is approx, the answer could be anything, the handling-logic is in the result-printer
BOOST_REQUIRE_EQUAL(expected[i], results[0]);
}
} catch (const base_error& er) {
BOOST_REQUIRE(approx);
Expand Down
4 changes: 3 additions & 1 deletion include/PetriEngine/Colored/ArcVarMultisetVisitor.h
Original file line number Diff line number Diff line change
Expand Up @@ -8,11 +8,13 @@
#ifndef VERIFYPN_ARCVARMULTISETVISITOR_H
#define VERIFYPN_ARCVARMULTISETVISITOR_H

#include <utils/errors.h>
#include "Expressions.h"
#include "ColorExpressionVisitor.h"
#include "VarMultiset.h"

#include <utils/errors.h>
#include <optional>

namespace PetriEngine::Colored {

std::optional<VarMultiset> extractVarMultiset(const ArcExpression &e);
Expand Down
4 changes: 3 additions & 1 deletion include/PetriEngine/Colored/VarMultiset.h
Original file line number Diff line number Diff line change
Expand Up @@ -8,9 +8,11 @@
#ifndef VERIFYPN_VARMULTISET_H
#define VERIFYPN_VARMULTISET_H

#include "Colors.h"

#include <vector>
#include <cstdint>
#include "Colors.h"
#include <optional>

namespace PetriEngine::Colored {
class VarMultiset {
Expand Down
2 changes: 1 addition & 1 deletion include/PetriEngine/Reducer.h
Original file line number Diff line number Diff line change
Expand Up @@ -134,7 +134,7 @@ namespace PetriEngine {
bool ReducebyRuleC(uint32_t* placeInQuery);
bool ReducebyRuleD(uint32_t* placeInQuery);
bool ReducebyRuleE(uint32_t* placeInQuery);
bool ReducebyRuleI(uint32_t* placeInQuery, bool remove_loops, bool remove_consumers);
bool ReducebyRuleI(uint32_t* placeInQuery, bool remove_consumers);
bool ReducebyRuleF(uint32_t* placeInQuery);
bool ReducebyRuleG(uint32_t* placeInQuery, bool remove_loops, bool remove_consumers);
bool ReducebyRuleH(uint32_t* placeInQuery);
Expand Down
Loading

0 comments on commit b6899cc

Please sign in to comment.