#! /usr/bin/env python
# -*- coding: iso-8859-15 -*-

# Contractor, a contract validation tool
#    Copyright (C) 2008  Guido de Caso, Alexis Tcach, Víctor Braberman, Diego Garbervetsky, Sebastián Uchitel
#    {gdecaso, atcach vbraber, diegog, suchitel}@dc.uba.ar
#    LaFHIS - Departamento de Computación - Facultad de Ciencias Exactas y Naturales - Universidad de Buenos Aires
#    Pabellón I - Ciudad Universitaria - (C1428EGA) - Buenos Aires - Argentina
#    Tel: +54-11-4576-3390 eext. 704
#
#    This program 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.
#
#    This program 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 this program.  If not, see <http://www.gnu.org/licenses/>.

import sys

from explore.explorator import explorator_main_interface

from feasability.query import query_main_interface

from model.fsm import FSM

from new_algorithm.explorer import explore

from old_algorithm.state_builder import build_states, build_initial_state
from old_algorithm.transition_builder import build_transitions

from reader.contract_parser import parse_contractor
from reader.options_parser import parse_options, Options

from stats.statistics import Statistics, print_statistics

from verifiers.reachable_states import restrict_to_reachable_states
from verifiers.unsat_elements import preconditions_unsat, postconditions_unsat

from writer.canonizer import canonize
from writer.fsm_writer import write_fsm

# parse command line arguments
parse_options()

# parse incoming contract
contract, fsm = parse_contractor(Options.options.file, Options.options) 

if Options.options.verbose:
	sys.stderr.write("CONTRACT:\n---------\n" + str(contract) + "\n")

if Options.options.explorator_state != None or Options.options.exploration_path != None:
	# We are in Explorator mode
	explorator_main_interface(contract)

elif Options.options.query_transition_model != None:
	# We are in QUERYING mode
	query_main_interface(contract)

else:
	# We are in ABSTRACTION CONSTRUCTION mode

	# check if the FSM was parsed, in that case we don't need to calculate it
	if fsm != None:
		if Options.options.verbose:
			sys.stderr.write("Using precalculated abstraction.\n")
	else:
		# we need to construct the abstraction

		# construct empty FSM
		fsm = FSM()

		if Options.options.old_algorithm:
			# old algorithm
			build_states(fsm, contract)
			build_transitions(fsm, fsm.states, contract)
			build_initial_state(fsm, contract)
		else:
			# new algorithm
			explore(fsm, contract)

	# canonize FSM if we need to
	if Options.options.canonical_output:
		restrict_to_reachable_states(fsm)
		canonize(fsm)
	
	if Options.options.verbose:
		sys.stderr.write("CVC VARS:\n---------\n" + contract.cvc() + "\n")
		sys.stderr.write("FSM:\n----\n" + str(fsm) + "\n")

	# check for unsat pre and postconditions
	preconditions_unsat(contract, fsm)
	postconditions_unsat(fsm)

	# write resulting FSM
	write_fsm(fsm, contract)
	
	# print statistics
	if Options.options.statistics:
		print_statistics()
		
