Timed-Altarica-To-Fiacre-Translator/src/console/epochmain.cc

/*******************************************************************************
 * 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 <boost/filesystem.hpp>
#include <boost/program_options.hpp>
#include <boost/date_time/posix_time/posix_time.hpp>
#include <boost/exception/diagnostic_information.hpp>

#include "epochconsolealtarica.hh"

//using namespace epoch;

int main (int ac, char* av[])
{
	unsigned int verbosity; // verbosity level
	std::string modelFile;
	std::string initFile;
	double threshold;
	unsigned int dtimebound;
	double ctimebound;
	std::string var1, var2 ;
	std::string value1, value2;
	std::string f1;
	std::string f2;
	bool invert_comp1 = false;
	bool invert_comp2 = false;
	int algo, hess, blas;
	bool ds;
	int ps;
	bool printfunction = false;
	std::string printGraph;
	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")	
		("ps", boost::program_options::value<int>(&ps)->default_value(-1), "print states up to specified depth (0 for initial state only )")	
	
		("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")
		("algo",  boost::program_options::value<int>(&algo)->default_value(5), "algo:\n -1 => all\n  0 => exact infinite\n  1 => iterative infinite\n  2 => bounded exact infinite\n  3 => bounded iterative infinite\n  4 => finite\n  5 => bounded finite\n  6 => coutinuous exact\n  7 => continuous bounded\nINFINITE HORIZON + EXACT COMPUTATION + MARKOV CHAIN WITH INFINITE NUMBER OF STATES => STACK OVERFLOW")
		("hess", boost::program_options::value<int>(&hess)->default_value(0), "hess:\n 0 => triangular Hessenberg matrices\n 1 => banded Hessenberg matrices\n 2 => dense Hessenberg matrices")
		("blas", boost::program_options::value<int>(&blas)->default_value(0), "blas:\n 0 => Ublas Standard\n 1 => Ublas BLAS bindings (use system's BLAS implementation)")
		("verbosity", boost::program_options::value<unsigned int>(&verbosity)->default_value(0), "verbosity level")    
		("thres",  boost::program_options::value<double>(&threshold)->default_value(0.001), "threshold for P(f1 U f2) >= t")
		("dhor",  boost::program_options::value<unsigned int>(&dtimebound)->default_value(10), "discrete horizon time")
		("chor",  boost::program_options::value<double>(&ctimebound)->default_value(100.0), "continuous horizon time")
		("var1",  boost::program_options::value<std::string>(&var1)->default_value(""), "var1 to check (left side of until)")
		("value1", boost::program_options::value<std::string>(&value1)->default_value("false"),"value for variable1 (false -> var1 = false)")
		("var2",  boost::program_options::value<std::string>(&var1)->default_value(""), "var2 to check ( right side of until)")
		("value2", boost::program_options::value<std::string>(&value1)->default_value("false"),"value for variable2 (false -> var2 = false)")
		("f1", boost::program_options::value<std::string>(&f1)->default_value("true"), "left-hand side formula of strong until operator")
		("f2", boost::program_options::value<std::string>(&f2)->default_value("true"), "right-hand side formula of strong until operator")
		("neg1", " replaces = with != for left side of until")
		("neg2", "replaces = with != for right side of until")
		("pfunc", "print continuous probability function")
		("pg", "print the search graph in a dot file")
		;

	    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::notify(vm);
	    
		if (vm.count("help")) {
			std::cout << desc << std::endl;
			return 1;
		}

		if (vm.count("neg1")) {
		    invert_comp1 = true;
		}

		if (vm.count("neg2")) {
		    invert_comp2 = true;
		}

		if (vm.count("pfunc")) {
			printfunction = true;
		}

      
//		if (!var2.empty()) {
//			if (var1.empty())
//				f1 = "true";
//			else
//				f1 = var1 + ((!invert_comp1)?(" = "):(" != ")) + value1;
//			f2 = var2 + ((!invert_comp2)?(" = "):(" != ")) + value2;
//			std::cout << "f2: (" << f2 << ")" << std::endl;
//		} else {
//			std::cout << "f1: " << f1 << std::endl;
//			std::cout << "f2: " << f2 << std::endl;
//		}
		// std::cout << "for finite time algos, dtimebound = " << dtimebound<<std::endl;
		// std::cout << "threshold for property ="<<threshold<<std::endl;

		// Get file path
		boost::filesystem::path filepath(modelFile);

		if (vm.count("pg")) {
			printGraph = filepath.stem().generic_string() + "_" + boost::posix_time::to_iso_string(boost::posix_time::second_clock::local_time());
		}
		
		if (!filepath.has_extension()) {
			std::cerr << "File '" << filepath << "' has no extension!" << std::endl;
			return -1;
		} else if (filepath.extension().generic_string() == ".alt") { // altarica file
			return epoch::console::DoAltarica(modelFile, initFile, var1, value1, var2, value2, ds, ps, invert_comp1, invert_comp2,
					                          ac, av, algo, hess, blas, threshold, dtimebound, ctimebound, printfunction, printGraph);
		}
	}
	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;
	}
}