#
# 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.
#

# Using the module as a singleton

import time
import utils
import cPickle
import logging
log = logging.getLogger("nice.inv")
from stats import getStats
stats = getStats()

from invariants.return_continue_stop import ReturnContinueStop
from invariants.no_drop_invariant import NoDropInvariant
from invariants.no_forgotten_packets import NoForgottenPackets

DEFAULT_INVARIANTS = [ReturnContinueStop, NoDropInvariant, NoForgottenPackets]

def registerInvariant(inv): # inv is an instance, already initialized
	inv.reportViolation = reportViolation
	invariants.append(inv)

def testPoint(event_name, **args):
	for i in invariants:
		if hasattr(i, event_name + "_cb"):
			method = getattr(i, event_name + "_cb")
			try:
				method(**args)
			except TypeError:
				utils.crash("Invariant '%s', callback '%s' has wrong arguments. Passing %s" % (i.name, event_name+"_cb", str(args)))

def reportViolation(violation):
	global last_violation
	violation.time_elapsed = violation.timestamp - time_start
	violation.transitions = model_checker.good_transitions_count
	violation.unique_states = model_checker.unique_states_count
	violation.action_sequence = model_checker.current_replay_list[:] + [model_checker.next_action]
	violations.append(violation)
	new_violations = True
	if last_violation == None or last_violation.invariant_name != violation.invariant_name:
		log.critical("Invariant violation: " + repr(violation))
		last_violation = violation

def checkNewViolations():
	global new_violations
	ret = new_violations
	new_violations = False
	return ret

def countViolations():
	return len(violations)

def serializedState():
	return cPickle.dumps(invariants, -1)

# Initialization

time_start = time.time()
model_checker = None
invariants = []
violations = []
new_violations = False
for i in DEFAULT_INVARIANTS:
	i = i()
	registerInvariant(i)
last_violation = None

