Skip to content

Commit

Permalink
fixes the case where we have 0 of something in an add expressions (TA…
Browse files Browse the repository at this point in the history 
…PAAL#42)

Fixes pnmlwriter, such that it can better handle all-expressions, and find color for places
  • Loading branch information
@MathiasMehl
MathiasMehl authored Apr 7, 2022
1 parent e4eeba0 commit 57eb947
Show file tree
Hide file tree
Showing 6 changed files with 129 additions and 33 deletions.
9 changes: 9 additions & 0 deletions include/PetriEngine/AbstractPetriNetBuilder.h
View file
Original file line number Diff line number Diff line change
Expand Up @@ -31,6 +31,7 @@ namespace PetriEngine {
class AbstractPetriNetBuilder {
protected:
bool _isColored = false;
bool _hasPartition = false;

public:
void parse_model(const std::string&& model);
Expand Down Expand Up @@ -108,6 +109,14 @@ namespace PetriEngine {
return _isColored;
}

virtual void enablePartition() {
_hasPartition = true;
}

virtual bool hasPartition() const {
return _hasPartition;
}

virtual void sort() = 0;

virtual ~AbstractPetriNetBuilder() {
Expand Down
4 changes: 2 additions & 2 deletions include/PetriEngine/Colored/PnmlWriter.h
View file
Original file line number Diff line number Diff line change
Expand Up @@ -85,11 +85,11 @@ namespace PetriEngine::Colored {

void handleProducts(std::vector<std::string> productSorts);

void handleMarking(Multiset multiset);

void handleTuple(const PetriEngine::Colored::Color *const c);

void handleOtherColor(const Color *const c);

void handleNumberOf(std::pair<const PetriEngine::Colored::Color *const, uint32_t> numberOff);
};
}

Expand Down
2 changes: 2 additions & 0 deletions include/PetriParse/PNMLParser.h
View file
Original file line number Diff line number Diff line change
Expand Up @@ -112,6 +112,8 @@ class PNMLParser {
ColorTypeMap colorTypes;
VariableMap variables;
bool isColored;
std::string placeTypeContext;
bool hasPartition;
std::vector<Query> queries;
std::vector<PetriEngine::Colored::ColorTypePartition> partitions;
std::vector<std::pair<char *, PetriEngine::Colored::ProductType*>> missingCTs;
Expand Down
76 changes: 46 additions & 30 deletions src/PetriEngine/Colored/PnmlWriter.cpp
View file
Original file line number Diff line number Diff line change
Expand Up @@ -9,6 +9,7 @@
namespace PetriEngine {
namespace Colored {
void PnmlWriter::toColPNML() {
//TODO cannot handle nets with partitions
metaInfo();
declarations();
page();
Expand Down Expand Up @@ -47,7 +48,6 @@ namespace PetriEngine {
std::vector<const ColorType *> types;
colortype->getColortypes(types);
if (types.size() > 1 && colortype->productSize() == 1) {
std::cout << colortype->getName();
throw base_error("types.size was over 1");
}
if (colortype->productSize() > 1) {
Expand Down Expand Up @@ -202,42 +202,58 @@ namespace PetriEngine {
_out << getTabs() << "<hlinitialMarking>\n";
_out << increaseTabs() << "<text>" << marking.toString() << "</text>\n";
_out << getTabs() << "<structure>\n";
_out << increaseTabs() << "<add>\n";
handleMarking(marking);
_out << decreaseTabs() << "</add>\n";

if (marking.size() > 1) {
bool first = true;
_out << increaseTabs() << "<add>\n";

for (const auto &p: marking) {
if (p.second == 0) {
continue;
}
if (first) {
_out << increaseTabs() << "<subterm>\n";
} else {
_out << getTabs() << "<subterm>\n";
}
handleNumberOf(p);
_out << decreaseTabs() << "</subterm>\n";
first = false;
}
_out << decreaseTabs() << "</add>\n";
} else {
for (const auto &p: marking) {
if (p.second == 0) {
continue;
}
handleNumberOf(p);
}
}

_out << decreaseTabs() << "</structure>\n";
_out << decreaseTabs() << "</hlinitialMarking>\n";
}

void PnmlWriter::handleMarking(Multiset marking) {
bool first = true;
for (const auto &p: marking) {
const auto &c = p.first;
const auto &m = p.second;
if (first) {
_out << increaseTabs() << "<subterm>\n";
} else {
_out << getTabs() << "<subterm>\n";
}
_out << increaseTabs() << "<numberof>\n";
_out << increaseTabs() << "<subterm>" << "\n";
_out << increaseTabs() << "<numberconstant value=\"" << m << "\">\n";
_out << increaseTabs() << "<positive/>\n";
_out << decreaseTabs() << "</numberconstant>\n";
void PnmlWriter::handleNumberOf(std::pair<const PetriEngine::Colored::Color *const, uint32_t> numberOff) {
const auto &c = numberOff.first;
const auto &m = numberOff.second;

_out << increaseTabs() << "<numberof>\n";
_out << increaseTabs() << "<subterm>" << "\n";
_out << increaseTabs() << "<numberconstant value=\"" << m << "\">\n";
_out << increaseTabs() << "<positive/>\n";
_out << decreaseTabs() << "</numberconstant>\n";
_out << decreaseTabs() << "</subterm>" << "\n";
if (c->isTuple()) {
_out << getTabs() << "<subterm>" << "\n";
handleTuple(c);
_out << decreaseTabs() << "</subterm>" << "\n";
if (c->isTuple()) {
_out << getTabs() << "<subterm>" << "\n";
handleTuple(c);
_out << decreaseTabs() << "</subterm>" << "\n";
} else {
_out << getTabs() << "<subterm>\n";
handleOtherColor(c);
_out << decreaseTabs() << "</subterm>\n";
}
_out << decreaseTabs() << "</numberof>\n";
} else {
_out << getTabs() << "<subterm>\n";
handleOtherColor(c);
_out << decreaseTabs() << "</subterm>\n";
first = false;
}
_out << decreaseTabs() << "</numberof>\n";
}

void PnmlWriter::handleTuple(const PetriEngine::Colored::Color *const c) {
Expand Down
66 changes: 65 additions & 1 deletion src/PetriParse/PNMLParser.cpp
View file
Original file line number Diff line number Diff line change
Expand Up @@ -41,6 +41,8 @@ void PNMLParser::parse(std::istream& xml,
arcs.clear();
_transitions.clear();
colorTypes.clear();
placeTypeContext = "";
hasPartition = false;

//Set the builder
this->builder = builder;
Expand Down Expand Up @@ -144,6 +146,8 @@ void PNMLParser::parseDeclarations(rapidxml::xml_node<>* element) {
variables[it->first_attribute("id")->value()] = var;
builder->addVariable(var);
} else if (strcmp(it->name(), "partition") == 0) {
builder->enablePartition();
hasPartition = true;
parsePartitions(it);
} else {
parseDeclarations(it);
Expand Down Expand Up @@ -620,6 +624,8 @@ void PNMLParser::parsePlace(rapidxml::xml_node<>* element) {
hlinitialMarking = PetriEngine::Colored::EvaluationVisitor::evaluate(*ae, context);
} else if (strcmp(it->name(), "type") == 0) {
type = parseUserSort(it);
placeTypeContext = type->getName();

}
}

Expand All @@ -644,6 +650,7 @@ void PNMLParser::parsePlace(rapidxml::xml_node<>* element) {
nn.id = id;
nn.isPlace = true;
id2name[id] = nn;
placeTypeContext = "";
}

void PNMLParser::parseArc(rapidxml::xml_node<>* element, bool inhibitor) {
Expand Down Expand Up @@ -814,7 +821,34 @@ void PNMLParser::parsePosition(rapidxml::xml_node<>* element, double& x, double&
}

const PetriEngine::Colored::Color* PNMLParser::findColor(const char* name) const {
bool placeTypeIsTuple = false;
if (!hasPartition && !placeTypeContext.empty()) {
auto &placeColorType = colorTypes.find(placeTypeContext)->second;
placeTypeIsTuple = placeColorType->productSize() > 1;
}

for (const auto& elem : colorTypes) {
if (!hasPartition && !placeTypeContext.empty()) {
//If we are finding color for a place, and the type of place is tuple
if (placeTypeIsTuple) {
auto &placeColorType = colorTypes.find(placeTypeContext)->second;
const auto *pt = dynamic_cast<const PetriEngine::Colored::ProductType *> (placeColorType);
//go through all colotypes in the tuple
for (uint32_t i = 0; i < placeColorType->productSize(); i++) {
const auto &nestedColorType = pt->getNestedColorType(i);
if (nestedColorType->productSize() > 1) {
throw base_error("Nested products when finding colors: ", nestedColorType->getName());
}
auto col = (*nestedColorType)[name];
if (col) {
return col;
}
}
//type of place is not a tuple
} else if (elem.first != placeTypeContext) {
continue;
}
}
auto col = (*elem.second)[name];
if (col)
return col;
Expand Down Expand Up @@ -846,19 +880,49 @@ std::vector<PetriEngine::Colored::ColorExpression_ptr> PNMLParser::findPartition
} else {
throw base_error("Could not find color expression in expression: ", element->name(), "\nCANNOT_COMPUTE\n");
}

for (auto partition : partitions) {
if (strcmp(partition.name.c_str(), name) == 0){
for(auto color : partition.colors){

colorExpressions.push_back(std::make_shared<PetriEngine::Colored::UserOperatorExpression>(color));

}
}
}
return colorExpressions;
}

const PetriEngine::Colored::Color* PNMLParser::findColorForIntRange(const char* value, uint32_t start, uint32_t end) const{
bool placeTypeIsTuple = false;
if (!hasPartition && !placeTypeContext.empty()) {
auto &placeColorType = colorTypes.find(placeTypeContext)->second;
placeTypeIsTuple = placeColorType->productSize() > 1;
}


for (const auto& elem : colorTypes) {
if (!hasPartition && !placeTypeContext.empty()) {
if (placeTypeIsTuple) {
auto &placeColorType = colorTypes.find(placeTypeContext)->second;
const auto *pt = dynamic_cast<const PetriEngine::Colored::ProductType *> (placeColorType);
//go through all colotypes in the tuple
for (uint32_t i = 0; i < placeColorType->productSize(); i++) {
const auto &nestedColorType = pt->getNestedColorType(i);
if (nestedColorType->productSize() > 1) {
throw base_error("Nested products when finding colors: ", nestedColorType->getName());
}
auto col = (*nestedColorType)[value];
if (col) {
if ((*nestedColorType).operator[](0).getId() == (start - 1) &&
(*elem.second).operator[]((*elem.second).size() - 1).getId() == end - 1)
return col;
}
}
//type of place is not a tuple
} else if (elem.first != placeTypeContext) {
continue;
}
}
auto col = (*elem.second)[value];
if (col){
if((*elem.second).operator[](0).getId() == (start -1) && (*elem.second).operator[]((*elem.second).size()-1).getId() == end -1)
Expand Down
5 changes: 5 additions & 0 deletions src/main.cpp
View file
Original file line number Diff line number Diff line change
Expand Up @@ -76,6 +76,11 @@ int main(int argc, const char** argv) {
throw base_error("CANNOT_COMPUTE\nError parsing the model\n", err.what());
}

if (!options.model_col_out_file.empty() && cpnBuilder.hasPartition()) {
std::cerr << "Cannot write colored PNML as the original net has partitions. Not supported (yet)" << std::endl;
return to_underlying(ReturnValue::UnknownCode);
}

if (options.cpnOverApprox && !cpnBuilder.isColored()) {
std::cerr << "CPN OverApproximation is only usable on colored models" << std::endl;
return to_underlying(ReturnValue::UnknownCode);
Expand Down

0 comments on commit 57eb947

Please sign in to comment.