#
# Copyright (c) 2011, EPFL (Ecole Politechnique Federale de Lausanne)
# All rights reserved.
#
# Created by Marco Canini, Daniele Venzano, Dejan Kostic, Jennifer Rexford
#
# Redistribution and use in source and binary forms, with or without
# modification, are permitted provided that the following conditions are met:
#
#   -  Redistributions of source code must retain the above copyright notice,
#      this list of conditions and the following disclaimer.
#   -  Redistributions in binary form must reproduce the above copyright notice,
#      this list of conditions and the following disclaimer in the documentation
#      and/or other materials provided with the distribution.
#   -  Neither the names of the contributors, nor their associated universities or
#      organizations may be used to endorse or promote products derived from this
#      software without specific prior written permission.
#
# THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS "AS IS" AND ANY
# EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED TO, THE IMPLIED WARRANTIES
# OF MERCHANTABILITY AND FITNESS FOR A PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT
# SHALL THE COPYRIGHT HOLDER OR CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL,
# SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT LIMITED TO,
# PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF USE, DATA, OR PROFITS; OR BUSINESS
# INTERRUPTION) HOWEVER CAUSED AND ON ANY THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT
# LIABILITY, OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE
# OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.
#

import os
import sys
import multiprocessing

import logging
log = logging.getLogger("nice.mc")
log_stats = logging.getLogger("stats")
import utils
from stats import getStats
stats = getStats()

MODEL_CHECKER_DIR = os.path.abspath(os.path.join(os.path.dirname(__file__), "../model_checker"))

class ModelCheckerProcess(multiprocessing.Process):
	def __init__(self, config, queues):
		multiprocessing.Process.__init__(self, group=None, target=self.model_check)
		self.queues = queues
		self.config = config

	def model_check(self):
		stats.reset()

		sys.path = [MODEL_CHECKER_DIR, os.path.join(MODEL_CHECKER_DIR, "nox_lib")] + sys.path

		if self.config.get("runtime.debug_mc"):
			sys.stdin = open("/dev/stdin", "r") # multiprocess closes it
			from lib.model_checker import DebugModelChecker
		else:
			from lib.model_checker import ModelChecker
		from lib.strategies import strategies, RandomWalk
		from models import models
		import invariants.invariant_dispatcher as Invariants

		if not models.has_key(self.config.get("model.name")):
			utils.crash("Invalid model name: " + self.config.get("model.name") + ".\nValid model names are: "+ ', '.join(models.keys()))

		if not strategies.has_key(self.config.get("strategy.name")):
			utils.crash("Invalid strategy name: " + self.config.get("strategy.name") + ".\nValid strategy names are: "+ ', '.join(strategies.keys()))

		self.config.set("model.class", models[self.config.get("model.name")])
		self.config.set("strategy.class", strategies[self.config.get("strategy.name")])

		stats.pushProfile("model checker init")
		symbolic_options = {"queues": self.queues}

		if self.config.get("runtime.debug_mc"):
			mc = DebugModelChecker(self.config, symbolic_options)
		else:
			mc = ModelChecker(self.config, symbolic_options)

		stats.popProfile()

		try:
			stats.pushProfile("model checker run")
			mc.start()
		except KeyboardInterrupt:
			log_stats.error("INTERRUPTED!")
		finally:
			stats.popProfile()

			log_stats.info("--- Profiling info for model checker ---")
			log_stats.info("\n" + stats.getProfilingOutput())
			log_stats.info("--- Results ---")
			log_stats.info("Total states: %d" % (mc.unique_states_count + mc.old_states_count))
			log_stats.info("Unique states: %d" % mc.unique_states_count)
			log_stats.info("Revisited states: %d" % mc.old_states_count)
			log_stats.info("Maximum path length: %d" % mc.max_path_length)
			log_stats.info("Invariant violations: %d" % Invariants.countViolations())

			import invariants.invariant_dispatcher as Invariants
			grouped_v = {}
			all_invs = Invariants.invariants
			for i in all_invs:
				grouped_v[i.name] = [0, sys.maxint, 0]
			grouped_v["internal check"] = [0, sys.maxint, 0]
			for v in Invariants.violations:
				grouped_v[v.invariant_name][0] += 1
				if v.time_elapsed < grouped_v[v.invariant_name][1]:
					grouped_v[v.invariant_name][1] = v.time_elapsed
					grouped_v[v.invariant_name][2] = v.transitions

			for k in grouped_v:
				if grouped_v[k][0] > 0:
					log_stats.error("%-20s: %d violations (first found after %.2fs, %d transitions)" % (k, grouped_v[k][0], grouped_v[k][1], grouped_v[k][2]))
				else:
					log_stats.debug("%-20s: %d violations" % (k, grouped_v[k][0]))

			if self.config.get("runtime.graph") != None:
				mc.graph.saveToFile()

			if self.config.get("strategy.class") == RandomWalk:
				log_stats.warning("Random walk seed: %d", mc.strategy.seed)

