/*
 * This file is part of PARAM.
 *
 * PARAM is free software: you can redistribute it and/or modify
 * it under the terms of the GNU General Public License as published by
 * the Free Software Foundation, either version 3 of the License, or
 * (at your option) any later version.
 *
 * PARAM is distributed in the hope that it will be useful,
 * but WITHOUT ANY WARRANTY; without even the implied warranty of
 * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
 * GNU General Public License for more details.

 * You should have received a copy of the GNU General Public License
 * along with PARAM.  If not, see <http://www.gnu.org/licenses/>.
 *
 * Copyright 2010 Ernst Moritz Hahn (emh@cs.uni-sb.de)
 */

#include <stdlib.h>
#include <sys/types.h>
#include <iostream>
#include <iomanip>
#include <istream>
#include <fstream>
#include <boost/program_options.hpp>
#include <limits>

#include "Controller.h"
#include "Statistics.h"
#include "LowLevelStateExplorer.h"
#include "rationalFunction/RationalFunction.h"
#include "RationalParser.h"

namespace parametric {
  using namespace std;
  using namespace Rational;
  using namespace boost;

  LowLevelStateExplorer::LowLevelStateExplorer(Controller &mc__) :
    mc(mc__) {
  }

  unsigned LowLevelStateExplorer::readNumStates(istream &stream) const {
    string line;
    getline(stream, line);
    vector<string> splitLine;
    istringstream iss(line);
    
    copy(std::istream_iterator<string>(iss),
         std::istream_iterator<string>(),
         back_inserter<vector<string> >(splitLine));
    
    if (2 != splitLine.size() || ("STATES" != splitLine[0])) {
      throw runtime_error("first line of low-level input file must be of"
			  " the form \"STATES <num-states>\"");
    }

    unsigned result(atoi(splitLine[1].c_str()));
    if (0 == result) {
      throw runtime_error("Invalid number of states.");
    }

    return result;
  }
  
  unsigned LowLevelStateExplorer::readNumTransitions(istream &stream) const {
    string line;
    getline(stream, line);
    vector<string> splitLine;
    istringstream iss(line);
    
    copy(std::istream_iterator<string>(iss),
         std::istream_iterator<string>(),
         back_inserter<vector<string> >(splitLine));
    
    if (2 != splitLine.size() || ("TRANSITIONS" != splitLine[0])) {
      throw runtime_error("second line of low-level input file must be of"
			  " the form \"TRANSITIONS <num-transitions>\"");
    }

    unsigned result(atoi(splitLine[1].c_str()));
    if (0 == result) {
      throw runtime_error("Invalid number of transitions.");
    }

    return result;
  }

  void LowLevelStateExplorer::readParameters(istream &stream, RationalParser &parser) {
    string line;
    getline(stream, line);
    if ("PARAM " != line.substr(0, 6)) {
      throw runtime_error("fifth line of low-level input file must be of"
			  " the form \"PARAM <param1> ... <paramp>\"");

    }
    parser.parseSymbols(line.substr(6));
  }

  void LowLevelStateExplorer::readInitStates(istream &stream) {
    string line;
    getline(stream, line);
    vector<string> splitLine;
    istringstream iss(line);
    
    copy(std::istream_iterator<string>(iss),
         std::istream_iterator<string>(),
         back_inserter<vector<string> >(splitLine));
    
    if (2 > splitLine.size() || ("INIT" != splitLine[0])) {
      throw runtime_error("third line of low-level input file must be of"
			  " the form \"INIT <state1> ... <staten>\"");
    }

    for (unsigned stateNr(1); stateNr < splitLine.size(); stateNr++) {
      unsigned init(atoi(splitLine[stateNr].c_str()));      
      if (0 == init) {
	throw runtime_error("Invalid initial state \"" + splitLine[stateNr] + "\"");
      }
      init--;
      mc.initStates.insert(init);
    }
  }

  void LowLevelStateExplorer::readTargetStates
  (istream &stream) {
    string line;
    getline(stream, line);
    vector<string> splitLine;
    istringstream iss(line);
    
    copy(std::istream_iterator<string>(iss),
         std::istream_iterator<string>(),
         back_inserter<vector<string> >(splitLine));
    
    if (2 > splitLine.size() || ("TARGET" != splitLine[0])) {
      throw runtime_error("fourth line of low-level input file must be of"
			  " the form \"TARGET <state1> ... <statem>\"");
    }

    for (unsigned stateNr(1); stateNr < splitLine.size(); stateNr++) {
      unsigned target(atoi(splitLine[stateNr].c_str()));      
      if (0 == target) {
	throw runtime_error("Invalid target state \"" + splitLine[stateNr] + "\"");
      }
      target--;
      mc.targetStates.insert(target);
    }
  }

  void LowLevelStateExplorer::readTransitions
  (istream &stream, unsigned numStates, unsigned numTransitions, RationalParser &parser) {
    unsigned lastFrom(1);
    while (!stream.eof()) {
      string line;
      getline(stream, line);
      if ("" != line) {
	istringstream iss(line);
	unsigned from;
	iss >> from;
	from--;
	unsigned to;
	iss >> to;
	to--;
	string restString;
	getline(iss, restString);
	RationalFunction prob(parser.parseRational(restString));
	if (lastFrom != from) {
	  mc.pmc->finishState();
	  if (lastFrom != from - 1) {
	    throw new runtime_error("Transitions must be ordered by source state.");
	  }
	}
	mc.pmc->addSucc(to, prob);
      }
    }
    mc.pmc->finishState();
  }

  void LowLevelStateExplorer::explore() {
    mc.statistics->exploreTime.start();
    string model_filename(mc.vm["model-file"].as<string>());
    string formula_filename;
    if (0 != mc.vm.count("formula-file")) {
      throw runtime_error("formula file disallowed for low-level models.");
    }

    mc.model_type = prismparser::DTMC;
    RationalParser parser;
    ifstream file(model_filename.c_str(), ifstream::in);
    const unsigned numStates(readNumStates(file));
    mc.pmc->reserveRowsMem(numStates);
    const unsigned numTransitions(readNumTransitions(file));
    mc.pmc->reserveColsMem(numTransitions);
    readInitStates(file);
    readTargetStates(file);
    readParameters(file, parser);
    readTransitions(file, numStates, numTransitions, parser);
    RationalFunction::removeUnusedSymbols();

    mc.statistics->numStatesModel = mc.pmc->getNumStates();
    mc.statistics->numTransitionsModel = mc.pmc->getNumTrans();
    mc.setAnalysisType(Controller::unboundedUntilAnalysis);
    mc.statistics->exploreTime.stop();
  }
}
