/*************************************************************************

    File: modelChecker1.pl
    Copyright (C) 2004,2005,2006 Patrick Blackburn & Johan Bos

    This file is part of BB1, version 1.3 (November 2006).

    BB1 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 2 of the License, or
    (at your option) any later version.

    BB1 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 BB1; if not, write to the Free Software Foundation, Inc., 
    59 Temple Place, Suite 330, Boston, MA  02111-1307  USA

*************************************************************************/

:- module(modelChecker1,[modelCheckerTestSuite/0,
                         info/0,
                         infix/0,
                         prefix/0,
			 evaluate/2,
			 evaluate/3,
			 satisfy/4]).

:- use_module(comsemPredicates,[memberList/2,
                                compose/3,
                                infix/0,
                                prefix/0,
                                printRepresentations/1]).

:- use_module(exampleModels,[example/2]).

:- use_module(modelCheckerTestSuite,[test/4]).


/*========================================================================
   Evaluate a formula in an example model
========================================================================*/

evaluate(Formula,Example):-
   evaluate(Formula,Example,[]).


/*========================================================================
   Evaluate a formula in an example model wrt an assignment
========================================================================*/

evaluate(Formula,Example,Assignment):-
   example(Example,Model),
   satisfy(Formula,Model,Assignment,Result),
   printStatus(Result).
   

/*========================================================================
   Test Suite
========================================================================*/

modelCheckerTestSuite:-
   format('~n>>>>> MODEL CHECKER 1 ON TEST SUITE <<<<<~n',[]),
   test(Formula,Example,Assignment,Status),
   format('~n~nInput formula:',[]),
   printRepresentations([Formula]),
   format('Example Model: ~p~nStatus: ',[Example]),
   printStatus(Status),
   format('~nModel Checker says: ',[]),
   evaluate(Formula,Example,Assignment),
   fail.

modelCheckerTestSuite.


/*========================================================================
   Print status of a testsuite example
========================================================================*/

printStatus(pos):- write('Satisfied in model. ').
printStatus(neg):- write('Not satisfied in model. ').
printStatus(undef):- write('Cannot be evaluated. ').


/*========================================================================
   Existential Quantification
========================================================================*/

satisfy(some(X,Formula),model(D,F),G,pos):-
   memberList(V,D),
   satisfy(Formula,model(D,F),[g(X,V)|G],pos).

satisfy(some(X,Formula),model(D,F),G,neg):-
   setof(V,(memberList(V,D),satisfy(Formula,model(D,F),[g(X,V)|G],neg)),Dom),
   setof(V,memberList(V,D),Dom).
   

/*========================================================================
   Universal Quantification
========================================================================*/

satisfy(all(X,Formula),Model,G,Pol):-
   satisfy(not(some(X,not(Formula))),Model,G,Pol).


/*========================================================================
   Conjunction
========================================================================*/

satisfy(and(Formula1,Formula2),Model,G,pos):-
   satisfy(Formula1,Model,G,pos),
   satisfy(Formula2,Model,G,pos).

satisfy(and(Formula1,Formula2),Model,G,neg):-
   satisfy(Formula1,Model,G,neg);
   satisfy(Formula2,Model,G,neg).


/*========================================================================
   Disjunction
========================================================================*/

satisfy(or(Formula1,Formula2),Model,G,pos):-
   satisfy(Formula1,Model,G,pos);
   satisfy(Formula2,Model,G,pos).

satisfy(or(Formula1,Formula2),Model,G,neg):-
   satisfy(Formula1,Model,G,neg),
   satisfy(Formula2,Model,G,neg).


/*========================================================================
   Implication
========================================================================*/

satisfy(imp(Formula1,Formula2),Model,G,Pol):-
   satisfy(or(not(Formula1),Formula2),Model,G,Pol).


/*========================================================================
   Negation
========================================================================*/

satisfy(not(Formula),Model,G,pos):-
   satisfy(Formula,Model,G,neg).

satisfy(not(Formula),Model,G,neg):-
   satisfy(Formula,Model,G,pos).


/*========================================================================
   Equality
========================================================================*/

satisfy(eq(X,Y),Model,G,pos):-
   i(X,Model,G,Value1),
   i(Y,Model,G,Value2),
   Value1=Value2.

satisfy(eq(X,Y),Model,G,neg):-
   i(X,Model,G,Value1),
   i(Y,Model,G,Value2),
   \+ Value1=Value2.


/*========================================================================
   One-place predicates
========================================================================*/

satisfy(Formula,model(D,F),G,pos):-
   compose(Formula,Symbol,[Argument]),
   i(Argument,model(D,F),G,Value),
   memberList(f(1,Symbol,Values),F),
   memberList(Value,Values).

satisfy(Formula,model(D,F),G,neg):-
   compose(Formula,Symbol,[Argument]),
   i(Argument,model(D,F),G,Value),
   memberList(f(1,Symbol,Values),F),
   \+ memberList(Value,Values).


/*========================================================================
   Two-place predicates
========================================================================*/

satisfy(Formula,model(D,F),G,pos):-
   compose(Formula,Symbol,[Arg1,Arg2]),
   i(Arg1,model(D,F),G,Value1),
   i(Arg2,model(D,F),G,Value2),
   memberList(f(2,Symbol,Values),F),
   memberList((Value1,Value2),Values).

satisfy(Formula,model(D,F),G,neg):-
   compose(Formula,Symbol,[Arg1,Arg2]),
   i(Arg1,model(D,F),G,Value1),
   i(Arg2,model(D,F),G,Value2),
   memberList(f(2,Symbol,Values),F),
   \+ memberList((Value1,Value2),Values).


/*========================================================================
   Interpretation of Constants and Variables
========================================================================*/

i(X,model(_,F),G,Value):-
   (
       var(X),
       memberList(g(Y,Value),G),
       Y==X, ! % IMPORTANT CUT!
   ;
       atom(X),
       memberList(f(0,X,Value),F)
   ).
   

/*========================================================================
   Info
========================================================================*/

info:-
   format('~n> ------------------------------------------------------------------------- <',[]),
   format('~n> modelChecker1.pl, by Patrick Blackburn and Johan Bos                      <',[]),
   format('~n>                                                                           <',[]),
   format('~n> ?- evaluate(F,E).          - evaluate a formula in a model                <',[]),
   format('~n> ?- evaluate(F,E,A).        - evaluate a formula in a model wrt assignment <',[]),
   format('~n> ?- modelCheckerTestSuite.  - run the test suite                           <',[]),
   format('~n> ?- infix.                  - switch to infix printing mode                <',[]),
   format('~n> ?- prefix.                 - switch to prefix printing mode               <',[]),
   format('~n> ?- info.                   - prints this information                      <',[]),
   format('~n> ------------------------------------------------------------------------- <',[]),
   format('~n~n',[]).


/*========================================================================
   Display info at start
========================================================================*/

:- info.

