mirror of
http://172.16.200.102/MOISE/Timed-Altarica-To-Fiacre-Translator.git
synced 2026-03-04 12:01:47 +01:00
234 lines
11 KiB
C++
234 lines
11 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:
|
|||
|
|
* Florent Teichteil-Königsbuch (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 "grammars/altarica/altarica_lexer.h"
|
|||
|
|
#include "epochconsolealtarica.hh"
|
|||
|
|
//#include "epochconsoleprism.hh"
|
|||
|
|
|
|||
|
|
#include "grammars/altarica/AltaricaGenerator.hh"
|
|||
|
|
#include "grammars/altarica/AltaricaJson.hh"
|
|||
|
|
#include "grammars/altarica/AltaricaInitInfoXML2.hh"
|
|||
|
|
#include "grammars/altarica/AltaricaInteractive.hh"
|
|||
|
|
//#include "algorithms/incrTarjan.hh"
|
|||
|
|
// #include "algorithms/LinearSystemExactParametricSolver.hh"
|
|||
|
|
#include "grammars/details/parsingdriverbaseimpl.hh"
|
|||
|
|
// #include "solvers/altaricaLogic.hh"
|
|||
|
|
#include <ios>
|
|||
|
|
|
|||
|
|
//using namespace epoch;
|
|||
|
|
|
|||
|
|
int main (int ac, char* av[])
|
|||
|
|
{
|
|||
|
|
unsigned int verbosity; // verbosity level
|
|||
|
|
std::string modelFile;
|
|||
|
|
std::string jsonFile;
|
|||
|
|
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)")
|
|||
|
|
("json", boost::program_options::value<std::string>(&jsonFile)->default_value(""), "json file (init, testcases)")
|
|||
|
|
("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;
|
|||
|
|
|
|||
|
|
|
|||
|
|
boost::filesystem::path filepath(modelFile);
|
|||
|
|
if (!filepath.has_extension()) {
|
|||
|
|
std::cerr << "File '" << filepath << "' has no extension!" << std::endl;
|
|||
|
|
return -1;
|
|||
|
|
} else if (filepath.extension().generic_string() == ".alt") { // altarica
|
|||
|
|
epoch::altarica::AltaricaGenerator gen(modelFile, pdr);
|
|||
|
|
gen.amodel_->setDebugSemantics(ds);
|
|||
|
|
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;
|
|||
|
|
|
|||
|
|
|
|||
|
|
epoch::altarica::AltaricaJson * aj;
|
|||
|
|
if (jsonFile.compare("") != 0) {
|
|||
|
|
aj = gen.amodel_->setInitInfoJSON(jsonFile);
|
|||
|
|
std::cout << aj->toString() <<std::endl;
|
|||
|
|
}
|
|||
|
|
|
|||
|
|
epoch::altarica::AltaricaState * cstate = gen.amodel_->initialState();
|
|||
|
|
std::cout << "Initial State:\n";
|
|||
|
|
if (printFlow)
|
|||
|
|
gen.amodel_->evaluateFlowVars(cstate);
|
|||
|
|
std::cout << cstate->toString(true,printFlow,printNULL,printDomain);
|
|||
|
|
|
|||
|
|
if (jsonFile.compare("") != 0) {
|
|||
|
|
if (aj->hasEvents())
|
|||
|
|
return aj->runTestCase(cstate);
|
|||
|
|
}
|
|||
|
|
if (jsonFile.compare("") == 0 || !aj->hasEvents())
|
|||
|
|
epoch::altarica::interactiveExecute(cstate, gen.amodel_,printFlow, printNULL, printDomain);
|
|||
|
|
|
|||
|
|
|
|||
|
|
|
|||
|
|
// epoch::altarica::interactiveExecute(gen.amodel_->initialState(), gen.amodel_,true, false, false);
|
|||
|
|
|
|||
|
|
// typedef epoch::algorithm::IncrTarjan<epoch::solvers::AltaricaLogic,
|
|||
|
|
// epoch::altarica::AltaricaGenerator,
|
|||
|
|
// epoch::graph::HashTable,
|
|||
|
|
// epoch::graph::List,
|
|||
|
|
// epoch::algorithm::LinearSystemExactParametricSolver> myTarjanAlt;
|
|||
|
|
// myTarjanAlt mt(gen);
|
|||
|
|
// epoch::solvers::AltaricaLogicF1 f1;
|
|||
|
|
// epoch::solvers::AltaricaLogicF2 f2(gen.amodel_, "main.s", "s9", false);
|
|||
|
|
|
|||
|
|
// mt.launch(gen.amodel_->initialState(), f1, f2);
|
|||
|
|
// delete gen.amodel_;
|
|||
|
|
|
|||
|
|
|
|||
|
|
}
|
|||
|
|
|
|||
|
|
/*** removing PRISM extension ****
|
|||
|
|
|
|||
|
|
else if (filepath.extension().generic_string() == ".prism" ||
|
|||
|
|
filepath.extension().generic_string() ==".nm" ||
|
|||
|
|
filepath.extension().generic_string() == ".pm" ||
|
|||
|
|
filepath.extension().generic_string() == ".sm") { // prism file
|
|||
|
|
epoch::prism::ParsingDriver parser(epoch::prism::ParsingDriver::PARSE_MODULES, pdr, modelFile);
|
|||
|
|
parser.context().setType(epoch::prism::Context::PRISM_TYPE_DTMC);
|
|||
|
|
parser.Parse();
|
|||
|
|
parser.context().setType(epoch::prism::Context::PRISM_TYPE_DTMC);
|
|||
|
|
epoch::prism::Generator<epoch::prism::Context::PRISM_TYPE_DTMC> gen(parser.context());
|
|||
|
|
typedef
|
|||
|
|
epoch::algorithm::IncrTarjan<epoch::solvers::PrismLogic,
|
|||
|
|
epoch::prism::Generator<epoch::prism::Context::PRISM_TYPE_DTMC>,
|
|||
|
|
epoch::graph::HashTable,
|
|||
|
|
epoch::graph::List,
|
|||
|
|
epoch::algorithm::LinearSystemExactParametricSolver> myTarjanPrism;
|
|||
|
|
myTarjanPrism mt(gen);
|
|||
|
|
|
|||
|
|
typename epoch::prism::Generator<epoch::prism::Context::PRISM_TYPE_DTMC>::State is(parser.context());
|
|||
|
|
for (epoch::prism::Context::BooleanVariableMap::const_iterator bi = parser.context().getBooleanVariables().begin() ; bi != parser.context().getBooleanVariables().end() ; ++bi) {
|
|||
|
|
if (!(bi->second->isInitialValueSpecified())) {
|
|||
|
|
std::cerr << "Initial value not specified for variable '" << *(bi->first) << "': assuming lowest value of its range" << std::endl;
|
|||
|
|
}
|
|||
|
|
is.m_BooleanVariables[bi->second->getIndex()] = bi->second->getInitialValue();
|
|||
|
|
}
|
|||
|
|
for (epoch::prism::Context::IntegerVariableMap::const_iterator ii = parser.context().getIntegerVariables().begin() ; ii != parser.context().getIntegerVariables().end() ; ++ii) {
|
|||
|
|
if (!(ii->second->isInitialValueSpecified())) {
|
|||
|
|
std::cerr << "Initial value not specified for variable '" << *(ii->first) << "': assuming lowest value of its range" << std::endl;
|
|||
|
|
}
|
|||
|
|
is.m_IntegerVariables[ii->second->getIndex()] = ii->second->getInitialValue();
|
|||
|
|
}
|
|||
|
|
for (epoch::prism::Context::DecimalVariableMap::const_iterator di = parser.context().getDecimalVariables().begin() ; di != parser.context().getDecimalVariables().end() ; ++di) {
|
|||
|
|
if (!(di->second->isInitialValueSpecified())) {
|
|||
|
|
std::cerr << "Initial value not specified for variable '" << *(di->first) << "': assuming lowest value of its range" << std::endl;
|
|||
|
|
}
|
|||
|
|
is.m_DecimalVariables[di->second->getIndex()] = di->second->getInitialValue();
|
|||
|
|
}
|
|||
|
|
for (epoch::prism::Context::ModuleMap::const_iterator mi = parser.context().getModules().begin() ; mi != parser.context().getModules().end() ; ++mi) {
|
|||
|
|
for (epoch::prism::Context::BooleanVariableMap::const_iterator bi = mi->second->getBooleanVariables().begin() ; bi != mi->second->getBooleanVariables().end() ; ++bi) {
|
|||
|
|
if (!(bi->second->isInitialValueSpecified())) {
|
|||
|
|
std::cerr << "Initial value not specified for variable '" << *(bi->first) << "': assuming lowest value of its range" << std::endl;
|
|||
|
|
}
|
|||
|
|
is.m_BooleanVariables[bi->second->getIndex()] = bi->second->getInitialValue();
|
|||
|
|
}
|
|||
|
|
for (epoch::prism::Context::IntegerVariableMap::const_iterator ii = mi->second->getIntegerVariables().begin() ; ii != mi->second->getIntegerVariables().end() ; ++ii) {
|
|||
|
|
if (!(ii->second->isInitialValueSpecified())) {
|
|||
|
|
std::cerr << "Initial value not specified for variable '" << *(ii->first) << "': assuming lowest value of its range" << std::endl;
|
|||
|
|
}
|
|||
|
|
is.m_IntegerVariables[ii->second->getIndex()] = ii->second->getInitialValue();
|
|||
|
|
}
|
|||
|
|
for (epoch::prism::Context::DecimalVariableMap::const_iterator di = mi->second->getDecimalVariables().begin() ; di != mi->second->getDecimalVariables().end() ; ++di) {
|
|||
|
|
if (!(di->second->isInitialValueSpecified())) {
|
|||
|
|
std::cerr << "Initial value not specified for variable '" << *(di->first) << "': assuming lowest value of its range" << std::endl;
|
|||
|
|
}
|
|||
|
|
is.m_DecimalVariables[di->second->getIndex()] = di->second->getInitialValue();
|
|||
|
|
}
|
|||
|
|
}
|
|||
|
|
epoch::solvers::PrismLogic F1("", parser.context(),pdr);
|
|||
|
|
epoch::solvers::PrismLogic F2("", parser.context(),pdr);
|
|||
|
|
|
|||
|
|
mt.launch(is, F1, F2);
|
|||
|
|
|
|||
|
|
}
|
|||
|
|
|
|||
|
|
*/
|
|||
|
|
|
|||
|
|
|
|||
|
|
// epoch::altarica::AltaricaInitInfoXML2 *aix2 = new epoch::altarica::AltaricaInitInfoXML2(jsonFile, gen.amodel_);
|
|||
|
|
// std::cout << aix2->toString();
|
|||
|
|
// exit(0);
|
|||
|
|
|
|||
|
|
|
|||
|
|
|
|||
|
|
|
|||
|
|
|
|||
|
|
exit(0);
|
|||
|
|
|
|||
|
|
|
|||
|
|
|
|||
|
|
|
|||
|
|
}
|
|||
|
|
catch (const boost::program_options::error& error) {
|
|||
|
|
std::cerr << error.what() << std::endl;
|
|||
|
|
return -1;
|
|||
|
|
}
|
|||
|
|
catch (const std::exception& error) {
|
|||
|
|
std::cerr << boost::diagnostic_information(error) << std::endl;
|
|||
|
|
return -1;
|
|||
|
|
}
|
|||
|
|
}
|