mirror of
http://172.16.200.102/MOISE/Timed-Altarica-To-Fiacre-Translator.git
synced 2026-03-06 14:51:47 +01:00
317 lines
11 KiB
C++
317 lines
11 KiB
C++
/*******************************************************************************
|
||
* Copyright (c) 2015-2016 ONERA.
|
||
* Ce logiciel est la propriété de l’ONERA (the French Aerospace Lab).
|
||
* Tous droits réservés.
|
||
*
|
||
* Ce programme et les éléments qui l'accompagnent sont mis à disposition
|
||
* aux conditions définies par le contrat de licence logiciel CeCILL-C soumise
|
||
* au droit français et respectant les principes de diffusion des logiciels libres.
|
||
* Vous pouvez utiliser, modifier et/ou redistribuer ce programme
|
||
* sous les conditions de la licence CeCILL-C (http://www.cecill.info).
|
||
|
||
* This software is property of ONERA (the French Aerospace Lab).
|
||
* All rights reserved.
|
||
*
|
||
* This program and the accompanying materials are made available under
|
||
* the terms of the CeCILL-C license under French law and
|
||
* abiding by the rules of distribution of free software.
|
||
* You can use, modify and/ or redistribute the software under the terms of
|
||
* the CeCILL-C license (http://www.cecill.info).
|
||
*
|
||
* Contributeurs/contributors:
|
||
* Florent Teichteil-Königsbuch (ONERA - Centre de Toulouse) - initial API and implementation
|
||
*
|
||
*******************************************************************************/
|
||
|
||
//#include "algorithms/EmptyStateVisitor.hh"
|
||
//#include "algorithms/DotStateVisitor.hh"
|
||
#include "grammars/altarica/FiacreTranslator.hh"
|
||
//#include "solvers/epochsolver.hh"
|
||
//#include "solvers/altaricaLogic.hh"
|
||
#include "console/ParsingDriverConsoleReporter.hh"
|
||
|
||
#include "grammars/altarica/Assignment.hh"
|
||
#include "grammars/altarica/AltaricaGenerator.hh"
|
||
#include "grammars/altarica/Event.hh"
|
||
#include "grammars/altarica/MemberAccess.hh"
|
||
#include "grammars/altarica/Synchronisation.hh"
|
||
#include "grammars/altarica/Transition.hh"
|
||
#include "grammars/altarica/Variable.hh"
|
||
|
||
#include "grammars/altarica/Event.hh"
|
||
#include "grammars/altarica/Assertion.hh"
|
||
|
||
|
||
namespace epoch {
|
||
namespace console {
|
||
void printStates(int ps, int maxDepth, epoch::altarica::AltaricaState* s, epoch::altarica::AltaricaModel* m) {
|
||
|
||
std::cerr << "\ndepth = "<< maxDepth-ps << std::endl;
|
||
std::cerr << s->toString(true, true, true, true);
|
||
if (ps == 0) {
|
||
delete s;
|
||
std::cerr << "\n!!!!!!!!!!!! GOING UP the tree\n"<< std::endl;
|
||
return;
|
||
}
|
||
|
||
std::vector<epoch::altarica::MetaEvent*> * mev = m->getEnabledMetaEventsAll(s);
|
||
std::cerr<<"\n # metaEvents: "<< mev->size() << std::endl;
|
||
for (int i=0; i<mev->size(); ++i) {
|
||
std::cerr << " MEV " << i << ": " << (*mev)[i]->toString() << std::endl;
|
||
}
|
||
|
||
|
||
for (int i=0; i<mev->size(); ++i) {
|
||
std::cerr << "\ndoing MEV " << i << ": " << (*mev)[i]->toString() << std::endl;
|
||
epoch::altarica::AltaricaState *s2 = m->getNextState(s,(*mev)[i]);
|
||
m->evaluateFlowVars(s2);
|
||
printStates(ps-1, maxDepth, s2, m);
|
||
}
|
||
|
||
// std::vector<epoch::altarica::Event*> ev = m->getAtomicEvents();
|
||
// std::cerr<<"\n # Events: "<< ev.size() << std::endl;
|
||
// for (int i=0; i<ev.size(); ++i) {
|
||
// std::cerr << " EV " << i << ": " << ev[i]->toString() << std::endl;
|
||
// }
|
||
|
||
}
|
||
|
||
|
||
|
||
std::string print_pre (const epoch::altarica::AltaricaModel *amodel_, const std::vector<epoch::altarica::Event*> *ev, int n, std::ostringstream * sout) {
|
||
|
||
std::ostringstream sret;
|
||
std::string s ;
|
||
if (n < 0)
|
||
return sout->str() + "\n";
|
||
|
||
// for (int i = ev->size(); i > 0; --i) {
|
||
|
||
// ss << "\tEvent" << i-1;
|
||
unsigned j = 0;
|
||
for (auto &ti : *(ev->at(n)->getTrans()) ) {
|
||
std::ostringstream ss;
|
||
ss << sout->str() << ti->getPrecond()->toString( ti->getNode(), amodel_);
|
||
if ( n != 0 )
|
||
ss << " and ";
|
||
//ss << sout->str() << "\tE" << n << "T" << j++;
|
||
sret << print_pre(amodel_, ev, n-1, &ss);
|
||
|
||
|
||
// const std::vector<epoch::altarica::Assignment*>* effects = ti->getAssigns();
|
||
// if(effects->size() > 0) {
|
||
// for(auto &a : *effects) {
|
||
// std::cout << "\tpost : "
|
||
// << a->getVar()->toFiacre()
|
||
// //<< a->getMA()->toString()
|
||
// << " := "
|
||
// << a->getExpr()->toString( a->getNode() )
|
||
// << ";" << std::endl;
|
||
// }
|
||
// }
|
||
// }
|
||
|
||
}
|
||
return sret.str();
|
||
}
|
||
|
||
|
||
bool DoAltarica(const std::string& modelFile, const std::string& initFile, const std::string& var1, const std::string& value1, const std::string& var2, const std::string& value2,bool ds, int ps, bool invert_comp1, bool invert_comp2,
|
||
int ac, char* av[], int algo, int hess, int blas, double threshold, unsigned int dtimebound, double ctimebound, bool printfunction, const std::string& printGraph) {
|
||
epoch::console::ParsingDriverConsoleReporter pdr;
|
||
epoch::altarica::AltaricaGenerator gen(modelFile, pdr);
|
||
gen.amodel_->setDebugSemantics(ds);
|
||
|
||
// if (initFile.compare("") != 0)
|
||
if (initFile.length() >= 4 &&
|
||
0 == initFile.compare(initFile.length() - 4, 4, ".xml"))
|
||
gen.amodel_->setInitInfoXML(initFile);
|
||
else if (initFile.length() >= 5 &&
|
||
0 == initFile.compare(initFile.length() - 4, 4, ".json"))
|
||
gen.amodel_->setInitInfoJSON(initFile);
|
||
|
||
epoch::altarica::AltaricaState * i = gen.amodel_->initialState();
|
||
gen.amodel_->evaluateFlowVars(i);
|
||
// std::cerr << i->toString(true,true,true,true);
|
||
std::cerr << std::endl << "MODEL STATS:" << std::endl;
|
||
std::cerr << "number of state vars: " << gen.amodel_->getNStateVars() << std::endl;
|
||
std::cerr << "number of _different_ flow vars: " << gen.amodel_->getNFlowVars() << std::endl;
|
||
std::cerr << "number of atomic events: " << gen.amodel_->getNEvents() << std::endl;
|
||
|
||
|
||
//// Debug printing start ////
|
||
|
||
if (gen.amodel_->getDebugSemantics())
|
||
{
|
||
std::cout << std::endl << "FLOW VARS" << std::endl;
|
||
|
||
for(auto &v : gen.amodel_->getFlowVars()) {
|
||
|
||
std::cout << v->getFullName() <<
|
||
" : " <<
|
||
v->getDomain()->toString() <<
|
||
std::endl;
|
||
}
|
||
|
||
std::cout << std::endl << "STATE VARS" << std::endl;
|
||
for(auto &v : gen.amodel_->getStateVars()) {
|
||
std::cout << v->getFullName()
|
||
<< " : "
|
||
<< v->getDomain()->toString()
|
||
<< std::endl;
|
||
}
|
||
|
||
std::cout << std::endl << "ATOMIC EVTS" << std::endl;
|
||
for(auto &e : gen.amodel_->getAtomicEvents()) {
|
||
std::cout << e->getMA()->toString()
|
||
<< " : "
|
||
<< std::endl;
|
||
if(e->getTrans()->size() > 0)
|
||
for(auto &t : *e->getTrans()) {
|
||
std::cout << " pre : "
|
||
<< t->getPrecond()->toString()
|
||
<< std::endl;
|
||
if(t->getAssigns()->size() > 0) {
|
||
std::cout << " post : ";
|
||
for(auto &a : *t->getAssigns()) {
|
||
std::cout << " "
|
||
// << a->getVar()->toFiacre() //getVar()->getMA()->toString()
|
||
<< a->getMA()->toString()
|
||
<< " := "
|
||
<< a->getExpr()->toString()
|
||
<< std::endl;
|
||
}
|
||
}
|
||
}
|
||
}
|
||
|
||
// Get Syncs //
|
||
unsigned nev=0, ne = 0;
|
||
for(auto &sy :gen.amodel_->getSyncs())
|
||
std::cout << sy->toString()<< std::endl;
|
||
|
||
std::cout << std::endl << "SYNCS" << std::endl;
|
||
// for(auto &sy :gen.amodel_->getSyncs())
|
||
// std::cout << sy->toString()<< std::endl;
|
||
unsigned n=0;
|
||
for(auto &sy :gen.amodel_->getMetaEvents()) {
|
||
std::cout << "Meta event" << n++ << std::endl;
|
||
if (sy->getEvents()->size() != 0) {
|
||
for (std::vector<epoch::altarica::Event*>::iterator i = sy->getEvents()->begin();
|
||
i!=sy->getEvents()->end(); ++i) {
|
||
ne = 0;
|
||
for (auto &t : *(*i)->getTrans()) {
|
||
std::cout << nev << "." << ne++ << ". pre : " << t->getPrecond()->toString( t->getNode(), gen.amodel_) << std::endl;
|
||
|
||
if(t->getAssigns()->size() > 0) {
|
||
for(auto &a : *(t->getAssigns())) {
|
||
std::cout << "\tpost : "
|
||
<< a->getVar()->toFiacre()
|
||
//<< a->getMA()->toString()
|
||
<< " := "
|
||
<< a->getExpr()->toString( a->getNode(), gen.amodel_ )
|
||
<< ";" << std::endl;
|
||
}
|
||
}
|
||
}
|
||
++nev;
|
||
}
|
||
}
|
||
else
|
||
std::cout << " NO EVENT";
|
||
}
|
||
|
||
////////
|
||
std::cout << std::endl << "SYNCS" << std::endl;
|
||
|
||
nev=0; ne = 0;
|
||
for(auto &sy :gen.amodel_->getMetaEvents()) {
|
||
std::cout << std::endl << "Meta event" << nev++ << std::endl;
|
||
if (sy->getEvents()->size() != 0) {
|
||
|
||
std::ostringstream ss("init ");
|
||
|
||
int num = sy->getEvents()->size()-1;
|
||
|
||
std::cout << print_pre(gen.amodel_, sy->getEvents() , num, &ss );
|
||
|
||
}
|
||
else
|
||
std::cout << " NO EVENT";
|
||
}
|
||
std::cout << std::endl << "ATOMIC DIRAC EVTS" << std::endl;
|
||
for(auto &e : gen.amodel_->getAtomicDiracEvents()) {
|
||
std::cout << e->getMA()->toString()
|
||
<< " : "
|
||
<< std::endl;
|
||
if(e->getTrans()->size() > 0)
|
||
for(auto &t : *e->getTrans()) {
|
||
std::cout << " pre : "
|
||
<< t->getPrecond()->toString()
|
||
<< std::endl;
|
||
if(t->getAssigns()->size() > 0) {
|
||
std::cout << " post: ";
|
||
for(auto &a : *t->getAssigns()) {
|
||
std::cout << " "
|
||
// << a->getVar()->toFiacre() //getVar()->getMA()->toString()
|
||
<< a->getMA()->toString()
|
||
<< " := "
|
||
<< a->getExpr()->toString()
|
||
<< std::endl;
|
||
}
|
||
}
|
||
}
|
||
}
|
||
|
||
std::cout << std::endl << "ASSERTIONS" << std::endl;
|
||
|
||
for(auto &e : gen.amodel_->getAsserts()) {
|
||
size_t et = (size_t)(e);
|
||
std::cout << et << " "<< e->getExpr()->toString()<< std::endl;
|
||
}
|
||
}
|
||
//////// Debug printing end ///////
|
||
|
||
|
||
if (ps >= 0) {
|
||
// Makes a FIACRE model
|
||
std::cerr << "\n!!!!!!!!!!!! Printing FIACRE model\n\n"<< std::endl;
|
||
|
||
epoch::altarica::FiacreTranslator f(gen.amodel_);
|
||
f.printFiacre();
|
||
|
||
}
|
||
|
||
return true;
|
||
// A partir d'ici : algorithme
|
||
//const epoch::altarica::Node& mainNode = *(gen.amodel_->findNodeByName("main"));
|
||
|
||
|
||
|
||
// Formule f1 : tout est ok
|
||
/* epoch::solvers::AltaricaLogic* f1;
|
||
|
||
|
||
if (strcmp(var1.c_str(), "") != 0)
|
||
f1 = new epoch::solvers::AltaricaLogicF2(gen.amodel_,var1,value1, invert_comp1);
|
||
else
|
||
f1 = new epoch::solvers::AltaricaLogicF1();
|
||
|
||
epoch::solvers::AltaricaLogicF2 f2(gen.amodel_,var1,value1, invert_comp1);
|
||
epoch::altarica::AltaricaGenerator::State is(i);
|
||
|
||
if (printGraph.empty()) {
|
||
return epoch::solvers::MySolver<epoch::solvers::AltaricaLogic, epoch::altarica::AltaricaGenerator, epoch::algorithm::EmptyStateVisitor>::solve(ac, av,
|
||
algo, hess, blas, threshold, dtimebound, ctimebound,
|
||
printfunction, epoch::algorithm::EmptyStateVisitor(),
|
||
gen, is, *f1, f2);
|
||
} else {
|
||
return epoch::solvers::MySolver<epoch::solvers::AltaricaLogic, epoch::altarica::AltaricaGenerator, epoch::algorithm::DotStateVisitor>::solve(ac, av,
|
||
algo, hess, blas, threshold, dtimebound, ctimebound,
|
||
printfunction, epoch::algorithm::DotStateVisitor(printGraph),
|
||
gen, is, *f1, f2);
|
||
}*/
|
||
}
|
||
}
|
||
}
|