mirror of
http://172.16.200.102/MOISE/Timed-Altarica-To-Fiacre-Translator.git
synced 2026-03-11 15:31:48 +01:00
212 lines
7.6 KiB
C++
212 lines
7.6 KiB
C++
|
/*******************************************************************************
|
|||
|
|
* Copyright (c) 2015-2017 ONERA and IRT AESE (IRT Saint Exupéry).
|
|||
|
|
* Ce logiciel est la propriété de l’ONERA (the French Aerospace Lab) et de
|
|||
|
|
* l'IRT AESE (IRT Saint Exupéry).
|
|||
|
|
* 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) and of
|
|||
|
|
* the IRT AESE (IRT Saint Exupéry).
|
|||
|
|
* 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:
|
|||
|
|
* Xavier Pucel (ONERA - Centre de Toulouse) - initial API and implementation
|
|||
|
|
* Alexandre Albore (IRT Saint-Exupéry) - Altarica/Fiacre translation
|
|||
|
|
*
|
|||
|
|
*******************************************************************************/
|
|||
|
|
|
|||
|
|
#include <boost/filesystem.hpp>
|
|||
|
|
#include <boost/program_options.hpp>
|
|||
|
|
#include <boost/exception/diagnostic_information.hpp>
|
|||
|
|
|
|||
|
|
#include "epochconsolealtarica.hh"
|
|||
|
|
|
|||
|
|
#include "grammars/altarica/AltaricaGenerator.hh"
|
|||
|
|
#include "grammars/altarica/Assignment.hh"
|
|||
|
|
#include "grammars/altarica/Event.hh"
|
|||
|
|
#include "grammars/altarica/MemberAccess.hh"
|
|||
|
|
#include "grammars/altarica/Node.hh"
|
|||
|
|
#include "grammars/altarica/Synchronisation.hh"
|
|||
|
|
#include "grammars/altarica/Transition.hh"
|
|||
|
|
#include "grammars/altarica/Variable.hh"
|
|||
|
|
|
|||
|
|
#include "symbolic/SymModel.hh"
|
|||
|
|
//using namespace epoch;
|
|||
|
|
|
|||
|
|
int main(int ac, char* av[]) {
|
|||
|
|
unsigned int verbosity; // verbosity level
|
|||
|
|
std::string modelFile;
|
|||
|
|
std::string initFile;
|
|||
|
|
bool ds;
|
|||
|
|
bool printFlow;
|
|||
|
|
bool printNULL;
|
|||
|
|
bool printDomain;
|
|||
|
|
|
|||
|
|
// try {
|
|||
|
|
boost::program_options::options_description desc("Allowed options");
|
|||
|
|
desc.add_options()
|
|||
|
|
("help", "produce help message")
|
|||
|
|
("ds",
|
|||
|
|
boost::program_options::value<bool>(&ds)->default_value(false),
|
|||
|
|
"print semantic debug messages for discrete models")
|
|||
|
|
("file",
|
|||
|
|
boost::program_options::value<std::string>(&modelFile)-> default_value(""),
|
|||
|
|
"model file (either .alt (altartica) or [.prism|.nm|.pm|.sm] (prism)")
|
|||
|
|
("init",
|
|||
|
|
boost::program_options::value<std::string>(&initFile)->default_value(""),
|
|||
|
|
"init file")
|
|||
|
|
("pf",
|
|||
|
|
boost::program_options::value<bool>(&printFlow)->default_value(false),
|
|||
|
|
"print flow vars")
|
|||
|
|
("pn",
|
|||
|
|
boost::program_options::value<bool>(&printNULL)->default_value(false),
|
|||
|
|
"print null values")
|
|||
|
|
("pd",
|
|||
|
|
boost::program_options::value<bool>(&printDomain)->default_value(false),
|
|||
|
|
"print var domains")
|
|||
|
|
;
|
|||
|
|
|
|||
|
|
boost::program_options::positional_options_description p;
|
|||
|
|
p.add("file", 1);
|
|||
|
|
|
|||
|
|
|
|||
|
|
namespace options_style_ns = boost::program_options::command_line_style;
|
|||
|
|
int options_style = options_style_ns::allow_short
|
|||
|
|
| options_style_ns::short_allow_adjacent
|
|||
|
|
| options_style_ns::short_allow_next
|
|||
|
|
| options_style_ns::allow_long
|
|||
|
|
| options_style_ns::long_allow_adjacent
|
|||
|
|
| options_style_ns::long_allow_next
|
|||
|
|
| options_style_ns::allow_sticky
|
|||
|
|
| options_style_ns::allow_dash_for_short;
|
|||
|
|
boost::program_options::variables_map vm;
|
|||
|
|
// boost::program_options::store
|
|||
|
|
// (boost::program_options::parse_command_line(ac, av, desc, options_style),
|
|||
|
|
// vm);
|
|||
|
|
boost::program_options::store
|
|||
|
|
(boost::program_options::command_line_parser(ac,av).options(desc).
|
|||
|
|
positional(p).style(options_style).run(),
|
|||
|
|
vm);
|
|||
|
|
boost::program_options::notify(vm);
|
|||
|
|
|
|||
|
|
if (vm.count("help")) {
|
|||
|
|
std::cout << desc << std::endl;
|
|||
|
|
return 1;
|
|||
|
|
}
|
|||
|
|
|
|||
|
|
epoch::console::ParsingDriverConsoleReporter pdr;
|
|||
|
|
epoch::altarica::AltaricaGenerator gen(modelFile, pdr);
|
|||
|
|
gen.amodel_->setDebugSemantics(ds);
|
|||
|
|
|
|||
|
|
// if (initFile.compare("") != 0)
|
|||
|
|
// gen.amodel_->setInitInfo(initFile);
|
|||
|
|
|
|||
|
|
// std::cout << std::endl << "MODEL STATS:" << std::endl;
|
|||
|
|
|
|||
|
|
// std::cout << "number of state vars: "
|
|||
|
|
// << gen.amodel_->getNStateVars()
|
|||
|
|
// << std::endl;
|
|||
|
|
|
|||
|
|
// std::cout << "number of _different_ flow vars: "
|
|||
|
|
// << gen.amodel_->getNFlowVars()
|
|||
|
|
// << std::endl;
|
|||
|
|
|
|||
|
|
// std::cout << "number of atomic events: "
|
|||
|
|
// << gen.amodel_->getNEvents()
|
|||
|
|
// << std::endl
|
|||
|
|
// << std::endl;
|
|||
|
|
|
|||
|
|
std::cout << std::endl << "FLOW VARS" << std::endl;
|
|||
|
|
for(auto &v : gen.amodel_->getFlowVars()) {
|
|||
|
|
std::cout << v->getFullName() << " : "
|
|||
|
|
<< v->getDomain()->toString()
|
|||
|
|
// << std::endl
|
|||
|
|
// << "var at " << v->getIndex()
|
|||
|
|
// << " is "
|
|||
|
|
// << gen.amodel_->getFlowVar(v->getIndex())->getFullName()
|
|||
|
|
<< 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
|
|||
|
|
// << "var at " << v->getIndex()
|
|||
|
|
// << " is "
|
|||
|
|
// << gen.amodel_->getStateVar(v->getIndex())->getFullName()
|
|||
|
|
<< std::endl;
|
|||
|
|
}
|
|||
|
|
|
|||
|
|
std::cout << std::endl << "ATOMIC EVTS" << std::endl;
|
|||
|
|
for(auto &e : gen.amodel_->getAtomicEvents()) {
|
|||
|
|
std::cout << e->getFullName()
|
|||
|
|
<< " : "
|
|||
|
|
<< 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: " << std::endl;
|
|||
|
|
for(auto &a : *t->getAssigns()) {
|
|||
|
|
std::cout << " "
|
|||
|
|
<< a->getVar()->toString()
|
|||
|
|
<< " := "
|
|||
|
|
<< a->getExpr()->toString()
|
|||
|
|
<< std::endl;
|
|||
|
|
}
|
|||
|
|
}
|
|||
|
|
}
|
|||
|
|
}
|
|||
|
|
|
|||
|
|
std::cout << std::endl << "SYNCS" << std::endl;
|
|||
|
|
for(auto &s: gen.amodel_->getSyncs()) {
|
|||
|
|
if(s->getMA() != NULL)
|
|||
|
|
std::cout << s->toString() << std::endl;
|
|||
|
|
if(s->getMandatoryEvents()->size() > 0) {
|
|||
|
|
std::cout << " Mandatory events:" << std::endl;
|
|||
|
|
for(auto &e : *s->getMandatoryEvents())
|
|||
|
|
std::cout << " " << e->getFullName() << std::endl;
|
|||
|
|
}
|
|||
|
|
if(s->getOptionalEvents()->size() > 0) {
|
|||
|
|
std::cout << " Optional events:" << std::endl;
|
|||
|
|
for(auto &e : *s->getOptionalEvents())
|
|||
|
|
std::cout << " " << e->getFullName() << std::endl;
|
|||
|
|
}
|
|||
|
|
if(s->getNumericalConstant() >= 0) {
|
|||
|
|
std::cout << " Constraint type: " << s->getConstraintType() << std::endl;
|
|||
|
|
std::cout << " Numerical constant: "
|
|||
|
|
<< s->getNumericalConstant()
|
|||
|
|
<< std::endl;
|
|||
|
|
}
|
|||
|
|
}
|
|||
|
|
|
|||
|
|
epoch::symbolic::SymModel bddmodel(gen.amodel_);
|
|||
|
|
|
|||
|
|
// }
|
|||
|
|
// catch (const boost::program_options::error& error) {
|
|||
|
|
// std::cerr << error.what() << std::endl;
|
|||
|
|
// return -1;
|
|||
|
|
// } catch (const epoch::altarica::AltaricaException& error) {
|
|||
|
|
// std::cerr << error.what() << std::endl;
|
|||
|
|
// return -1;
|
|||
|
|
// } catch (const std::exception& error) {
|
|||
|
|
// std::cerr << boost::diagnostic_information(error) << std::endl;
|
|||
|
|
// return -1;
|
|||
|
|
// }
|
|||
|
|
}
|