You selected impl12.pl


/* Nash implementation theory on prolog. Sep 2001--Dec 2002. */


% modified: 7,8 Jan 2003. to be compatible with swi-prolog version 5.
:- dynamic preference/3.
:- dynamic difference/3.
:- dynamic scc/3.
:- dynamic environment/3.
:- dynamic mechanism/3.
:- dynamic impl_stream/3.
:- dynamic br_stream/3.
:- dynamic br_result/1.
:- dynamic default_model/1.
:- dynamic true_state/1.
:- dynamic last_goal/1.
:- dynamic wsid_history/1.

% -----------------------------------------------------------  %
%   headline
% -----------------------------------------------------------  %

welcome:-
 wn(' /*--------------------------------------------------*/'),
 wn(' /*    A Nash implementation theory on Prolog.       */'),
 wn(' /*-------------- Sep 2001--Jan 2003 ----------------*/'),
 wn(' % file: impl12.pl      '),
 wn(' % author: Kenryo INDO  (Kanto Gakuen University)'),
 wn(' % Dept of Management, Faculty of Economics, Kanto Gakuen University.'),
 wn(' % ---This code has tested by Swi-prolog 1.9.0 and 5.0.9 partly.'),
 wn(' % ?- setup_domain : To setup the current domain model.'),
 wn(' % ?- test_impl : To test Nash implementability.'),
 wn(' % ?- test_nash : To generate nash equilibrium.'),
 wn(' % ?- wsid : What shall I do, instead of online help. ').
 %wn(' % ?-explain_me: telling stories.').


% -----------------------------------------------------------  %
%   A CommandLine User Interface
% -----------------------------------------------------------  %
% added: 25 Oct 2002.
% modified: 10 Nov 2002.
% modified: 27 Nov 2002. 
%  as for wsid(3), to check mechanism/3 instead of environment/3.
% modified: 8 Jan 2003.
%  rename of wsid_history/1 and to declare dynamic.

wsid:-
 nl,
 assert(wsid_history([0])),
 wn('%   1. modeling for preference and mechanism.'),
 wn('%   2. modeling for scc.'),
 wn('%   3. simulate mechanism.'),
 wn('%   4. end this menu.'),
 write('input number>'),
 read(Y),
 (member(Y,[1,2,3,4])->wsid(Y);wsid).
%
update_wsid(N):-
 wsid_history([N|_]).
update_wsid(N):-
 retract(wsid_history(H)),
 assert(wsid_history([N|H])).
%
wsid(4).
wsid(3):-
 update_wsid(3),
 (clause(mechanism(_,_,_),_)->true
  ; 
   (write('Please setup your domain and mechanism at first'),
    nl,wsid
   )
 ),
 write('----- simulating nash equilibrium ------'),
 nl,
 M=[[0,test_ne],[1,test_nash],[2,test_impl]],
 write('please selct a number from: '),nl,write(M),read(U),
 (member([U,A],M)->A;true).
 %wsid.  
wsid(2):-
 update_wsid(2),
 write('----- auto generating and testing for sccs ------'),
 nl,
 gen_test_sccs.
wsid(1):-
 update_wsid(1),
 wn('%   1. see current preference domain.'),
 wn('%   2. setup preference domain and mechanism.'),
 wn('%   3. modeling new scc by self.'),
 wn('%   4. go back previous menu.'),
 write('input number>'),read(Y),
 (member(Y,[1,2,3,4])->wsid([1,Y]);wsid(1)).
wsid([1,4]):-
 wsid.
wsid([1,1]):-
 update_wsid([1,1]),
 Goal=display_domain(user),
 Goal,wsid.
wsid([1,2]):-
 update_wsid([1,2]),
 domain_models(Ds),
 Goal=setup_domain(U),
 %hear(domain,D),
 write('input domain name'),read(U),
 ((member(U,Ds) -> Goal); (U = end -> true)
  ;(	write('no such domain. please select from below, or b to go back.'),
	nl,write(Ds),nl,wsid([1,2]))
 ),wsid.
wsid([1,3]):-
 update_wsid([1,3]),
 write('Edit your file.'),
 wsid.

explain_me:-
 nl,
 wn('%   1. Basic Model for Preference and Scc '),
 nl,
 %write('read this section?(y/n) '),read(U1),
 U1=y,
 (U1=y->(
  wn('% This program simulates Nash Implementation Theory on Prolog machine.'),
  wn('% I have developed and tested on this program using SWI-Prolog version 1.9.0.'),
  wn('% The most basic data is preference/3, the model of rational preference orderings of each agent under each state, and scc/3, the model of social choice correspondences.'),
  wn('% Also, prefer_to/4 and its varsions represent the binary relations for pairwise comparison of outcomes.'),
  wn('% Several examples of preference domain model has cited from books in our reference list, including some vary small unrestricted domains, ud22, ud 23, ud33.'),
  wn('%  To see Sccs available, enter sccs(F). '),
  wn('%  Especifically, mr, the scc for N=2 which is an implementable example as insisted in Moore-Repullo(1990).')
 );true),
  nl,
  wn('%   2. Simulating Nash Implementation '),
  nl,
  write('read this section?(y/n) '),read(U2),
 (U2=y->(
   wn('% Up to now, the available mechanisms in this system are gM(Maskin-Vind), gD(Daniov), gMR and gMR2(Moore-Repullo,Dutta-Sen) only. '),
  wn('% You have need to prepare the preference model in this file and reload it, and then to specify Scc before simulation bellow. '),
  wn('% To test Nash-implementability via simulation, type after prompt "?- " as follows. '),
  wn('%   test_impl(gM,F,_Is,full(_),O) and return key if 3-person case, '),
  wn('%   test_impl(gD,F,[I,J],full(_),O) and return key if 2-person case, '),
  wn('%  where you must specify F, the variable for SCC. '),
  tab(4),wn(' *** Tools for Simulation and Its Results  ****'),
  wn('%  The output file will created automatically, as for test_impl/5.'),
  wn('%  And you may print any goal by using results_to_file/3 in this source program. '),
  wn('%  If you want to output file the results for any goal, it may useful by using results_to_file/3, or tell_test/1 for any goal.')
 );true),
  nl,
  wn('%   3. Testing for Scc and Domain '),
  nl,
  write('read this section?(y/n) '),read(U3),
 (U3=y->(
   wn('%  Insted of verifying Nash implementability by simulation,  you may test for the representative properties for sccs, such as monotonicity, nvp, unanimity, pareto optimality, essential monootnicity, individulal rationality, MR property, condition mju and so on, and for domain models such as condititon D. '),
   wn('%  To test the scc for its properties, use tests_for_scc/3.'),
   wn('%   tests_for_scc(F,[I,J],Properties) and return key if 2-person case, '),
   wn('%  To test the domain model for its properties, use tests_preference/5.'),
   wn('%   test_preference(Profs,F,[J,K],[G1,G2,G3,...],[NG3,NG4,...])  %')
 );true),
   nl,
   wn('%   4. Generating-and-Testing Automatically '),
   nl,
   write('read this section?(y/n) '),read(U4),
 (U4=y->(
 %
   wn('%  You can generate all sccs and enumeratively test, by gen_test_sccs/3.'),
   wn('%  And you can generate sccs with any desirable set of properties on the fixed domain model, by gen_test_sccs/3.'),
   wn('%  You can model or generate any possible, but unristricted up to now, preference domain by using gen_test_preference/6 with any desirable set of properties on the fixed scc of which you have need to specify it.')
  %
 );true),
  nl,
  wn('%   Reference '),
  nl,
  write('display reference list?(y/n) '),read(U5),
 (U5=y->reference_list;true).

/*
  %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
  %  display the reference list 
  %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
*/
% edited: 30 Aug 2002.
 
reference_list:-
   write('short or long? (s/l/v(very short))'),
   read(U),
   forall(
     ref(Sig,
	  Author,Year,Title,JournalOrBook,VolNoPage,Commnent
	),
      (
	Short = [Author,Year,Title],
	Add = [JournalOrBook,VolNoPage,Commnent],
	append(Short,Add,Long),
	( U = v -> vshort_refer(Sig,Short);
	  U = s -> short_refer(Sig,Short);
	  long_refer(Sig,Long)
	)
      )
   ),
   nl,
   wn('% ------------------------------------------------------------ %'),
   wn('You may refer any reference specified by [Sig] ,the brief name,'),
   wn('which is appear in the left upper corner.'),
   wn('In order to redisplay the specific one, or to cite in your code, type: '),
   wn('  short_refer(Sig, X) or long_refer(Sig, X).'),nl.

vshort_refer(Sig,[Author,Year,Title]):-
	ref(Sig,Author,Year,Title,_J,_P,_C),
	write([Sig]),tab(3),
	write(Author),
	write('('),
	write(Year),
	wn('). ').
short_refer(Sig,[Author,Year,Title]):-
	ref(Sig,Author,Year,Title,_J,_P,_C),
	wn([Sig]),tab(3),
	write(Author),
	write('('),
	write(Year),
	write('). '),
	wn(Title).
long_refer(Sig,[A,Y,T,JournalOrBook,VolNoPage,Commnent]):-
	ref(Sig,A,Y,T,JournalOrBook,VolNoPage,Commnent),
	short_refer(Sig,[A,Y,T]),
	write(JournalOrBook),
	wn(VolNoPage),
	((var(Commnent);Comment='')->true;wn(Comment)).



ref(head,'reference:').
ref(jp(01),
	 'M.O. Jackson and T.R. Palfrey',
	 2001,
	 'Voluntary implementation.',
	 'JET',
	 '98:1-25.',
	 'Especially, the example 1 (Voting) in Jackson and Palfrey (2001).'
	).
ref(d(92),
	'V. Danilov',
	1992,
	'Implementation via Nash equilibria.',
	' Econometrica',
	' 60(1):43-56.',_).
ref(mr(90),
	'J. Moore and R. Repullo',
	1990,
	'Nash implementation: A full charaterization.',
	'Econometrica',
	'58(5):1083-99.',_).
ref(ds(91),
	'B. Dutta and A. Sen',
	1991,
	'A necessary and sufficient condition for two-person Nash implementation.',
	'Review of Economic Studies',
	'58:121-8.',_).
ref(m(93),
	'J. Moore',
	1993,
	'Implementation, contracts, and renegotiation in environments with complete information.',
	'In J.-J. Laffont (ed.), Advances in Economic Theory, Cambridge University Press.',
	'pp.182-282.',_).
ref(ms(02),
	'E. Maskin and T. Sjostrom',
	2002,
	'Implementation theory.',
	'In K. Arrow, A. Sen, and K. Suzumura (eds.), Handbook of Social Choice and Welfare, Vol. 1, North-Holland',
	'pp.237-288.',_).
ref(m(99),
	'E. Maskin',
	1999,
	'Nash equilibrium and welfare optimality.',
	'Review of Economic Studies',
	'66:23-38.',_).
ref(sj(91),
	'T. Sjostrom',
	1991,
	'On the necessary and sufficient conditions for Nash implementation.',
	'Social Choice and Welfare',
	'8:333-40.',_).
ref(y(92),
	'T. Yamato',
	1992,
	'On Nash implementation of social choice correspondences.',
	'Games and Economic Behavior',
	'4:484-92.',_).
ref(p(98),
	'B. Peleg',
	1998,
	'Effective functions, game forms, games, and rights.',
	'Social Choice and Welfare',
	'15:67-80.',_).
ref(saijo(88),
	'T. Saijo',
	1988,
	'Strategy space reduction in Maskins theorem: Sufficient conditions for Nash implementation.',
	'Econometrica',
	'56(3):693-700.',_).
ref(suh(96),
	'S.-C. Suh',
	1996,
	'An algorithm for checking strong Nash implementability.',
	'Journal of Mathematical Economics',
	'25:109-22.',_).


edit_history:-
  wn(H1),H1='% editorial history:',
  wn('% created: 20-21 Sep 2001  "checking monotonicity" for SCCs.'),
  wn('% modified: 28-30 Sep   "cannonical(Maskin-Vind) mechanism, rule 1."'),
  wn('% modified: 3-4 Oct  "For n=3, rules 1,2,3 have almost done."'),
  wn('% modified: 5-8 Oct  "Nash strategy" for players, and gM rules.'),
  wn('% modified: 10-11 Oct  "br_defeasible/5" and "nash/5" has been debugged.'),
  wn('% modified: 12-13 Oct  "br_defeasible/6","mutate/5" have modified and '),
  wn('% modified: 14 Oct  "best_response/5"and  "nash/5" has completed.'),
  wn('% modified: 18 Oct  "lcc/3" added, and "monotone/1" has modified.'),
  wn('% modified: 19 Oct  "ess/4","is_essential/4","ess_monotone/1" has added.'),
  wn('% and "nash/5" has modified.'),
  wn('% modified: from 19 to 26 Dec totally debugged including "nash"'),
  wn('% modified: from 27 to 31 Dec "test_impl" and several to write stream.'),
  wn('% modified: 1-4,17-20 Jan 2002  blocking, test_block, test_proposition.'),
  wn('% modified: 20-22 Jan 2002  beta_blocking. individual rationality.'),
  wn('% modified: 23-28 Jan 2002  2-person case: MR-property, prefer_profile.'),
  wn('% modified: 29-31 Jan 2002  2-person case: Danilov mechanism gD.'),
  wn('% modified: 1-3 Feb 2002  gM, test_impl, test_nash, gD, ess, blocking.'),
  wn('% modified: 4-7 Feb 2002  game_forms and mechanism for gD.'),
  wn('% modified: not yet 18- Feb 2002  nash, test_impl for gD.'),
  wn('% modified: 27-30 Apr 2002  mechanism, nash, test_impl for gM and for gD.'),  wn('% modified: 1-9 May 2002 "impl06.pl"  totally bug fixed and generalized for gM and gD both, N-person nash, test_impl and so on. '),

  wn('% modified: 16 May 2002  simple mechanism for nash equilibrium test.'),

  wn('% modified: 23 Jul 2002  is_blocked_by/6, blockings/4,is_I_rational/4.'),

  wn('% modified: 25-28 Jul 2002  is_I_rational/4, i_rationals/5, is_MR...'),

  wn('% modified: 29 Jul--1 Aug 2002  new test routines for scc0, auto-generated, including results_to_file/3'),

  wn('% modified: 1-7 Aug 2002  Moore-Repullo example, difference/3, prefer_to/4, and related parts.'),

  wn('% modified: 9-10 Aug 2002  Moore-Repullo mechanism,test_dan55/1,test_sa/1.'),

  wn('% modified: 11-13 Aug 2002  gen_test_sccs for a simple universal domain, ud22,partially, m=3.'),

  wn('% modified: 15 Aug 2002  Pareto property, dictator, NVP, unanimity'),

  wn('% modified: 17-9 Aug 2002  unified mechanism, restricted VP, bad_outcome, nonempty_lower_intersection, minimal liberalism, ud32, an aproximated universal domain,  added the dictatorial sccs in ud22 and tested.'),

  wn('% modified: 20-23 Aug 2002  condition_D by Yamato(1992), difference/3 and strict_prefer_to/4,  B_k/star,C_k/star,conditions mju/mju2, M/M2, by Sjostrom. Suhs mechanism for storong implementation has started, but only partially.'),

  wn('% modified: 24-26 Aug 2002  gMR and gMR2, the Moore-Repullo-Dutta-Sen mechanism. modified several test routines including  tell_test, mtest, auto_preference, gen_test_preference.'),

  wn('% modified: 27-28 Aug 2002  the several bugs fixed. gD message has to include the empty set. The remaining five implementable sccs umd1--5 in ud22 has added and M2 tested. the impossibility  result of N=2 has verified for simple domain model ud22 where without nul outcome scc. '),

  wn('% modified: 29 Aug 2002  As for the game forms of gD and test_nash, best_reponse, mutate (allowing equality) have bug fixed respectively. And the roulette, previously its choice range of using dictatorship has wrong, has corrected and separated from these forms. I also fixed that findall, insted of setof, used in check_on_scc, check_off_scc, in order to pass, without fail, the check for the empty set.'),

  wn('% modified 30-31 Aug 2002  the part of roulette and dictatorship in gD and nash and test_nash has bug fixed. setup_domain/1 as auto setup for preference domain. reference_list/0 as auto display for the reference. New testing method for mechanism outcomes stored into a file, via verify_messages/4, and nash and test_nash has modified to use this message file in order for some computational efficiency. %'),


  wn('% modified 1-2 Sep 2002  some routines for permutation of outcomes and neutrality/2 for scc. Version up the file name to impl09.pl. gen_test_neutral and gen_test_condMju have added. the rules 2-6 of gMR2 has modified.  %'),

  wn('% modified 3-7 Sep 2002  test routines for nash outcomes which includes test_nash, nash, bset_response and the message profile routines for each of mechanisms have edited. I intend that the system to be decomposed into 8 modules, but it is postponed. gD has a bug in dictatorship with pre-verified messages. Because of the hidden true state, message verification was incomplete. %'),

  wn('% modified 8-24 Sep 2002  Three papers with regarding this experimental system has been written by me, two-long, one-short. (And now I am intending one more important.) During authorizing them, I noticed a bug and has fixed it, e.g., the message profiles for Maskin mechanism, have the gen_test_sccs /3 to save its results as the clauses, and added some routines such that extract_em /3, extract_sccs /4, and tell_all_pred /0 for the convienience of the analysis. %'),

  wn('% modified 25 Sep 2002  contract_domain /3, related to condition_D /2, has modified. It is now possible to auto-generate a domain that satifies condition D by means of contracting the subset of states from any domain. %'),

  wn('% modified 26-8 Sep 2002  The predicates that related to condition_mju, condition_M, their subconsitions, including anew collect_cx /7, and that related gen_sccs have modified.  %'),

  wn('% modified 1-24 Oct 2002  a command user interface wsid has added. And several predicates related to  gen_sccs have modified so that they have an arity 0 version as the command line interface. A bug of gM as for non-0-integer messages, by using lpom, has detected and it has been tried to fixed but done partially up to now. %'),

  wn('% modified 25 Oct 2002  a command user interface of toplevel menu wsid / 0 and of setup_domain /1 have modified. hear /2 has added to the latter so that the online-mode of simulated mechanisms to be permitted in our system. And so verify_message_file has renemed and dichotomized into verify_messages(file) and verify_messages(online). test_ne /0,5, nec /1, ne /4, and br /6 have added. %'),

  wn('% modified 10 Nov 2002  wsid / 0 has minorlly modified. A bug of mechanism simulation has fixed. gen_test_mju has modified and test_mju has separated from it. display scc has extended by including condition mju. Tentative comments in condition mju has suppressed. %'),

  wn('% modified 10-12 Nov 2002 The online mode mechanism /3 has modified with a cut operator. lpom / 4 has extended so that you may select to set integer or only to extract the integer part of a message profile optionally. %'),

  wn('% modified 26 Nov 2002 Updated version impl11.pl because of this month. Almost same as imple10.pl but for a bug fixed in verify_messages, a missing argument in the strucure of lpom, and some minor bugs in game_forms of rule 2 and rule 3 of gM. However, lpom has not yet been enabled.%'),

  wn('% modified 27 Nov 2002 a bug fix in mtest_z0 of gMR and gMR2, a missing bit argument after 0 argument. The expost integer-setting added in the 2nd rule of game_form of gMR2. And update_env/1 has separated from update_messages. %'),

  wn('% modified 2-5 Dec 2002 a bug fix about online-mode, including game_form(gM(2)), mechanism /4, best_response /5 and update_messages /3 for online mode. %'),

  wn('% modified 8-10 Dec 2002 a bug fix on the rule 1 and 2 of game_form gM. %'),

  wn('% modified 29 Dec 2002 some bugs fix, or recovered the previous state. It is rather late in the day to made, a bag on the rule 3 of game_form gM and mr_message. Both mode of delay and of reduce for message spaces in setup_domain (verify_messages) has abolished. Instead, online mode test plays the role partially. I devised a little intelligence to communicate with user. That is the prerequisite model parameter in environment and default_model will be passed to test_nash and test_impl in the background and so as to prevent unintended abend when user type mismatch such context params in. And the online generated outcomes by mechanism /3 temporally specified instead of those which by setup_domain enabled. %'),

  wn('% modified 30-31 Dec 2002 a bug fix in game_form 3 of gMR. Truth-telling mode in test_nash, and test_impl, etc. has added. %'),

  wn('% modified 1-3 Jan 2003  Some simplifications in best_response, nash, test_nash, test_impl and etc, including that the mode part has abolished, in order to get rid of instability in mechanism simulations. A time stamp has added but not appropriately behave in version 1.9.0. %'),

  wn('% modified 4-5 Jan 2003  a bug fix. lpom/4 and the rule 3 of gM (and gMR) of integer part and the position of a cut operator. A simplification of best_response.  %'),

  wn('% modified 6-7 Jan 2003  a bug fix. A delicate backtrak problem of mechanism /3 in best_response, which has at first fixed 3 Dec 2002.  A debug for the rule 2 of gM. And with a debug of check_truth_telling, the inappropriate use of mtest, in test_nash, to generate truthful messages which yield the scc outcomes for each state has modified. %'),

  wn('% modified: 8 Jan 2003. the system to be compatible partly with swi-prolog 5.0.9. a bug fix in the rule 2 of gM and gMR. a bug fix. mechanism/3, which was not allowed by privious modification in last September, to be free to generate outputs by mtest. %'),

 wn('% end of editorial history.').


wn(X):-write(X),nl.
wn(Strm,X):-write(Strm,X),nl(Strm).


% -----------------------------------------------------------  %
%%%%%% save data for all predicates in this system %%%%%%%
% -----------------------------------------------------------  %
% added: 24 Sep 2002.
tell_all_pred:-
    tell_test(
	forall(
	  (
           impl_pred(P)
	  ),
	  (
	   P=..[X|Z],
 	   %current_functor(X,Y)
	   length(Z,L),
	   write(X),write(' / '),
	   write(L),nl
	  )
	)
    ).

impl_pred(P):-predicate_property(P,file('/c:/decision/pl/bin/impl09.pl')).



% -----------------------------------------------------------  %
%%%%%% some set and other basic operations %%%%%%%
% -----------------------------------------------------------  %

% warning:  in this version I use several incorporated predicates
% of SWI-prolog, (my_)maplist, nth1,nth0, and numbervars, 
% which may not work on your prolog system.
% However, probabily it is easy for you to write the first two of them.
% Since numbervars is foreign, this is not easy, but I use it only 
% in generating, ud32, a small sample domain model. (ud32 is described later.) 

%--
/* apply /2 : not found in If-Prolog */
my_apply(A,B):-C=..[A|B],C.

/*  same as maplist /3,select /3, and  sublist / 3of SWI-prolog  */ 
my_maplist(_A, [], []).
my_maplist(A, [B|C], [D|E]) :-
        apply(A, [B,D]),
        my_maplist(A, C, E).

my_select([A|B], A, B).
my_select([A|B], C, [A|D]) :-
        my_select(B, C, D).

my_sublist(_A, [], []) :- !.
my_sublist(A, [B|C], D) :-
        apply(A, [B]), !,
        D = [B|E],
        my_sublist(A, C, E).
my_sublist(A, [_B|C], D) :-
        my_sublist(A, C, D).


/* nth0 and nth1 of SWI-prolog. if you need to write, use this.

nth1(A, B, C) :-
        integer(A), !,
        D is A - 1,
        nth0_1(D, B, C).
nth1(A, B, C) :-
        var(A),
        nth0_2(D, B, C),
        A is D + 1.
nth0(A, B, C) :-
        integer(A), !,
        nth0_1(A, B, C).
nth0(A, B, C) :-
        var(A), !,
        nth0_2(A, B, C).
nth0_1(0, [A|B], A) :- !.
nth0_1(A, [B|C], D) :-
        E is A - 1,
        nth0(E, C, D).
nth0_2(0, [A|B], A).
nth0_2(A, [B|C], D) :-
        nth0_2(E, C, D),
        succ(E, A).
*/


% a sequence of binary choice for a list:
%--------------------------------------------------
% projection(3rd ar) of vector(2nd ar) using a sequence of digits(1st ar). 
% you must specify the second ('a base set') argument.
% this predicate is important so that it is used in subset_of /3.
list_projection([],[],[]).
list_projection([X|Y],[_A|B],C):-
   X = 0,
   list_projection(Y,B,C).
list_projection([X|Y],[A|B],[A|C]):-
   X = 1,
   list_projection(Y,B,C).

% added: 15 Oct 2002. 
plist_projection(P,A,[],[]):-
   list_projection(P,A,[]).
plist_projection(P,A,C,C1):-
   list_projection(P,A,C1),
   C1\=[],
   permutation_of(C1,C,_N).



% count frequency of occurence of the specified value of variable, M.
% -----------------------------------------------------------  %
% note: Both of M and L have to be specified.

counter(N,M,L):-
    length(L,_),
    findall(M,member(M,L),Mx),
    length(Mx,N).



% equality for pair of set
% -----------------------------------------------------------  %
% an old version.
seteq(X,Y,L):-
   length(X,L),
   length(Y,L),
   forall(member(Z,X),member(Z,Y)),
   forall(member(Z,Y),member(Z,X)).
% edited: 15 Nov 2002.
seteq(X,Y):-
   sort(X,Sort),
   sort(Y,Sort).

% subset_of/3 : useful for subset-enumeration 
% -----------------------------------------------------------  %
subset_of(A,N,As):-
   length(As,L),
   length(D,L),
   list_projection(D,As,B),
   length(B,N),
   sort(B,A).

%subset_of(A,N,As):-multiple_subset_of(A,N,As).

% subset allowing multiple membership 
% -----------------------------------------------------------  %
multiple_subset_of([],0,_):-!.
multiple_subset_of([X|A],N,As):-
   length([X|A],N),
   multiple_subset_of(A,N1,As),
   member(X,As),
   N is N1 + 1.



% set of all subsets 
% -----------------------------------------------------------  %
powerset_of(X,A):-
   length(A,_),
   findall(Y,N^subset_of(Y,N,A),X1),
   sort(X1,X),!. 

% descending/ascending natural number sequence less than N.
% -----------------------------------------------------------  %
desc_nnseq([],N):-N<0,!.
desc_nnseq([0],1).
desc_nnseq([A|Q],N):-
   A is N - 1,
   length(Q,A),
   desc_nnseq(Q,A).
asc_nnseq(Aseq,N):-desc_nnseq(Dseq,N),sort(Dseq,Aseq).

% bag0/3 : allow multiplicity
% -----------------------------------------------------------  %
bag0([],_A,0).
bag0([C|B],A,N):-length([C|B],N),bag0(B,A,_N1),%N is N1 + 1,
  member(C,A).

% bag1/3 : do not allow multiplicity
% -----------------------------------------------------------  %
% modified: 15 Oct 2002. bag fixed for unboundness.

bag1([],_A,0).
bag1([C|B],A,N1):-
  \+var(A),
  length(A,L),
  asc_nnseq(Q,L),
  member(N,Q),
  length(B,N),bag1(B,A,N),N1 is N + 1,
  member(C,A),\+member(C,B).

% ordering/3
% -----------------------------------------------------------  %
ordering(A,B,C):-bag1(A,B,C).


% permutation.
% -----------------------------------------------------------  %
% modified: 1 Sep 2002. to be used in is_neutral/2. 
% modified: 15 Oct 2002. add a non-variable constraint for the base set A. 

% permutation of alternatives.
poa(P,APs):-
   alternatives(A),
   permutation_of(A,P,APs).

permutation_of(A,P,APs):-
   \+var(A),
   length(A,M),
   ordering(P,A,M),
   asc_nnseq(Qm,M),
   my_maplist(nth_of_permutation(A,P),Qm,APs).

%caution:
%notations 'A->B's bellow have cause precedence errors in IF-prolog.

nth_poa(P,K,Ak->Pk):-
   alternatives(A),
   nth_of_permutation(A,P,K,Ak->Pk).
nth_of_permutation(A,P,K,Ak->Pk):-
   length(A,M),
   ordering(P,A,M),
   nth0(K,A,Ak),
   nth0(K,P,Pk).

permutate_of_order(PoA,[Q->R]):-
   poa(_P,PoA),
   alternatives(A),
   length(A,M),
   ordering(Q,A,M),%wn(Q),
   ordering(R,A,M),%wn(R),
   permutation(Q,PoA,R).

permutation([],[],[]).
permutation(Q,[A->P|PoA1],R):-
   subtract(Q,[A],Q1),nth1(K,Q,A),
   subtract(R,[P],R1),nth1(K,R,P),
   permutation(Q1,PoA1,R1).


% projection operator via index set. (an exchange economy?)
% choice1 from base1 :: choice2 from base2.
% modified : 15 Oct 2002. to be order-neutral (pending:-)
% 
pcm([Choice1,Base1],[Choice2,Base2]):-
    pairwise_contract_map([Choice1,Base1],[Choice2,Base2]).


pairwise_contract_map([Choice1,Base1],[Choice2,Base2]):-
  %  length(Base1,N2),
  %  length(Base2,N2),
    subset_of(Choice1,N1,Base1),
    subset_of(Choice2,N1,Base2),
    list_projection(Project,Base1,Choice1),
    list_projection(Project,Base2,Choice2).

% ppcm /2 using plist_projection 
% added: 15 Oct 2002.
ppcm([Choice1,Base1],[Choice2,Base2]):-
    subset_of(C1,N1,Base1),
    subset_of(C2,N1,Base2),
    plist_projection(Project,Base1,Choice1,C1),
    plist_projection(Project,Base2,Choice2,C2).


% replace(Project,Goal,Base,Goal1):-
% -----------------------------------------------------------  %
% added: 15 Oct 2002.
  % a sequence of replacement of a subset of elements in Goal 
  % which specified by a list, Project, 0-1^n, over Base 
  % a list of length n, which brings about Goal1.
  % X=1 --> preserve the original. X=0 --> do replace.
replace([],[],[],[]).
replace([X|A],[_|B],[Z|C],[Z|D]):-
   X = 0,
   replace(A,B,C,D).
replace([X|A],[Y|B],[_|C],[Y|D]):-
   X = 1,
   replace(A,B,C,D).


% sum
% -----------------------------------------------------------  %
sum([],0).
sum([X|Members],Sum):-
   sum(Members,Sum1),
   number(X),
   Sum is Sum1 + X.

% ゴールの重複度を調べる。
% -----------------------------------------------------------  %
sea_multiple(Goal,Cond,N,M):-
  Clause=..Goal,
  findall(Cond,Clause,Z),length(Z,N),sort(Z,Q),length(Q,M).

% concatenate for list elements 
% -----------------------------------------------------------  %
concat_v([],'',0).
%concat_v([b,c],Z,2):-length([c],1),concat_v([c],c,1),concat(b,c,Z).
%concat_v([a,b,c],Z,3):-length([a,c],2),concat_v([b,c],bc,2),concat(a,bc,Z).
concat_v([X|Y],Z,L):-concat_v(Y,Z1,L1),length(Y,L1),L is L1 + 1, concat(X,Z1,Z).

% 差分リスト(参考)
concat_dl(A-B,B-C,A-C).

/* sample executions

 ?- concat_dl([a,b|X]-X,[c,d|Y]-Y,R).
X = [c,d|G1172]
Y = G1172
R = [a,b,c,d|G1172] - G1172 
Yes

 ?- concat_dl([a,b|X]-X,[c,d|[]]-[],R-[]).
X = [c,d]
R = [a,b,c,d] ;

 ?- concat_dl([a,b|X]-X,X-[],[a,b,c,d]-[]).
X = [c,d]

 ?- concat_dl(A,[c,d|[]]-[],[a,b,c,d]-[]).
A = [a,b,c,d] - [c,d] 
Yes
*/



% -----------------------------------------------------------  %
% Tools for write the results of executing any goal to file. 
% -----------------------------------------------------------  %
%   save to file the test-run results for any goal
% modified: 23 Sep 2002.
% modified: 28 Sep 2002. augmented with tell_test.
% modified: 18 Oct 2002. to_file, an alias.

to_file:-
   results_to_file.
results_to_file:-
   tab(5),write(' input your goal'),read(U1),
   tab(5),write(' output file'),read(U2),
   concat(U2,'.txt',File),
   U1=..Goal,
   tab(5),write(' tell file ? (y/n) '),read(U3),
   (U3=y->Tell=tell;Tell=no),
   results_to_file(Goal,Tell,File,_S).

to_file(_Goal,_,File,S):-
   results_to_file(_Goal,_,File,S).
results_to_file(_Goal,_,File,S):-
  \+current_stream(File,write,S),
  write('Now opening output file:'),wn(File),
  wn('Please type semicron ; after prompt'),
  open(File,write,S).
  %fail.

results_to_file(_Goal,tell,_File,_):-
  \+current_stream('res_tell.txt',write,Strm),
  open('res_tell.txt',write,Strm),
  tell('res_tell.txt'),
  fail.

results_to_file(Goal,_Both,File,S):-
  current_stream(File,write,S),
  %Goal=[_G,_A,_B,_Is],
  Goal1=..Goal,
  Goal1,
  wn(Goal1),
  write(S,Goal1),write(S,'.'),nl(S),
  fail.

results_to_file(_Goal,tell,_File,_):-
  current_stream('res_tell.txt',write,Strm),
  close(Strm),
  tell(user),
  fail.

results_to_file(_Goal,_Both,File,S):-
  current_stream(File,write,S),
  write(S,end_of_run),nl(S),
  write('Now closing output file:'),wn(File),
  wn('Please type enter key after prompt'),
  close(S).


% using tell/1 in order to change the standard output to file.

tell_test(Goal):-
  open('tell.txt',write,S),
  tell('tell.txt'),
  Goal,
  current_stream('tell.txt',write,S),
  tell(user),wn(end),
  close(S).



% 社会選択環境 *********************
% -----------------------------------------------------------  %
% *****    The Social Coice Environment    *****
% -----------------------------------------------------------  %
% edited : since Sep 201.

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% social environment, including agents' preferences, states, 
% and alternatives (i.e., candidates of the social choice objectives).
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%

alternatives(As):-findall(A,(preference(_,_,R),member(A,R)),B),sort(B,As),!.
all_agents(Is):-findall(J,preference(J,_,_),B),sort(B,Is),!.
agents(Is):-all_agents(Is).
states(Ss):-findall(S,preference(_,S,_),B),sort(B,Ss),!.


/* 
  %%% an old version %%%%
 alternatives([w,x,y,z]).
 all_agents([1,2,3]).
 agents([1,2,3]).
 states([s1,s2]).
 % status_quo(w).
*/

% modified: 2 Jan 2002.
alternative(A):-
   alternatives(As),member(A,As).
alternative(A):-
   alternatives(As),\+ member(A,As),
   write('no such alternative.'),nl,fail.
agent(I):-
   agents(N),member(I,N).
agent(I):-
   agents(N),\+ member(I,N),
   write('no such agent.'),nl,fail.
state(S):-
   states(Ss),member(S,Ss).
state(S):-
   states(Ss),\+ member(S,Ss),
   write('no such state.'),nl,fail.

powerset_of_alt(X):-
   alternatives(As),
   powerset_of(X,As). 

subset_of_alt(Y,N):-
   alternatives(As),
   N^subset_of(Y,N,As).

subset_of_agents(Y,N):-
   all_agents(As),
   N^subset_of(Y,N,As).

two_person([J1,J2]):-
    agents(Is),
    member(J1,Is),member(J2,Is),J1 < J2.
    % subset([J1,J2],Is),  %これだとJ1=J2にしかならない



% an environment for N persons.
% modified: 25 Oct 2002.
% Now, we will use this preicate for modeling like as the enviroment 
% `class'-object, and use it in simulation by its instance asserted to db
% in setup_domain.

% default domain: jp
environment([[1,2,3],[s1,s2],[w,x,y,z]], [3,2,4], [[[x,z,y,w],[y,z,x,w],[z,x,w,y]],[[x,z,y,w],[y,z,x,w],[z,x,y,w]]]).

gen_environment([Is,Ss,As],[N,K,L],Rs):-!,
 %   length(Is, N),
    subset_of_agents(Is,N),
    states(Ss),
    length(Ss, K),
    alternatives(As),
    length(As, L),
    prefer_profiles(Is,Ss,Rs).

gen_environment(Is,E):-
   gen_environment([Is,Ss,As],[N,K,L],Rs),
   E1=[[Is,Ss,As],[N,K,L],Rs],
   E=..[environment|E1],
   forall(
    clause(environment(EB1,EB2,EB3),true),
    (
     retract(environment(EB1,EB2,EB3)),
     write(retracted(environment(EB1,EB2,EB3))),nl
    )
   ),
   assert(E),
   wn(asserted(E)).

% エージェントの選好 *********************
% -----------------------------------------------------------  %
%  *****  The model of preference for rational agents    ****  %
% -----------------------------------------------------------  %
% edited from: Sep 2001.

% rational preferences of individuals, which is a profile 
% of state-dependent preference relations. 

% pairwise comparizon. transitive, reflective, complete.
%% ranking (for an weak ordered set)

is_prefer_to(I,S,X,Y):-
  preference(I,S,Order),
  nth1(J,Order,X),
  nth1(K,Order,Y),
  J =< K. 
is_prefer_to(I,S,X,Y):-
  preference(I,S,Order),
  nth1(J,Order,X),
  nth1(K,Order,Y),
  J > K,
  difference(I,S,Diffs),
  forall(
   (
    nth1(L,Diffs,Diff),
    L >= K, L < J
   ),
   Diff = e). 

% この解釈は一応、サイクルを考えている。
indifferent_to(I,S,X,Y):-
  is_prefer_to(I,S,X,Y),
  is_prefer_to(I,S,Y,X).

% strict ordering.
is_strict_prefer_to(I,S,X,Y):-
  is_prefer_to(I,S,X,Y),
  preference(I,S,Order),
  nth1(J,Order,X),
  nth1(K,Order,Y),
  J < K,
  difference(I,S,Diffs),
  nth1(L,Diffs,s),
  L >= J, L =< K. 

% the following are equivalent when assuming NAF(nagation as failuare),
% in the sense that the indifference relation can not be proved.
%is_strict_prefer_to(I,S,X,Y):-
%  is_prefer_to(I,S,X,Y),
%  \+indifferent_to(I,S,X,Y).
% but next one is erroneous.
%is_strict_prefer_to(I,S,X,Y):-
%  is_prefer_to(I,S,X,Y),
%  \+is_prefer_to(I,S,Y,X).




% -----------------------------------------------------------  %
%   current preference model 
% -----------------------------------------------------------  %
% please copy a tuple of preference/3 and difference/3
% from following soup stock of examples :

/*  the default domain model  */

preference(1,s1,[x,z,y,w]).
preference(2,s1,[y,z,x,w]).
preference(3,s1,[z,x,w,y]).
preference(1,s2,[x,z,y,w]).
preference(2,s2,[y,z,x,w]).
preference(3,s2,[z,x,y,w]).
% extended relations for above example, optionally.
difference(_,_,[s,s,s,end]).


/*
% the example 2 of Moore-Repullo(1990). an elementary coding.
preference(1,s1,[a,c,d,b,z]).
preference(1,s2,[a,d,c,b,z]).
preference(1,s3,[a,c,d,b,z]).
preference(1,s4,[a,d,c,b,z]).
preference(2,s1,[b,c,d,a,z]).
preference(2,s2,[b,d,c,a,z]).
preference(2,s3,[b,d,c,a,z]).
preference(2,s4,[b,c,d,a,z]).
%
% indifferenceの実現方法:選好種類の追加。利点:prefer_toだけ直せばよい。
% 末尾のzとの比較はいずれも無差別
difference(1,s1,[s,s,s,e,end]).
difference(1,s2,[s,s,s,e,end]).
difference(1,s3,[s,s,s,e,end]).
difference(1,s4,[s,s,s,e,end]).
difference(2,s1,[s,s,s,e,end]).
difference(2,s2,[s,s,s,e,end]).
difference(2,s3,[s,s,s,e,end]).
difference(2,s4,[s,s,s,e,end]).
*/

/*

% the example 2 of Moore-Repullo(1990). more sophisticated modelling.

% the monotone scc mr, which is implementable, is rvp, not nvp,
% with the "bad outcome" z.  
preference(1,S11,[a,c,d,b,z]):-member(S11,[s1,s3]).
preference(2,S21,[b,c,d,a,z]):-member(S21,[s1,s4]).
preference(1,S12,[a,d,c,b,z]):-member(S12,[s2,s4]).
preference(2,S22,[b,d,c,a,z]):-member(S22,[s2,s3]).
difference(_,_,[s,s,s,e,end]).
%
*/


/*    choose the preferences from the stock    */
% modified: 25 Oct 2002. permit on-line simulation mode.

domain_models(Doms):-
   findall(M,stock_of(M,_,_,_,_),Ms),
   sort(Ms,Doms).

display_domain(Strm):-
   nl,wn('preference domain: '),
   wn([agent,state,preference,difference]),
   forall(
     (preference(Agent,State,Order),
      difference(Agent,State,Diff)
     ),(tab(3),
      wn([Agent,State,Order,Diff])
     )
   ),
   nl,
  ((var(Strm);Strm=user)->true;
   (
    nl(Strm),wn(Strm,'preferene domain: '),
    wn(Strm,[agent,state,preference,difference]),
    forall(
     (preference(Agent,State,Order),
      difference(Agent,State,Diff)
      ),(tab(Strm,3),
      wn(Strm,[Agent,State,Order,Diff])
     )
    ),
    nl(Strm)
   )
  ).


% modified: 7 Dec 2002. a test of the domain via condition_D has added.

setup_domain:- hear(domain,D), setup_domain(D).

setup_domain(Goal):-
   domain_models(Doms),
   member(Goal,Doms),
   assert(preference(dummy,0,0)),
   assert(difference(dummy,0,0)),
   abolish(preference,3),
   abolish(difference,3),
   forall(
     (
      member(Pred,[preference,difference]),
      apply(stock_of,[Goal,Pred,J,S,O]),
      Domain=..[Pred,J,S,O]
     ),
     (
      assert(Domain)%,wn(Domain)
     )
    ),
   update_env([GF,Scc,Is,E]),
   wn(' The domain model has changed.'),
   check_domain(Is,_Ss,_Rs,_U),nl,
   write(' Do you use on-line mode in mechanism simulation ? (y/n) '),
   (read(y)
    ->update_messages([GF,Scc,Is,E],online)
    ;(
      write(' Will you update the message file? (y/n) '),
      (read(y)
       ->(update_messages([GF,Scc,Is,E],file),
         wn('ok. type [messages] if you like to import messages.'))
       ;true
      )
     )
   ).


% added: 27 Nov 2002. separated from update_messages.
% modified: 29 Dec 2002. assert the default model params.
update_env([GF,Scc,Is,E]):-
   	hear(scc,Scc),
	hear(agents,Is),
	hear(game_form,GF),
   gen_environment(Is,E),
   abolish(default_model,1),
   assert(default_model([GF,Scc,Is,E])).

% added: 8 Jan 2003.
default_model(Model):-update_env(Model).

% modified: 29-31 Dec 2002. 
% reduce by 0 is re-enabled. delayed integer have prohibited.

update_messages([GF,Scc,Is,E],file):-
   abolish(mechanism,3),
   %R = n,  % if not use reduce.
   write('reduced test by 0-integers? (y/n) '),read(R),
   D = y,  % if not use delay.
   %(R=y->D=y;
   %  (write('delayed resolution for integers? (y/n) '),read(D))
   %),
   verify_messages(GF,Scc,Is,E,R,D),
   [messages],
   wn('messages imported').

% modified: 3 Dec 2002.
% modified: 29-31 Dec 2002.
% modified: 2 Jan 2003.
update_messages([_GF,_Scc,_Is,E],online):-
   abolish(mechanism,3),
   %retractall((mechanism(G0,M0,C0):-mechanism(G0,_E0,M0,C0))),
   %G =..[_GF1,_P,_Scc1],  % Scc is unbound
   assert(
     ( mechanism(G,M,C):-
	 (E=environment(_,_,_),mechanism(G,E,M,C))
         % ,lpom(set,M,[GF1,Scc1,Is],_Z),!
     )
   ).



/*  verify all messages ---- called from setup_domain  */
% modified: 25 Oct 2002. 
% added hear/2.

verify_messages:-
   wn('verify_messages(GF,Scc,Is,E,Reduce0,Delay0)').
verify_messages(GF,Scc,Is,E,Reduce0,Delay0):-
   mechanisms(GFs),
   member(GF,GFs),
   scc(Scc),
   subset_of_agents(Is,N),
    E = environment([Is,_,_],[N,_,_],_),
    E,
   wn(ok),
   !,
   open('messages.pl',write,Strm),
   wn('creating a file of the mechanism.'),
   write('ファイルに書出しています。'),nl,
   Goal=[GF,Scc, M,Is],
   (Reduce0=y->Mtest=..[mtest_z0|Goal];Mtest=..[mtest|Goal]),
   (Delay0=n->Lpom=..[lpom,set,M,[GF,Scc,Is],_Zs];Lpom=true),
   (GF=gD->State=..[update_state,_S];State=true),
   forall(
     ( 
      Mtest, Lpom, State
     ),
     (
      G=..[GF,P,Scc],
      (mechanism(G,E,M,C)->true;(P=nul,C=non)),%wn([M,G,C]),read(y),
      write(Strm,mechanism(G,M,C)),wn(Strm,'.')
     )
   ),
   close(Strm).



% modified: 25 Oct 2002. 
% added hear/2 
% modified: 27 Nov 2002. not hear if bound.

hear(_,Hear):- \+var(Hear).
hear(domain,D):-
	var(D),
	domain_models(Ds),
	write('domain? '),read(U),
	(member(U,Ds)->D=U
	;
	(write('no such prepared domain. please select from '),
	 write(Ds),nl,
	 hear(domain,D))).
hear(game_form,GF):-
	var(GF),
	mechanisms(MC),
	write('game_form? '),read(U),
	(member(U,MC)->GF=U
	;
	(write('no such mechanism. please select from '),
	 write(MC),nl,
	 hear(game_form,GF))).
hear(scc,Scc):-
	var(Scc),
	write('scc? '),read(U),
	(scc(U)->Scc=U
	;
	(write('no such scc. please select from '),
	 sccs(SCCs),write(SCCs),nl,
	 hear(scc,Scc))).
hear(agents,Is):-
	var(Is),
	write('agents? '),read(U),
	(subset_of_agents(U,_)->Is=U
	;
	(write('its not an appropriate set of agents. please type '),nl,
	 write(' a subsequence of '),
	 agents(Js),write(Js),nl, 
	 write(' or you may re-setup the domain.'),nl,
	 hear(agents,Is))).


/*
  %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
  %% the soup stock of alternative preferences %% 
  %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
*/

% note:
% each argument in difference/3 correspondes to that of preference/3 resp.
% [s:strict_prefer, w:weak_prefer, e:indifferent] to the succeeding alternative.
% ud32: the approximated universal domain for 3 outcomes and 2 agents
stock_of(ud32,preference,J,S,P):-
   ud32_preference([J,S,P]).
stock_of(ud32,difference,_,_,[s,end]).


% ud22: the (stict) universal domain for 2 outcomes and two agents
stock_of(ud22,preference,1,S11,[x,y]):-member(S11,[s1,s2]).
stock_of(ud22,preference,1,S12,[y,x]):-member(S12,[s3,s4]).
stock_of(ud22,preference,2,S21,[x,y]):-member(S21,[s1,s3]).
stock_of(ud22,preference,2,S22,[y,x]):-member(S22,[s2,s4]).
% extended relations for above example, optionally.
stock_of(ud22,difference,_,_,[s,end]).

% ud23: the (strict) universal domain for 3 outcomes and two agents
%---------------------------------------------------------------------
% note: computational complexity consideration
% probably, this is not computationary tractable in enumerating sccs.
% #(possible orderings) = (#(oucomes)!) << =2*1=2 if ud22;=6 if ud23 >>
% #(states) = #(possible orderings)^#(agents) << =2^2=4 ud22;=6^2=36 ud23 >>
% #(subsets of outcomes) = 2^#(oucomes)  <<  2^2 ud22; 2^3 ud23  >>
% #(possible sccs) = (2^#(subsets of outcomes))^#(states) << 4^4=256; 8^36 >>


stock_of(ud23,preference,1,S,[x,y,z]):-
	member(S2,[1,2,3,4,5,6]),concat(s1,S2,S).
stock_of(ud23,preference,1,S,[x,z,y]):-
	member(S2,[1,2,3,4,5,6]),concat(s2,S2,S).
stock_of(ud23,preference,1,S,[y,z,x]):-
	member(S2,[1,2,3,4,5,6]),concat(s3,S2,S).
stock_of(ud23,preference,1,S,[y,x,z]):-
	member(S2,[1,2,3,4,5,6]),concat(s4,S2,S).
stock_of(ud23,preference,1,S,[z,y,x]):-
	member(S2,[1,2,3,4,5,6]),concat(s5,S2,S).
stock_of(ud23,preference,1,S,[z,x,y]):-
	member(S2,[1,2,3,4,5,6]),concat(s6,S2,S).
stock_of(ud23,preference,2,S,[x,y,z]):-
	member(S1,[1,2,3,4,5,6]),concat_v([s,S1,1],S,3).
stock_of(ud23,preference,2,S,[x,z,y]):-
	member(S1,[1,2,3,4,5,6]),concat_v([s,S1,2],S,3).
stock_of(ud23,preference,2,S,[y,z,x]):-
	member(S1,[1,2,3,4,5,6]),concat_v([s,S1,3],S,3).
stock_of(ud23,preference,2,S,[y,x,z]):-
	member(S1,[1,2,3,4,5,6]),concat_v([s,S1,4],S,3).
stock_of(ud23,preference,2,S,[z,y,x]):-
	member(S1,[1,2,3,4,5,6]),concat_v([s,S1,5],S,3).
stock_of(ud23,preference,2,S,[z,x,y]):-
	member(S1,[1,2,3,4,5,6]),concat_v([s,S1,6],S,3).
% an extended relations for above example, optionally.
stock_of(ud23,difference,_,_,[s,s,end]).




% the example 2 of Moore-Repullo(1990).
% the monotone scc mr, which is implementable, is rvp, not nvp,
% with the "bad outcome" z.  
stock_of(mr,preference,1,S11,[a,c,d,b,z]):-member(S11,[s1,s3]).
stock_of(mr,preference,1,S12,[a,d,c,b,z]):-member(S12,[s2,s4]).
stock_of(mr,preference,2,S21,[b,c,d,a,z]):-member(S21,[s1,s4]).
stock_of(mr,preference,2,S22,[b,d,c,a,z]):-member(S22,[s2,s3]).
stock_of(mr,difference,_,_,[s,s,s,e,end]).
%




% the example of the footnote 91 in Moore(1992).
% it is implementable but is not strongly monotone under ud.  
% scc: s1-> a;s2->b;s3->c.
stock_of(md,preference,1,s1,[a,d,c,b]).
stock_of(md,preference,1,s2,[d,a,b,c]).
stock_of(md,preference,1,s3,[c,a,d,b]).
stock_of(md,preference,2,S,[b,a,d,c]):-member(S,[s1,s2]).
stock_of(md,preference,2,s3,[b,c,a,d]).
stock_of(md,difference,_,_,[s,s,s,end]).
%




% the voting example from Jackson and Palfrey (2001)
% scc f, and its modified sccs: f1,f0,g,g0,g1,g2,g4.
% note:
% since there are only 2 states, rule 3 of gM (or gMR) will not be invoked if 0-integered.
stock_of(jp,preference,1,S,[x,z,y,w]):-member(S,[s1,s2]).
stock_of(jp,preference,2,S,[y,z,x,w]):-member(S,[s1,s2]).
stock_of(jp,preference,3,s1,[z,x,w,y]).
%stock_of(jp,preference,1,s2,[x,z,y,w]).
%stock_of(jp,preference,2,s2,[y,z,x,w]).
stock_of(jp,preference,3,s2,[z,x,y,w]).
% extended relations for above example, optionally.
stock_of(jp,difference,_,_,[s,s,s,end]).



% the example of Suh(1996), 
% strongly implemetable with scc suh.
stock_of(suh,preference,1,S1,[b,a,d,c,e,f]):-member(S1,[s11,s12,s13]).
stock_of(suh,preference,1,S1,[d,b,a,c,e,f]):-member(S1,[s21,s22,s23]).
stock_of(suh,preference,1,S1,[b,d,a,c,e,f]):-member(S1,[s31,s32,s33]).
stock_of(suh,preference,2,S2,[e,d,c,a,b,f]):-member(S2,[s11,s21,s31]).
stock_of(suh,preference,2,S2,[d,b,a,c,e,f]):-member(S2,[s12,s22,s32]).
stock_of(suh,preference,2,S2,[c,d,b,a,e,f]):-member(S2,[s13,s23,s33]).
stock_of(suh,difference,_,_,[w,w,w,w,w,end]).


% the King Solomom example from Wolinsky and Rubinstein(1994)
% with scc ks: scc(ks,s1,[a]).scc(ks,s2,[b]).
stock_of(ks,preference,1,s1,[a,b,d]).
stock_of(ks,preference,2,s1,[b,d,a]).
stock_of(ks,preference,1,s2,[a,d,b]).
stock_of(ks,preference,2,s2,[b,a,d]).
stock_of(ks,difference,_,_,[s,s,end]).
% ibid., excercise, p.191. monotone but not Nash-implementable
% with scc ks.?
stock_of(ks1,preference,1,s1,[a,c,b]).
stock_of(ks1,preference,2,s1,[c,b,a]).
stock_of(ks1,preference,1,s2,[c,a,b]).
stock_of(ks1,preference,2,s2,[b,c,a]).
stock_of(ks1,difference,_,_,[s,s,end]).



% the examples 2 from Yamato(1992)
% ex 2. with scc y1.
%scc(y1,s1,[a,c]).
%scc(y1,s2,[c]).
stock_of(y1,preference,1,s1,[a,b,c]).
stock_of(y1,preference,2,s1,[c,a,b]).
stock_of(y1,preference,3,s1,[c,a,b]).
stock_of(y1,preference,1,s2,[b,a,c]).
stock_of(y1,preference,2,s2,[c,a,b]).
stock_of(y1,preference,3,s2,[c,a,b]).
stock_of(y1,difference,_,_,[w,w,end]).

% the examples 3 from Yamato(1992)
% ex 3. with scc y1,y2.
%scc(y2,s1,[a,b]).
%scc(y2,s2,[a]).
stock_of(y2,preference,1,s1,[a,b,c]).
stock_of(y2,preference,2,s1,[c,b,a]).
stock_of(y2,preference,3,s1,[c,b,a]).
stock_of(y2,preference,1,s2,[a,c,b]).
stock_of(y2,preference,2,s2,[c,a,b]).
stock_of(y2,preference,3,s2,[c,a,b]).
%
stock_of(y2,difference,_,_,[w,w,end]).



/*
  %%%%%%%%%%%%%%%%%%%%%%%%%%%
  %%    end of the stock   %% 
  %%%%%%%%%%%%%%%%%%%%%%%%%%%
*/


% -----------------------------------------------------------  %
% ud32: the approximated universal domain for 3 outcomes and 2 agents
% -----------------------------------------------------------  %
% edited from: Aug 2002. modified: 25 Aug 2002.

ud32_preference([J,S,P]):-
   ud32_preferences(Pud32),
   member(Ts,Pud32),
   T=[J,S,P],
   nth1(_K,Ts,T).

ud32_preferences(Pa):-
    Is =[1,2,3],
    Alt=[a,b],
    findall(P,
      ud_profile([Is,Alt],[_N,_M],P),
     Pa),
    numbervars(Pa,s,1,_E).

ud_preference([Is,Alt],[N,M],S,J,[J,S,P]):-
    length(Alt,M),
    length(Is,N),
    member(J,Is),
    ordering(P,Alt,M).

ud_profile([Is,Alt],[N,M],Profile):-
    my_maplist(ud_preference([Is,Alt],[N,M],_S),Is,Profile).



% -----------------------------------------------------------  %
% auto-generated preferences
% -----------------------------------------------------------  %
% edited from: Aug 2002. modified: 25 Aug 2002.

all_preferences(Rs,Alts,M):-
   alternatives(Alts),
   length(Alts,M),
   setof(C,
   (
    ordering(C,Alts,M),
    sort(C,Alts)
   ),Rs).
auto_preference(I,S,P):-
   agent(I),state(S),
   alternatives(Alts),
   length(Alts,M),
   ordering(P,Alts,M).
auto_profile(Is,S,Ps):-
   state(S),
   subset_of_agents(Is,N),
   all_preferences(Rs,_Alts,_M),
   bag0(Ps,Rs,N).
auto_profiles(Ss,Is,Pss):-
   subset_of_agents(Is,_),states(Ss),
   my_maplist(auto_profile(Is),Ss,Pss).
generate_preferences(Is,Profs):-
  subset_of_agents(Is,_),states(Ss),
  auto_profiles(Ss,Is,Profs),
  forall(
   (nth1(K,Is,J),nth1(U,Ss,S)),
   (
    nth1(U,Profs,Pu),nth1(K,Pu,Puk),
    preference(J,S,P),
    retract(preference(J,S,P)),
    assert(preference(J,S,Puk))
   )
  ).

% -----------------------------------------------------------  %
% testing with auto-generated preferences
% -----------------------------------------------------------  %
% edited from: Aug 2002. modified: 25 Aug 2002.

gen_test_preference(Profs,Is,F,Goals,NoGoods):-
  subset_of_agents(Is,_),
  GR=[cd,cm,cm2,mm,em,mr,ir,bad,nvp,rvp,unan,po,co,dict,neli,mlib],
  subset_of(Goals,_,GR),
  subset_of(NoGoods,_,GR),
  intersection(Goals,NoGoods,Conflict),
  (Conflict=[]
   ->true;
    (wn(['conflicting goals',Conflict,' please retry.']),fail)
  ),wn(p),
  GL = [ condition_D([Is,_Ss,Profs]),
  	condition_M(F,Is),
  	condition_M2(F,Is),
	monotone(F,Is),
  	ess_monotone(F,Is),
  	has_MR_property(F,Is),
  	test_irat_n2(F,Is),
  	bad_outcome(_Bad,F,Is),
  	nvp(F,Is),
  	rvp(F,Is),
  	unanimity(F,Is),
  	has_pareto_property(F,Is),
  	has_condorcet_property(F,Is),
  	dictatorial(F,Is),
  	neli(F,Is),
  	mlib(F,Is)],
  !,
  generate_preferences(Is,Profs),%wn(Profs),
  %states(Ss),prefer_profiles(Is,Ss,PP),wn(PP),
  forall(
    (
     member(Gx,Goals),nth1(Num,GR,Gx),wn([Num,Gx])
    ),
    (nth1(Num,GL,Gox),%wn([go,GoX]),
     Gox)
  ),
  forall(
    (
     member(Gx,NoGoods),nth1(Num,GR,Gx),wn([Num,Gx])
    ),
    (nth1(Num,GL,GoX),%wn([go_not,GoX]),
     \+ GoX)
  ).

     
/*
member(cd,Goals)->condition_D(Is,Ss,Profs); true),
  scc(F),
  (member(cm,Goals)->condition_M(F,Is); true),
  (member(cm2,Goals)->condition_M2(F,Is); true),
  (member(mm,Goals)->monotone(F,Is) ; true),
  (member(em,Goals)->ess_monotone(F,Is) ; true),
  (member(mr,Goals)->has_MR_property(F,Is) ; true),
  (member(ir,Goals)->test_irat_n2(F,Is) ; true),
  %---------------------------------------------------------%
  (member(bad,Goals)->(bad_outcome(_Bad,F,Is)) ; true),
  (member(nvp,Goals)->nvp(F,Is) ; true),
  (member(rvp,Goals)->rvp(F,Is) ; true),
  (member(unan,Goals)->unanimity(F,Is) ; true),
  (member(po,Goals)->has_pareto_property(F,Is) ; true),
  (member(co,Goals)->has_condorcet_property(F,Is) ; true),
  (member(dict,Goals)->dictatorial(F,Is) ; true),
  (member(neli,Goals)->neli(F,Is) ; true),
  (member(mlib,Goals)->mlib(F,Is) ; true),
  true.
*/

% -----------------------------------------------------------  %
%%% preference profiles
% -----------------------------------------------------------  %
% edited from: sep 2001. modified: 25 Aug 2002.


prefer_profiles(Is,Ss,Rs):-
   subset_of_agents(Is,_N),
   states(Ss),
   bagof(Rks,
     S^(
      member(S,Ss),
      bagof(Rk,
        I^(member(I,Is),preference(I,S,Rk)),
      Rks)
     ),
   Rs).

%true_prefer_profile
prefer_profile(Is,S,Rks):-
    true_prefer_profile(Is,S,Rks).
true_prefer_profile(Is,S,Rks):-
    subset_of_agents(Is,_N),
    state(S),
    bagof(Rk,
      I^(
       member(I,Is),preference(I,S,Rk)
      ),
    Rks).

%true_or_false_prefer_profile

prefer_profile(Is,Rs):-
    subset_of_agents(Is,_N),
    bagof(Rk,
      I^(
       member(I,Is),    state(S),
       preference(I,S,Rk)
      ),
    Rs).

% a new code:
% profile by using maplist/3
m_profiles(Is,Rs):-
   subset_of_agents(Is,_N),
   my_maplist(m_profile(preference),Is,Rs).



% -----------------------------------------------------------  %
%%%%%% finding reversals.
% -----------------------------------------------------------  %
% edited from: Sep 2001.

% no_reversals/5, no_reversals_1/5, and no_reversals_2/5, (omitted.)
% have a common function to detect a preference reversal.
%

is_reversal(I,S1,S2,X,Y):-
 %  states(S),member(S1,S),member(S2,S),
 %  agents(Society),member(I,Society), not is_prefer_to(I,S1,Y,X),
  is_prefer_to(I,S1,X,Y),
  is_prefer_to(I,S2,Y,X).


reversals(I,S1,S2,X,A,Rvs):-
  alternatives(A),
  subset_of_agents(Is,_N),
  states(S),
  findall((I,X,S1,S2),
   ( 
     member(I,Is),
     member(X,A),
     member(S1,S),
     member(S2,S),
     is_reversal(I,S1,S2,X,_)
   ),Rvs
  ).


% -----------------------------------------------------------  %
%    lower/upper contour set (lcc/3,ucc/3)
% -----------------------------------------------------------  %
% edited from: 18 Oct 2001. 

% lower contour set
lcc([I,S,R],A,Lcc) :-
    alternative(A),
    agent(I),
    state(S),
    preference(I,S,R),
    findall(L,
     (
       alternative(L), 
       is_prefer_to(I,S,A,L)
     ),
      Lcc0),
    sort(Lcc0,Lcc).



% the following three variations of lcc is augumented
% in 18 Aug 2002.

% upper contour set
ucc([I,S,R],A,Ucc) :-
    alternative(A),
    agent(I),
    state(S),
    preference(I,S,R),
    findall(L,
     (
       alternative(L), 
       is_prefer_to(I,S,L,A)
     ),
      Ucc0),
    sort(Ucc0,Ucc).




% -----------------------------------------------------------  %
%    strict lower/upper contour set (slcc/3, succ/3)
% -----------------------------------------------------------  %
% added: Aug 2002. 

slcc([I,S,R],A,SL) :-
    alternative(A),
    agent(I),
    state(S),
    preference(I,S,R),
    ucc([I,S,R],A,Ucc),
    alternatives(As),
    subtract(As,Ucc,SL0),
    sort(SL0,SL).

succ([I,S,R],A,SU) :-
    alternative(A),
    agent(I),
    state(S),
    preference(I,S,R),
    lcc([I,S,R],A,Lcc),
    alternatives(As),
    subtract(As,Lcc,SU0),
    sort(SU0,SU).


% -----------------------------------------------------------  %
%     maximal element
% -----------------------------------------------------------  %
% added: Aug 2002. 

maximal(A,X,[I,S,R]):-
    preference(I,S,R),
    subset_of_alt(X,_),X\=[],
    member(A,X),
    lcc([I,S,R],A,Lcc),
    subset(X,Lcc).
maximal_set(Y,X,[I,S,R]):-
    preference(I,S,R),
    subset_of_alt(X,_),X\=[],
    findall(A,maximal(A,X,[I,S,R]),Max),
    sort(Max,Y).
    


%      %%%%%%%%%%%%%%%%%%%%%%%%%
%      %%%    condition D    %%%
%      %%%%%%%%%%%%%%%%%%%%%%%%%
%
% -----------------------------------------------------------  %
% Condition D  :
%  checking the domain restriction whether it is near universal.
% -----------------------------------------------------------  %
% reference: Yamato(1992), p.487.
% creared: 20 Aug 2002. modified: 25 Aug 2002.
% modified: 25 Sep 2002. arity /2 --> /1

condition_D(Is,Ss,Rs):-
   ((var(Rs),agents(Is),states(Ss),prefer_profiles(Is,Ss,Rs),wn(initial));\+var(Rs)),
   subset_of_agents(Is,_),
   alternatives(As),
   forall(
    (
     nth1(K,Ss,S),    % K: the index for the state
     nth1(K,Rs,R),
     nth1(L,Is,J),    % J: the index for the agent
     nth1(L,R,RJ),
     alternative(A),
     lcc([J,S,RJ],A,Lcc),
     member(B,Lcc)%,wn([S,J,A,B])
    ),
     (
      member(S1,Ss),
      lcc([J,S1,_RJ1],B,Lcc),%wn([J,S1,B,Lcc]),
      forall((nth1(_L1,Is,J1),J1\=J),
        (
         %wn([J,S1,B,Lcc]),
	 lcc([J1,S1,_RJ2],B,As)
        )
      )
     )
   ).

condition_D_debug([Is,Ss,Rs]):-
   alternatives(As),
   subset_of_agents(Is,_),
   (var(Rs)->prefer_profiles(Is,Ss,Rs);true),
   forall(
    (
     nth1(K,Ss,S),    % K: the index for the state
     nth1(K,Rs,R),
     nth1(L,Is,J),    % J: the index for the agent
     nth1(L,R,RJ),
     alternative(A),
     lcc([J,S,RJ],A,Lcc),
     member(B,Lcc),wn([S,J,A,B])
    ),
     (
      lcc([J,S1,_RJ1],B,Lcc),tab(2),wn([J,S1,B,Lcc]),
      forall((nth1(_L1,Is,J1),J1\=J),
        (
         tab(4),wn([J,S1,B,Lcc]),
	 lcc([J1,S1,_RJ2],B,As)
        )
      )
     )
   ).

/* ------------------------------------------------------------ */
% contract_domain_with_condition_D(Domain):-
/* ------------------------------------------------------------ */
% added : 8 Sep 2002.
% but pending. previously, and... I had made the another one like as this.
% modified : 25 Sep 2002.
% modified : 15 Oct 2002.
% modified : 7 Dec 2002.  chek_domain /4 has separated from cntract_domain /4.

check_domain(Is,Ss,Rs,yes):-
    prefer_profiles(Is,Ss,Rs),
    condition_D(Is,Ss,Rs),
    wn('---- your domain model ---'),
    display_domain(user),
    wn('The_condition_D_has_satisfied.').
check_domain(Is,Ss,Rs,no):-
    prefer_profiles(Is,Ss,Rs),
    \+condition_D(Is,Ss,Rs),
    wn('---- your domain model ---'),
    display_domain(user),
    wn('This_doimain_does__not__satisfy_condition_D.').

contract_domain(Is,Ss,Rs,dialog):-
    check_domain(Is,Ss,Rs,_YN),
    wn('Are you sure to contract it? (y/n) '),
    read(U),\+U=y.
contract_domain(Is,NewSs,Rs1,_):-
    prefer_profiles(Is,Ss,Rs),
    subset_of(Removed,_,Ss),
    \+member(Removed,[[],Ss]),
    subtract(Ss,Removed,NewSs),
    pairwise_contract_map([NewSs,Ss],[Rs1,Rs]),
    condition_D(Is,NewSs,Rs1),
     wn('---- I found a contracted domain model ! ---'),
     wn(newStates(NewSs)),wn(newDomain(Rs1)),
     wn('Are you really update the model ? (y/n) '),
     read(y),
     forall(
       (
        preference(A,B,C),\+member(B,NewSs)
       ),
       retract(preference(A,B,C))
     ),
     wn('---- updated domain model ---'),
     display_domain(user).
contract_domain(Is,Ss,Rs,_):-
    prefer_profiles(Is,Ss,Rs),
    %\+condition_D(Is,Ss,Rs),
    wn('There_is_no_more_contracted_domain_which_satisfies_condition_D.'),!.


% -----------------------------------------------------------  %
% 社会選択対応  (SCC)
% -----------------------------------------------------------  %
%
range(Scc,C):- setof(Z,S^scc(Scc,S,Z),Zs),all_members(Zs,C).
all_members(A,B):-setof(D,C^(member(C,A),member(D,C)),B).
sccs(Fs):- setof(F,S^Z^scc(F,S,Z),Fs).
scc(F):-sccs(Fs),member(F,Fs).
%
scc_defined_states(Sd,F):-scc(F),setof(S,Z^scc(F,S,Z),Sd).
scc_defined_states([],_F).
scc_defined_state(S,F):-scc_defined_states(Sd,F),member(S,Sd).


%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% samples of SCC; social choice correspondece, mapping F:S-->->A.
% checking the monotonicity of SCCs.
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% edited from Sep 2001.

% f a non-monotonic SCC
% the example1 (Voting) of Jackson & Palfrey, p.8.
scc(f,s1,[x,z]).
scc(f,s2,[x]).
% next 2 factas are extended for debug.
%scc(f,s3,[x,z]).
%scc(f,s4,[x]).
%range(f,[x,z]).

% f1 a monotone, but not ess_monotone SCC
scc(f1,s1,[x]).
scc(f1,s2,[x,y]).
%range(f1,[x,y]).

% g a monotone, but not ess_monotone SCC
scc(g,s1,[x,w]).
scc(g,s2,[x]).
%range(g,[x,w]).

% g1 an ess_monotone SCC
scc(g1,s1,[x,w]).
scc(g1,s2,[x,y]).
%range(g1,[x,w,y]).

% g0 an ess_monotone SCC
scc(g0,s1,[x,y]).
scc(g0,s2,[x,y]).
%range(g0,[x,y]).


% g2 an ess_monotone SCC
scc(g2,s1,[w]).
scc(g2,s2,[y]).
%range(g2,[w,y]).

% g4 an ess_monotone SCC
scc(g4,s1,[w,x,y]).
scc(g4,s2,[x,y]).
%range(g4,[w,x,y]).



% mr an ess_monotone SCC from Moore and Repullo
scc(mr,s1,[c]).
scc(mr,s2,[d]).
scc(mr,s3,[c]).
scc(mr,s4,[c]).
%range(mr,[c,d]).

% an example in Moore(1992), footnote 91.
% scc: s1-> a;s2->b;s3->c.
scc(md,s1,[a]).
scc(md,s2,[b]).
scc(md,s3,[c]).

% suh an ess_monotone SCC from Suh(1996)
scc(suh,s11,[a,e]).
scc(suh,S2,[b]):-member(S2,[s12,s32]).
scc(suh,S3,[c]):-member(S3,[s13,s33]).
scc(suh,s22,[d]).
scc(suh,s21,[d,e]).
scc(suh,s31,[e]).
%range(suh,[a,b,c,d,e]).


% urd: five auto_generated SCCs for the unristricted domain 
% (its linear order part) of N=2, M=2, each of which clear 
% EM+IR+MR. i.e., is essentially monotone, is individually 
% rational, and has the Moore-Repullo property.
scc(urd0,s1,[]).
scc(urd0,s2,[]).
scc(urd0,s3,[]).
scc(urd0,s4,[]).
%range(urd0,[]).
scc(urd1,s1,[y]).
scc(urd1,s2,[y]).
scc(urd1,s3,[y]).
scc(urd1,s4,[y]).
%range(urd1,[y]).
scc(urd2,s1,[x,y]).
scc(urd2,s2,[y]).
scc(urd2,s3,[y]).
scc(urd2,s4,[y]).
%range(urd2,[x,y]).
scc(urd3,s1,[x]).
scc(urd3,s2,[x]).
scc(urd3,s3,[x]).
scc(urd3,s4,[x]).
%range(urd3,[x]).
scc(urd4,s1,[x]).
scc(urd4,s2,[x]).
scc(urd4,s3,[x]).
scc(urd4,s4,[x,y]).
%range(urd4,[x,y]).


% dictatorial sccs for ud22.
scc(udd1,s1,[x]).
scc(udd1,s2,[x]).
scc(udd1,s3,[y]).
scc(udd1,s4,[y]).
%range(udd1,[x,y]).
scc(udd2,s1,[x]).
scc(udd2,s2,[y]).
scc(udd2,s3,[x]).
scc(udd2,s4,[y]).
%range(udd2,[x,y]).

%  remaining five sccs each of which satisfies em+ir+mr. 
scc(Umd,s1,[x]):-member(Umd,[umd1,umd2,umd3,umd4,umd5]).
scc(Umd,s2,[]):-member(Umd,[umd1,umd2,umd5]).
scc(Umd,s2,A):-member([Umd,A],[[umd3,[x]],[umd4,[y]]]).
scc(Umd,s3,B):-member([Umd,B],[[umd1,[x]],[umd2,[y]]]).
scc(Umd,s3,[]):-member(Umd,[umd3,umd4,umd5]).
scc(Umd,s4,[y]):-member(Umd,[umd1,umd2,umd3,umd4,umd5]).
%range(Umd,[x,y]).



% some problematic sccs for ud22.
scc(umr1,s1,[x]).
scc(umr1,s2,[]).
scc(umr1,s3,[]).
scc(umr1,s4,[]).
%range(umr1,[x,y]).
scc(umr2,s1,[]).
scc(umr2,s2,[]).
scc(umr2,s3,[]).
scc(umr2,s4,[y]).
%range(umr2,[x,y]).
scc(umr3,s1,[x,y]).
scc(umr3,s2,[x,y]).
scc(umr3,s3,[x,y]).
scc(umr3,s4,[x,y]).
%range(umr3,[x,y]).




% pareto corr for ud22.
% also mlib, and unan (a Peleg impossibility) for ud22.
scc(par,s1,[x]).
scc(par,s2,[x,y]).
scc(par,s3,[x,y]).
scc(par,s4,[y]).
%range(par,[x,y]).

% pareto corr for ud22.
% also mlib, and unan (a Peleg impossibility).
scc(par1,s1,[x]).
scc(par1,s2,[x,y]).
scc(par1,s3,[y]).
scc(par1,s4,[y]).
%range(par1,[x,y]).

% non_pareto corr for ud22.
% mlib, and unan (a Peleg impossibility).
scc(pel,s1,[x,y]).
scc(pel,s2,[x,y]).
scc(pel,s3,[y]).
scc(pel,s4,[y]).
%range(pel1,[x,y]).

% not implementable corr for ud22.
scc(fd1,s1,[y]).
scc(fd1,s2,[x]).
scc(fd1,s3,[y]).
scc(fd1,s4,[x]).
%range(fd1,[x,y]).
% not implementable (em+ir,but not mr) corr for ud22.
scc(fr,s1,[x,y]).
scc(fr,s2,[x,y]).
scc(fr,s3,[x,y]).
scc(fr,s4,[x,y]).
%range(fr,[x,y]).
% not implementable (po+em+ir,but not mr) corr for ud22.
scc(po1,s1,[x]).
scc(po1,s2,[x]).
scc(po1,s3,[x]).
scc(po1,s4,[y]).
%range(po1,[x,y]).
% not implementable (po+em+ir,but not mr) corr for ud22.
scc(po2,s1,[x]).
scc(po2,s2,[y]).
scc(po2,s3,[y]).
scc(po2,s4,[y]).
%range(po2,[x,y]).



% King Solomon's choice function.
scc(ks,s1,[a]).
scc(ks,s2,[b]).
% King Solomon's other choice functions.(po+em+ir, not mr).
scc(kspo1,S,[a]):-member(S,[s1,s2]).
scc(kspo2,S,[b]):-member(S,[s1,s2]).
scc(kspo3,S,[a,b]):-member(S,[s1,s2]).
% King Solomon's choice function.(em+ir, not mr, not po).
scc(ksnpo,S,[d]):-member(S,[s1,s2]).




% examples 2,and 3 in Yamato(1992),pp.490-491.
% y1: the scc of example 2
scc(y1,s1,[a,c]).
scc(y1,s2,[c]).
% y2: the scc of example 3
scc(y2,s1,[a,b]).
scc(y2,s2,[a]).

% -----------------------------------------------------------  %
% auto-generating-and-testing of possible SCCs.
% -----------------------------------------------------------  %
% added: July--Aug 2002. 
% modified: Sep 26 2002.


% gen_test_sccs /0 added: 15 Oct 2002.
gen_test_sccs:-
  Goals=[mm,em,mr,ir,bad(_),nvp,rvp,unan,po,co,dict,neli,mlib,neu],
  Base0=[_1,_2,_3,_4,_5,_6,_7,_8,_9,_10,_11,_12,_13,_14],
  tab(4),write('conditions to be satisfied'),read(C),
  subset(C,Goals),
  list_projection(Project,Goals,C1),seteq(C1,C),
  replace(Project,Goals,Base0,G1), % mask over [no,no,..].
  tab(4),write('agents'),read(A),
  (subset_of_agents(A,_)->Is=A;agents(Is)),
  tab(4),write('range of scc (or full)'),read(B),
  (subset_of_alt(B,_)->Range=B;alternatives(Range)),
  tab(4),write('permit empty scc (y/n) '),read(E),
  (E=y->true;Empty=nonempty),
  gen_test_sccs(SCC,G1,[Is,Range,Empty]),
  (
    nl,wn('generated scc:'),wn(scc1(SCC)),wn(satisfied(G1))
  ).

% modified: 19 Oct 2002. prerequisit for `structural' match.
gen_test_sccs(SC_tuples,Goals):-
  G0=[mm,em,mr,ir,bad(_),nvp,rvp,unan,po,co,dict,neli,mlib,neu],
  length(G0,Lg),
  (length(Goals,Lg);subset_of(G0,Goals)),
  Range=full,Empty=nonempty,agents(Is),
  gen_test_sccs(SC_tuples,Goals,[Is,Range,Empty]).

gen_test_sccs(SC_tuples,Goals,[Is,Range,Empty]):-
  G0=[mm,em,mr,ir,bad(_),nvp,rvp,unan,po,co,dict,neli,mlib,neu],
  length(G0,Lg),
  (length(Goals,Lg);subset_of(G0,Goals)),
  subset_of_agents(Is,_),
  generate_scc(scc1,SC_tuples,[Range,Empty]),
  tests_for_scc(scc1,Is,Goals).

generate_scc(F,Cc,[Range,Empty]):-
  member(F,[scc0,scc1,scc2]),
  states(Ss), length(Ss,K),
  scc_tuple(Cc,K,Ss,[Range,Empty]),
  clear_scc(F),  % note: this position is sensitive.
  update_scc(F,Cc).
%range(scc0,[x,y,z,w]).

scc_tuple([],0,[],[_Range,_Empty]).
scc_tuple([[S,X]|Cr],K,[S|Sc],[Range,Empty]):-
  scc_tuple(Cr,K1,Sc,[Range,Empty]),
  K is K1 + 1,
  states(Ss),reverse(Ss,Sr),nth1(K,Sr,S),
  subset_of_alt(X,_N1),
  (Empty=nonempty->X\=[];true),
  (Range=full->true;subset(X,Range)).

update_scc(scc1,Cc):-
  forall(member([S,X],Cc),assert(scc(scc1,S,X))).

clear_scc(scc1):-
  forall(scc(scc1,S,W),retract(scc(scc1,S,W))).

%added: 23 Sep 2002.
extract_em(Pred,SCC,Conditions):-
  A=[],B=[[_,[]]],C=[em],D=[ng],
  extract_sccs(Pred,SCC,Conditions,[A,B,C,D]).
extract_sccs(Pred,SCC,Conditions,[Cond1,Cond2,Cond3,Cond4]):-
  (member([_,[]],Cond2)->Empty=nonempty;true),
  G=..[Pred,SCC,Conditions,[_Range,Empty]],
  G,
  % 1st condition: SCC keywords;
  % 2nd condition: SCC NG words;
  % 3rd condition: Conditions keywords;
  % 4th condition: Condiitons NG words.
  subset(Cond1,SCC),
  \+subset(Cond2,SCC),
  subset(Cond3,Conditions),
  \+subset(Cond4,Conditions).

gen_test_mr(SC_tuples,G3):-
  agents(Is),Range=full,Empty=nonempty,
  gen_test_mr(SC_tuples,G3,[Is,Range,Empty]).
gen_test_mr(SC_tuples,G3,[Is,Range,Empty]):-
  generate_scc(scc1,SC_tuples,[Range,Empty]),
  (has_MR_property(scc1,Is) -> G3 = mr; G3 = no).

% gen_test_neutral has added: 1 Sep 2002.
gen_test_neutral(SC_tuples,Neu):-
  agents(Is),Range=full,Empty=nonempty,
  gen_test_neutral(SC_tuples,Neu,[Is,Range,Empty]).
gen_test_neutral(SC_tuples,Neu,[Is,Range,Empty]):-
  generate_scc(scc1,SC_tuples,[Range,Empty]),
  (is_neutral(scc1,Is) -> Neu = neutral; Neu = no).

% gen_test_mju has added: 1 Sep 2002.
%  modified: 27-8 Sep 2002.
gen_test_mju(SC_tuples,[Gm1,Gm2,Gm3,Gm4]):-
   agents(Is),
   gen_test_mju(SC_tuples,[Gm1,Gm2,Gm3,Gm4],[Is,full,nonempty]).
gen_test_mju(SC_tuples,[Gm1,Gm2,Gm3,Gm4],[Is,Range,Empty]):-
  generate_scc(scc1,SC_tuples,[Range,Empty]),
  test_mju(scc1,Is,[Gm1,Gm2,Gm3,Gm4]).

% modified: 10 Nov 2002. test_mju has separated from gen_test_mju.
test_mju(Scc,Is,[Gm1,Gm2,Gm3,Gm4]):-
  (condition_mju(Scc,Is,Bx,[yes,yes],[i]) -> Gm1 = mju1; Gm1 = '-'),
  (condition_mju(Scc,Is,Bx,[yes,yes],[ii]) -> Gm2 = mju2; Gm2 = '-'),
  (condition_mju(Scc,Is,Bx,[yes,yes],[iii]) -> Gm3 = mju3; Gm3 = '-'),
  (condition_mju(Scc,Is,Bx,[yes,yes],[iv]) -> Gm4 = mju4; Gm4 = '-').


% gen_test_M has added: 2 Sep 2002.
gen_test_M(SC_tuples,[M1,M2]):-
  agents(Is),Range=full,Empty=nonempty,
  gen_test_M(SC_tuples,[M1,M2],[Is,Range,Empty]).
gen_test_M(SC_tuples,[M1,M2],[Is,Range,Empty]):-
  generate_scc(scc1,SC_tuples,[Range,Empty]),
  (condition_M(scc1,Is) -> M1 = cnd_M; M1 = no),
  (condition_M2(scc1,Is) -> M2 = cnd_M2; M2 = no).

% -----------------------------------------------------------  %
% testing the major properties for scc.
% -----------------------------------------------------------  %
% edited : Aug 2002.
% modified: 15 Oct 2002.

% each test routine has included in the section of the property resp.



tests_for_scc(F,Is,[G1,G2,G3,G4,BO,G5,G6,G7,G8,G9,G10,G11,G12,G13]):-
  scc(F),
  subset_of_agents(Is,_),
  (monotone(F,Is) -> G1 = mm; G1 = '-'),
  (ess_monotone(F,Is) -> G2 = em; G2 = '-'),
  (has_MR_property(F,Is) -> G3 = mr; G3 = '-'),
  (test_irat_n2(F,Is) -> G4 = ir; G4 = '-'),
  %---------------------------------------------------------%
  ((bad_outcome(Bad,F,Is)) ->BO = bad(Bad); BO = '-'),
  (nvp(F,Is) -> G5 = nvp; G5 = '-'),
  (rvp(F,Is) -> G6 = rvp; G6 = '-'),
  (unanimity(F,Is) -> G7 = unan; G7 = '-'),
  (has_pareto_property(F,Is) -> G8 = po; G8 = '-'),
  (has_condorcet_property(F,Is) -> G9 = co; G9 = '-'),
  (dictatorial(F,Is) -> G10 = dict; G10 = '-'),
  (neli(F,Is) -> G11 = neli; G11 = '-'),
  (mlib(F,Is) -> G12 = mlib; G12 = '-'),
  (is_neutral(scc1,Is) -> G13 = neu; G13 = '-'),
  true.

% -----------------------------------------------------------  %
%   several tests for 2-state case the properties of SCC
% -----------------------------------------------------------  %

test_urd_m2(Out):-
   Out=[Scc,[1,2],Results,Mr],
   member(Scc,[urd1,urd2,urd3,urd4]),
   test_gD(Scc,[1,2],Results,Mr).

test_impl2([A,B],[I,J],[GF,Summary]):-
  generate_scc(scc0,[A,B]),
  two_person([I,J]),
  test_impl(GF,scc0,[I,J],2,Summary).
% save_br_results(_File,_Strm)

test_null(F,[A,B],_):-
  generate_scc(F,[A,B]).

test_mrp(F,[A,B],[J,K]):-
  generate_scc(F,[A,B]),has_MR_property(F,[J,K]).

test_irat(F,[A,B],[J,K]):-
  generate_scc(F,[A,B]),test_irat_n2(F,[J,K]).

test_irmr(F,[A,B],[J,K]):-
  generate_scc(F,[A,B]),test_irat_n2(F,[J,K]),
  has_MR_property(F,[J,K]).

test_ess(F,[A,B],Is):-
  subset_of_agents(Is,_N),generate_scc(F,[A,B]),ess_monotone(F,Is).

test_ess1(F,[A,B],Is):-
  subset_of_agents(Is,_N),generate_scc(F,[A,B]),
  monotone(F,Is),\+ess_monotone(F,Is).

test_mono(F,[A,B],Is):-
  subset_of_agents(Is,_N),generate_scc(F,[A,B]), monotone(F,Is).



% -----------------------------------------------------------  %
%     A reversion function  h:S-->A. 
% -----------------------------------------------------------  %
% edited : Sep 2001.

% ---the reversion theorem of Nash Implementation Theory-----
% Recently Palfray and Srivastava proposed the another version of Nash 
% implementability  using reversion function and provided the proofs.
% If f is  not monotone, then it is not Nash implementable. But if f is 
% IR-monotone that it is monotone under reversion function with a fixed 
% status quo, H(y,s1,h)=w and H(y,s2,h)=y , then it is IR-implementable.
%  By this reversion, a reversal for the outcome z which has excluded 
% from SCC in stae s2 has occured for agent2 with another outcome y in 
% the range of the revised SCC. 

reversion(h0,_S,_A,_A).
reversion(h1,_S,_A,w).
reversions([h0,h1]).
% And a mapping, H:AxSx[F], induced by the reversion function h is
% H(a,s,h)=a if aR[i](s)h(s)  for all i;=h(s) otherwise.

reversed_map(H,S,A,A):-
    state(S),
    alternative(A),
    reversion(H,S,A,Ch),
    forall(agent(I),
      is_prefer_to(I,S,A,Ch)
    ).   %% -> Z = A; Z = Zh.

% probably, the cut, !, is implicit in if_then, ->, has a side-effect
% to exclude backtracking other tuples for reversed_map. 

reversed_map(H,S,A,Ch):-
   state(S),alternative(A),
   reversion(H,S,A,Ch),agent(I),
   \+ is_prefer_to(I,S,A,Ch).


/* 社会選択対応の重要な性質 単調性、ESS、ブロッキングなど */
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% some important conditions for sccs
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

% -----------------------------------------------------------  %
%    Maskin monotonicity: checking via lcc correspondence.
% -----------------------------------------------------------  %
% edited: Sep 2001. modified: 18 Oct 2001.
% 
% ---the basic theorem of Nash Implementation Theory-----
% Monotonicity is necessary for Nash-implementability if N>2, and 
% is also sufficient if NVP (no veto power) condition is satisfied.
% The proof of this fact proposed by Eric Maskin in 1970's at first
% and has elaborated by Vind, Repullo, and other game theorists. 


monotone(F):-
  agents(Is),
  monotone(F,Is).

monotone(F,Is):-
  scc(F),
  subset_of_agents(Is,_N),
  % there is a reversal everywhere an outcome retracted from scc.  
  forall(
     (
      state(S),
      scc(F,S,C),
      member(A,C),
      state(S1),% S1 \= S,
      scc(F,S1,C1),
      \+ member(A,C1),%write([A,member_of,C,in,S,out_of,C1,in,S1]),
      true),
     (
      member(I,Is),
      lcc([I,S,_R],A,K1),
      lcc([I,S1,_R1],A,K2),%wn([lcc_of,I,K1,K2]),
      \+ subtract(K1,K2,[]),%wn(ok),
      true)
   ).


% -----------------------------------------------------------  %
%           Strong Monotonicity (Essential Monotonicity)
% -----------------------------------------------------------  %
% added: May 2002.

% The properties of 'essentialy-monotone" sccs has explicated 
% in Danilov(1992) and the notion has cited by other papers.

% This shoud be modified so as to be under any subset of agents.
% ess-monotone scc is Nash-implementable if N>=3. Nevertheless,
% is generally not necessary for implementability, but so is when 
% universal domain or its strict part. You can use the condition-D
% by Yamato(1992) to check the domain model is safficient large so
% that ess-monotonicity become necessary condition. 



ess_monotone(F):-
  agents(Is),
  ess_monotone(F,Is).


%%% The difference between ess_monotnicity and (Maskin-)moinotonicity 
%%%  is only in the part [1] and [2] instead of using lcc per se.

ess_monotone(F,Is):-
  scc(F),
  subset_of_agents(Is,_N),
  % for each dropped scc element, there is a reversal in the ess_outcomes.  
  forall(
     (
      state(S),
      scc(F,S,C),
      member(A,C),
      state(S1),% S1 \= S,
      scc(F,S1,C1),
      \+ member(A,C1)
     ),
     (
      member(I,Is),
      lcc([I,S,_],A,Lcc1),  % [1]
      ess(F,I,Lcc1,Ess),    % [2]
      lcc([I,S1,_],A,Lcc2),
      \+ subtract(Ess,Lcc2,[])
     )
   ).


%%% essential set Ess (in the term of Danilov(1992)).

ess(F,I,X,Ess):-
   agent(I),scc(F),
   subset_of_alt(X,_),
   findall(A,
     S^R^(alternative(A),is_essential(A,X,[I,S,R],F)),
     Y),
   sort(Y,Ess).

ess_mon(F,I,X,Ess):-
   agent(I),scc(F),
   subset_of_alt(X,_),
   findall(A,
     S^R^(alternative(A),is_essential_mon(A,X,[I,S,R],F)),
     Y),
   sort(Y,Ess).

% subset of an ess
ess_subset(F,I,X,Ess):-
   agent(I),scc(F),
   subset_of_alt(X,_),
   subset_of_alt(Ess,_),
   forall(member(A,Ess),
     is_essential(A,X,[I,_S,_R],F)).

is_essential_mon(A,X,[I,S,R],F):-
% this definition of ess is of provided monotonicity
% for unristricted domain only
    preference(I,S,R),%wn([state,S,agent,I,preference,R]),
    scc(F,S,C),
    member(A,C),
    subset_of_alt(X,_),
    %maximal(A,X,[I,S,R]),
    lcc([I,S,R],A,Lcc),subset(X,Lcc),
    wn([maximal,A,in,X,pref,R]),
    alternatives(As),
    forall((agent(J),J\=I),lcc([J,S,_RJ],A,As)).

is_essential(A,X,[I,S,R],F):-
%    (var(X) -> write('set X is unspecified.'),nl,fail);
    subset_of_alt(X,_),
    agent(I),
    state(S),
    preference(I,S,R),
    scc(F,S,C),
    member(A,C),
    lcc([I,S,R],A,Lcc),
    subset(Lcc,X).
  %  forall(member(Y,X),alternative(Y)),  % subset(X,Alternatives),
  %  forall(member(Y,Lcc),member(Y,X)).   % subset(Lcc,X),
   % 注意:上の部分だけだと、Unboundになって∞ループする。




% -----------------------------------------------------------  %
% blocking and individual rationality (in Danilov(1992)).
% -----------------------------------------------------------  %
% added: Jan 2002.  modified: May,July,Aug,Sep 2002.

% blocking via scc 
% def. agent I blocks set B if there is a R(I) s.t.
%      intersection(Scc([R(I),R(-I)]), B) is empty. 

% to sepcify the preference with which the agent blocks an alternative.
is_blocked_by(X,J,[S,RJ],Is,F):-
    alternative(X),
    subset_of_agents(Is,_N),
    nth1(K,Is,J),
    state(S),
    preference(J,S,RJ),
    scc(F,S,_SccVal0),
    forall(
      (
       prefer_profile(Is,S1,R1),
       nth1(K,R1,RJ)
      ),
      (
       scc(F,S1,SccVal),
       \+member(X,SccVal)
      )
    ).

is_blocked_by(X,J,Is,F):-
    scc(F),
    subset_of_agents(Is,_),
    member(J,Is),
    preference(J,S,R),
    max_blocking(Bs,[J,S,R],Is,F),
    subset_of_alt(X,_),
    subset(X,Bs).


% maximal blocked set
max_blocking(Bs,[J,S,R],Is,F):-
    scc(F),
    subset_of_agents(Is,_),
    member(J,Is),
    preference(J,S,R),
    findall(X,
     (is_blocked_by(X,J,[S,R],Is,F)%,wn([X,J])
     ),
    Bs0), sort(Bs0,Bs).

% unblocked pair
% added : Aug 2002.

unblocked_pair([X1,X2],[J1,J2],F):-
    unblocked(X1,J1,[J1,J2],F),
    unblocked(X2,J2,[J1,J2],F).
unblocked0(X,I,Is,F):-
    scc(F),
    subset_of_agents(Is,_N),member(I,Is),
    subset_of_alt(X,_M),X\=[],
    forall(member(A,X),
      \+is_blocked_by(A,I,[_S,_R],Is,F)).
unblocked(X,I,Is,F):-
    scc(F),
    subset_of_agents(Is,_N),member(I,Is),
    subset_of_alt(X,_M),X\=[],
    \+ is_blocked_by(X,I,Is,F).

test_subadditivity([I,J],F,Result):-
    unblocked_pair([X,Y],[I,J],F),
    intersection(X,Y,W),
    Result=[unblocked,[X,Y],intersect,W].
test_sa(S,F):-results_to_file([test_subadditivity,[1,2],F,_R],'sa.txt',S).


% -----------------------------------------------------------  %
% blocking via mechanism (beta-blocking)
% -----------------------------------------------------------  %
% added: Jan 2002.

beta_blocking(J,Is,MJ,G,E,Blocked):-
    G =.. [_GF, _P, _Scc],
    agent(J),
    subset_of_agents(Is,_N),
    message(G,Is,J,MJ,true),
    findall(B,
     ( alternative(B),
       is_beta_blocked_by(B,J,Is,MJ,G,E))
    ,Blocked).

is_beta_blocked_by(X,J,Is,MJ,G,E):-
  % agents(Is),
    subset_of_agents(Is,N),
    member(J,Is),
  % state(S),
    E =.. [environment,[Is,_,_],[N,_,_],_],
    E,
    alternative(X),
    G =.. [GF, P, Scc],
    message(G,Is,J,MJ,true),
    \+ (
      mtest(GF,Msg1,Scc,Is),
      nth1(J, Msg1, MJ),
      member(P,[1,2,3]),
      mechanism(G,E,Msg1,C),
      member(X,C)
     ).


% -----------------------------------------------------------  %
% individual rationality (individually rational outcomes)
% -----------------------------------------------------------  %
% added: Jan 2002.  modified: May,July,Aug, resp., in 2002.
% note: this notion based on blocking differs from the IR wrt status quo. 


i_rationals(As,S,Rn,Is,F):-
    scc(F),
    subset_of_agents(Is,_),
    prefer_profile(Is,S,Rn),
    findall(A,
     (
      alternative(A),
      forall(member(J,Is),
       ( nth1(K,Is,J),
         nth1(K,Rn,RJ),
         is_I_rational(A,[J,S,RJ],Is,F)))
     ),
    As1),sort(As1,As).


is_I_rational(A,[J,S,RJ],Is,F):-
    subset_of_agents(Is,_N),
    scc(F),
    member(J,Is),
    preference(J,S,RJ),
    alternative(A),
    lcc([J,S,RJ],A,Lcc),
    \+is_blocked_by(Lcc,J,Is,F).

% for debug.
is_I_rational(A,[J,S,RJ],Is,F,test):-
    is_I_rational(A,[J,S,RJ],Is,F).
is_I_rational(A,[J,S,RJ],Is,F,test):-
    \+is_I_rational(A,[J,S,RJ],Is,F),
    alternative(A),
    preference(J,S,RJ),
    subset_of_agents(Is,_N),
    lcc([J,S,RJ],A,Lcc),
    scc(F,S,Scc),
    wn([alt,A,blocked_by_agent,J,in_state,S]),write(':'),
    wn([with_preference,RJ,lcc_is,Lcc, and_scc_is,Scc]).


% tests for IR
% edited: 

test_irat_n2(F,[I,J]):-
  scc(F),
  two_person([I,J]),
  forall(scc_defined_state(S,F), (
     test_irat_n2(F,[I,J],[S,_V,_A,yes])
   )).

test_irat_n2(F,[I,J],[S,V,A,B]):-
    scc(F,S,V),
    i_rationals(A,S,_R,[I,J],F),
    subset_query(V,A,B),
    wn([state,S,scc,V,ir_set,A,'ir?',B]).

subset_query(V,A,B):-
    subset(V,A) -> B = yes; B = no.


% checking some critical statements as for MR property in Danilov(1992) 
% using unblocked_pairs.
% added: Aug 2002.
 
test_dan55(S):-results_to_file([test_danilov_p55,mr,_R],'mr_dan55.txt',S).
test_danilov_p55(mr,Result):-
  scc(mr,S,C),
  member(A,C),
  lcc([1,S,R1],A,L1),lcc([2,S,R2],A,L2),
  (is_blocked_by(L1,2,[1,2],mr)->B1=lcc1_is_blocked_by_2;B1=unblocked),nl,
  (is_blocked_by(L2,1,[1,2],mr)->B2=lcc2_is_blocked_by_1;B2=unblocked),
  (is_MR_element(A,[L1,L2],[1,2],[[R1,R2],S],mr)->MR=is_mr_element;MR=no_mr),
  Result=[at,S,scc_element,A,lcc,[L1,L2],summary,[B1,B2,MR]].



% -----------------------------------------------------------  %
% Moore-Repullo property(Danilov,1992) for unrestricted domain
% with two agents.
% -----------------------------------------------------------  %
% edited from: Jan 2002.

% Condition of implementability for two-person case: 
% Scc F is implementable
%  <-> ess(F,Is),
%      has_MR_property(F,[J1,J2],X12),
%      forall((scc(F,S,C),member(A,C)),is_I_rational(A,Is,F)).


is_MR_element(A,[X1,X2],[J1,J2],[[R1,R2],S],F):-
    alternative(A),
    scc(F,S,C),
    member(A,C),
    prefer_profile([J1,J2],S,[R1,R2]),
    lcc([J1,S,R1],A,L1),
    lcc([J2,S,R2],A,L2),L1=X1,L2=X2.

is_MR_elements(MR,[X1,X2],[J1,J2],F):-
    scc(F),
    two_person([J1,J2]),
    subset_of_alt(X1,_N1),
    subset_of_alt(X2,_N2),
    findall(A,
      (
       scc_defined_state(S,F),
       prefer_profile([J1,J2],S,R),
       is_MR_element(A,[X1,X2],[J1,J2],[R,S],F)
      ),
    MR0),sort(MR0,MR).
  % it may have sorted by setof/3 but fail under MR=[].


has_MR_property(F,[J1,J2]):-
    scc(F),
    two_person([J1,J2]),
    forall(
      unblocked_pair([X1,X2],[J1,J2],F),
	% --note---The fact of existence of an unblocked pair can be 
	%  regarded as the analog of the 'self-selection constraint'
	%  in the term of Dutta-Sen(1991). ------- %
     (
      is_MR_elements(MR,[X1,X2],[J1,J2],F),MR\=[],
      wn(['MR-elements:',MR,'for unblocked pair:',[X1,X2]])
     )
   ).


ubp_test_mrp(F,[J1,J2],Result):-
    test_mrp_for_unblocked_pair(F,[J1,J2],Result).
test_mrp_for_unblocked_pair(F,[J1,J2],Result):-
    scc(F),
    two_person([J1,J2]),
      unblocked_pair([X1,X2],[J1,J2],F),
      scc(F,S,C),
      member(A,C),
      lcc([J1,S,_R1],A,L1),wn([lcc1,L1]),
      lcc([J2,S,_R2],A,L2),wn([lcc2,L2]),
      is_MR_elements(MR,[X1,X2],[J1,J2],F),
     Result=[state,S,scc,C,'MRs',MR,unblocked_pair,[X1,X2],lcc,[L1,L2]].


%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% some tests for blocking relations 

test_b(n,G,Is):-
   subset_of_alt(M,_),
   \+is_blocked_by(M,J,Is,G),
   wn([M,J,G]),
   fail.
test_b(y,G,Is):-
   subset_of_alt(M,_),
   is_blocked_by(M,J,[S,_R],Is,G),
   wn([M,J,S,G]),
   fail.

test_blocking(F,FileName):-
    concat('block_',F,A),
    concat(A,'.txt',FileName),
    open(FileName,write,_Strm),
    test_blocking(F,_J,_Y,_Z),fail.

test_blocking(_,FileName):-
    current_stream(FileName,write,Strm),
    close(Strm).

test_blocking(F,J,Is,Y,Z):-
    subset_of_agents(Is,_N),member(J,Is),
    max_blocking(Y,[J,S,R],Is,F),
    current_stream(_,write,Strm),
    nl(Strm),
    wn(Strm,[Y,'is blocked','by',J,'under scc',F,when,[S,R]]),
    ess(F,J,Y,Z),
   % If the Scc is ess-monotone, then ess is empty for an agent 
   % iff X is blocked by the agent. (proposition 3)
    wn(Strm,[' ess',Z]),
    forall(
      (state(S1),prefer_profile(_Is,S1,R1),nth1(J,R1,_RJ)),
      (scc(F,S1,SccVal1),
       intersection(Y,SccVal1,Meet),
       % by definition, the meet of scc values and blocked set is empty.
       write(Strm,' state='),write(Strm,S1),
       write(Strm,' scc='),write(Strm,SccVal1),
       write(Strm,' preference='),wn(Strm,R1),
       write(Strm,' =>intersection(scc,blocked)='),wn(Strm,Meet))),nl(Strm).

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% tests for proposition 3 of Danilov(1992) 

test_proposition(3,F,FileName):-
    concat('prop3_',F,A),
    concat(A,'.txt',FileName),
    open(FileName,write,_Strm),
    proposition(3,F,[_I,_S,_Z]),fail.
test_proposition(3,_,FileName):-
    current_stream(FileName,write,Strm),
    close(Strm).

proposition(3,F,[I,S,Z]):-
     scc(F,S,Scc),
     state(S),
     agent(I),
     current_stream(_,write,Strm),
     alternative(X),
     alternatives(A),
     findall(Lcc,(lcc([I,S,_R],X,Lcc)),D),
     nl(Strm),
     wn(Strm,[scc, F, agent,I,state,S,scc_val,Scc,lccs,D]),
     findall(Y,L^(
           member(L,D),
           alternative(Y),
           \+member(Y,L)),
        Hyp),
     subtract(A,Hyp,Inf),
     intersection(Scc,Inf,Z),%Z = [],
     tab(Strm,3),write(Strm,[hyp,Hyp]),
     tab(Strm,3),write(Strm,[inf,Inf]),
     wn(Strm,['scc∩inf',Z]),agents(Is),
     is_blocked_by(Inf,I,Is,F),ess(F,I,inf,Ess),
     wn(Strm,[agent,I,blocks,Inf,and_ess_is,Ess]).



/*   Other important correspondences    */

    %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
    %%   Pareto, Condorcet, Dictatorial, NVP, RVP. %%
    %%   : with unanimity, minimal liberalism, etc.
    %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% added:  15-18 Aug 2002 

% -----------------------------------------------------------  %
% the (weak) Pareto optimal correspondence 
% -----------------------------------------------------------  %
% w.r.t. any preference domain coded in prolog-db.
% {a|for all b in A there exists an agent i, s.t., 
% is_prefer_to(i,S,a,b)},for any state S (and preference R(S)).

has_pareto_property(F,Is):-
   scc(F),
   subset_of_agents(Is,_),
   forall(scc(F,S,C),(wpo(Cpo,Is,S),subset(C,Cpo))).

% weak pareto optimal correspondence.
wpo(Cpo,Is,S):-
   subset_of_agents(Is,_),
   state(S),
   findall(A,is_wpo(A,S,Is),Cpo0),
   sort(Cpo0,Cpo).

% partial version.
partial_wpo(Cpo,Is,S):-
   subset_of_agents(Is,_),
   subset_of_alt(Cpo,_),
   state(S),
   forall(member(A,Cpo),is_wpo(A,S,Is)).

% alternative A is efficient for agent J in state S.
is_wpo(A,S,Is):-
   is_weak_parete_optimal(A,S,Is).
is_weak_parete_optimal(A,S,Is):-
   subset_of_agents(Is,_),
   %preference_profile(Is,S,_P),
   state(S),
   alternative(A),
   forall(alternative(B),is_prefer_to(_J,S,A,B)).

% -----------------------------------------------------------  %
% the majority rule for strict preferences
% -----------------------------------------------------------  %

has_condorcet_property(F,Is):-
   scc(F),
   subset_of_agents(Is,_),
   forall(scc(F,S,C),(condorcet(Con,Is,S),subset(C,Con))).

condorcet(Con,Is,S):-
   subset_of_agents(Is,_),
 %  subset_of_alt(Con,_),
   state(S),
   findall(A,(
    alternative(A),
    forall(alternative(B),
    pairwise_majority(A,B,_Na,_Nb,S,Is))
   ),Con0),
  sort(Con0,Con).

pairwise_majority(A,B,Na,Nb,S,Is):-
   subset_of_agents(Is,_),
   state(S),
   alternative(A),
   alternative(B),
   bagof(J,(member(J,Is),is_prefer_to(J,S,A,B)),Jas),
   bagof(J,(member(J,Is),is_prefer_to(J,S,B,A)),Jbs),
   length(Jas,Na),
   length(Jbs,Nb),
   Na >= Nb.



% -----------------------------------------------------------  %
% dictator, dictatorial scc
% -----------------------------------------------------------  %

dictatorial(F,Is):-
   scc(F),
   subset_of_agents(Is,_),
   member(J,Is),
   is_a_dictator(J,F,Is).

is_a_dictator(J,F,Is):-
   subset_of_agents(Is,_),
   agent(J),member(J,Is),
   scc(F),
   alternatives(Alts),
   forall((scc(F,S,C),member(A,C)),
     lcc([J,S,_R],A,Alts)
   ),
   forall(lcc([J,S,_R],A,Alts),
     (scc(F,S,C),member(A,C))
   ).

% -----------------------------------------------------------  %
% NVP (no veto power) and RVP (restricted veto power)
% -----------------------------------------------------------  %
% note: rvp/2, the ristricted version of nvp in the sense 
%  that there is no_veto_power unless  the outcome 
%  is strictly worse tha any outcome in range(scc). 
% -----------------------------------------------------------  %

nvp(F,Is):-
   no_veto_power(F,Is,full).

nvp0(F,Is):-
   no_veto_power0(F,Is,full).

nvp1(F,Is):-
   no_veto_power1(F,Is,full).

rvp(F,Is):-
   no_veto_power(F,Is,ristricted).

unanimity(F,Is):-
   subset_of_agents(Is,_),
   scc(F),
   alternatives(As),
   forall(
    (
     alternative(A),
     scc_defined_state(S,F),
     findall(J,(member(J,Is),lcc([J,S,R],A,As)),Is0),
     sort(Is0,Is)
    ),
    (scc(F,S,C), wn([[unanimity,Is0,A],[scc,S,C]]),
     member(A,C),
     forall(lcc([J,S,R],A,L),
     wn([ok,[preference,J,S,R],[lcc,A,L]])))
   ).


% agent has a power to veto the outcome under scc
%(=blocking+some_additional_power).
veto_outcome(A,J,S,Is,F):-
   subset_of_agents(Is,_),
   scc(F),
   agent(J),
   state(S),
   scc(F,S,C),
   alternative(A),
   \+member(A,C),
   alternatives(As),
   forall((agent(K),K\=J),
     lcc([K,S,_Rk],A,As)
   ).


% nvp by using lcc:  (equivalence has confirmed as for 
% no_veto_power0/ using veto_outcome, or no_veto_power1/ using weak).

no_veto_power(F,Is,full):-
   subset_of_agents(Is,_),
   scc(F),
   alternatives(As),
   forall(
    (
     alternative(A),
     scc_defined_state(S,F),
     agent(I),member(I,Is),
     subtract(Is,[I],Is1),
     findall(J,lcc([J,S,R],A,As),Is0),
     subset(Is1,Is0)
    ),
    (scc(F,S,C),
     member(A,C),  wn([[nvp,Is0,A],[scc,S,C]]),
     forall(lcc([J,S,R],A,L), wn([ok,[preference,J,S,R],[lcc,A,L]]))
    )
   ).


no_veto_power(F,Is,ristricted):-
   subset_of_agents(Is,_),
   scc(F),
   range(F,Bs),
   forall((agent(J),member(J,Is),
       alternative(A),scc_defined_state(S,F)),
     (
      \+veto_outcome(A,J,S,Is,F);
      (
       member(B,Bs),
       \+is_prefer_to(J,S,A,B)
      )
     )
   ).

%

no_veto_power0(F,Is,full):-
   subset_of_agents(Is,_),
   scc(F),
   forall((agent(J),member(J,Is),
        alternative(A),scc_defined_state(S,F)),
     (
      \+veto_outcome(A,J,S,Is,F)
     )
   ).

% NVP <--> no agent has veto outcome <--> all agent are weak.
no_veto_power1(F,Is,full):-
   subset_of_agents(Is,_),
   scc(F),
   forall((agent(J),member(J,Is)),weak(J,Is,F)).

% an agent is "weak" if it has no veto outcome.
% note: in this case ess(F,J,X,X) always hold.

weak(J,Is,F):-
   subset_of_agents(Is,_),
   scc(F),
   agent(J),
   \+veto_outcome(_A,J,_S,Is,F).

% agent J is weak <--> J blocks only [].
weak_b(J,Is,F):-
   subset_of_agents(Is,_),
   scc(F),
   agent(J),
   \+ (alternative(A),
   is_blocked_by(A,J,[_S,_R],Is,F)).

r_weak(J,Is,F,_):-
   weak(J,Is,F).
r_weak(J,Is,F,restricted):-
   subset_of_agents(Is,_),
   scc(F),
   agent(J),member(J,Is),
   forall(
     veto_outcome(A1,J,S1,Is,F),
    (wn([found_veto_outcome,A1,by,J,when,S1]),
     range(F,Bs),
     member(B,Bs),
     \+is_prefer_to(J,S1,A1,B)
     ,tab(2),wn([but_is_strongly_wrose_than,B])
    )
   ).


%lemma: weak-> lcc(X)=X, nvp->ess(X)=X.

test_lemma_weak(J,Is,F,R):-
  member(R,[full,restricted]),wn(R),
  forall(
    (
     agent(J),member(J,Is),
     subset_of_alt(X,_),
    true),
    (r_weak(J,Is,F,R)
    ->
     ess(F,J,X,X)
    )
  ).
   
test_lemma_nvp(F,Is,R):-
  member(R,[full,restricted]),wn(R),
  no_veto_power(F,Is,ristricted),wn(nvp),
  %
  forall(
    (alternative(A),
     agent(J),member(J,Is),
     scc_defined_state(S,F)
    ),
    (set_C_star(X,_,[[J,S,R],A,_Bstar],Is,F)
    ->
     lcc([J,S,R],A,X)
    )
  ).


tell_test_nvp(Mju):-
  subset_of(Mju,_,[i,ii,iii,iv]), 
  open('mju.txt',write,S),
  tell('mju.txt'),
  condition_mju(mr,[1,2],_B,[yes,yes],Mju),
  tell(user),wn(end),
  current_stream('mju.txt',write,S),
  close(S).



% tests for equivalence of some versions of nvp
test_nvp_def:-
   forall(
    (member(P,[a1,a2,b1,b2]),
     member(R,[full,restricted])
    ),
    (wn([P,R]),
     (test_nvp(P,R)->wn([found_diff_in,P,R]);true)
    )
   ),
   wn([no_difference_has_found_in_3_versions_of_no_veto_power]).
test_nvp(a1,R):-
   member(R,[full,restricted]),wn(R),
   \+no_veto_power(F,Is,R),
   no_veto_power0(F,Is,R),
   wn([is,no_veto_power0, but_is_not, no_veto_power]).
test_nvp(a2,R):-
   member(R,[full,restricted]),wn(R),
   no_veto_power(F,Is,R),
   \+no_veto_power0(F,Is,R),   % take a minute
   wn([is,no_veto_power, but_is_not, no_veto_power0]).

test_nvp(b1,R):-
   member(R,[full,restricted]),wn(R),
   \+no_veto_power(F,Is,R),
   no_veto_power1(F,Is,R),
   wn([is,no_veto_power1, but_is_not, no_veto_power]).
test_nvp(b2,R):-
   member(R,[full,restricted]),wn(R),
   no_veto_power(F,Is,R),
   \+no_veto_power1(F,Is,R),
   wn([is,no_veto_power1, but_is_not, no_veto_power1]).



% -----------------------------------------------------------  %
%  bad_outcome, nonempty_lower_intersection
% -----------------------------------------------------------  %
% 18 Aug 2002.
% reference: M_R(1990), p.1090.


bad_outcome(Z,F,Is):-
   scc(F),
   subset_of_agents(Is,_),
   alternative(Z),
   range(F,B),
   forall(
     (
      member(X,B),
      member(J,Is),
      state(S)
     ),
   is_strict_prefer_to(J,S,X,Z)
  ).


bad_outcome1(Z,F,Is):-
% note: in this version, if the scc maps into the out of 
% the set of alternatives, it is vacuously true.
   scc(F),
   subset_of_agents(Is,_),
   alternative(Z),
   range(F,B),
   \+ (member(J,Is),member(X,B),state(S),is_prefer_to(J,S,Z,X)).


%no_empty_lower_intersection (neli) for N=2.
neli(F,Is):-
   scc(F),
   subset_of_agents(Is,_),
   forall(
     neli(F,Is,[_,_,_,SL12]),
     SL12 \= []
   ).

neli(F,[J1,J2],[[R1,R2],[X,Y],[SL1,SL2],SL12]):-
   scc(F),
   subset_of_agents([J1,J2],_),
   scc(F,S1,C1),
   scc(F,S2,C2),
   member(X,C1),
   member(Y,C2),
   slcc([J1,S1,R1],X,SL1),
   slcc([J2,S2,R2],Y,SL2),
   intersection(SL1,SL2,SL12).  


% -----------------------------------------------------------  %
% decisiveness and minimal liberalism(ML).
% -----------------------------------------------------------  %
% 19 Aug 2002.
% reference: Peleg(1998), p.76.

is_decisive(J,for(X),over(Y),F):-
   scc(F),
   agent(J),
   alternative(X),
   alternative(Y),Y\=X,
   forall( 
     ( preference(J,S,R),
       subset_of_alt(_B,_) ),
     ( forall(  
        ( slcc([J,S,R],X,SL),
          member(Y,SL),
          scc(F,S,C),
          \+member(X,C)
         ),
        \+member(Y,C))
     )
   ).


% Sen's weakest condition of liberalism (ML).

mlib(F,Is):-
   scc(F),
   subset_of_agents(Is,_),
   subset_of([J1,J2],2,Is),
  % member(J1,Is),member(J2,Is),J2\=J1,
   decisive_pairs([J1,_X,_Y],[J2,_Z,_W],F).

decisive_pairs([J1,X,Y],[J2,Z,W],F):-
   agent(J1),
   agent(J2),
   alternative(X),
   alternative(Y),
   alternative(Z), Z\=X, 
   alternative(W), W\=Y,
   is_decisive(J1,for(X),over(Y),F),
   is_decisive(J2,for(Z),over(W),F).


% -----------------------------------------------------------  %
%  neutrality of scc wrt permutation of the alternatives
% -----------------------------------------------------------  %
%  it is always true that scc(permutated_preference)=permutation(scc).
% added: 1 Sep 2002.

%caution:
%notations 'A->B's bellow have cause precedence errors in IF-prolog.

is_neutral(F,Is):-
   scc(F),
   subset_of_agents(Is,_),
   forall( % -----forall (1)---------%
     (
      poa(_,PoA),
      ppp(Is,PoA,Ps->Rs)
     ),
     (
      forall( % -----forall (2)---------%
        (
         state(S),prefer_profile(Is,S,Ps),
         scc(F,S,C),member(C0,C)
        ),
        (
         state(S1),prefer_profile(Is,S1,Rs),
         scc(F,S1,C1),
         member(C0->X,PoA),
         member(X,C1)
        )
      )% ----end forall (1)------%
     )% -----end forall (2)---------%
   ).

ppp(Is,PoA,Rtrans):-
   permutated_prefer_profile(Is,PoA,Rtrans).

permutated_prefer_profile(Is,PoA,Ps->Rs):-
   subset_of_agents(Is,_),
   alternatives(A),
   state(S),
   prefer_profile(Is,S,Ps),
   ordering(P,A,_M),
   poa(P,PoA),!,%wn(PoA),
   bagof(R,
     K^J^Q^(
       nth1(K,Is,J),
       nth1(K,Ps,Q),
       permutate_of_order(PoA,[Q->R])
     ),
    Rs).

/*
%   --------permutation of outcomes (citation from earlier part)-------
poa(P,APs):-
   alternatives(A),
   permutation_of(A,P,APs).
 % <-----  omitted ------>
permutate_of_order(PoA,[Q->R]):-
   poa(_P,PoA),
   alternatives(A),
   length(A,M),
   ordering(Q,A,M),%wn(Q),
   ordering(R,A,M),%wn(R),
   permutation(Q,PoA,R).
 % <-----  omitted ------>
%   ---------------( end of citation )----------
%
*/


% -----------------------------------------------------------  %
% Condition M, M2 and iterative elimination of awkward outcomes.
% with the sets B_star and C_star.
% -----------------------------------------------------------  %
% 20,23 Aug 2002.
% reference: Sjostrom(1991), p.336. Maskin and Sjostrom(2002),Suh(1996).
%


/*
  %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
  %%% Sjostrom's Iterative Elimination 
  %%% ( in order for awkwardlessness )
  %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
*/
% edited: Aug 2002.
% an algorithm for computing the set B_star iteratively, up to 
% the convergence of the sequence {B_k}.

set_B_star(Bstar,Kmin,Is,F):-
   (scc(F)->true;(!,fail)),
   subset_of_agents(Is,_),
   % the first fixed point, CB, of the sequece of set operations
   set_Bk([Kmin|_],Bk-Bk,Is,F),
   Bstar=Bk,!.

set_Bk([1|[]],B0-[],Is,F):-
   (scc(F)->true;(!,fail)),
    subset_of_agents(Is,_),
    alternatives(As),
    B0=As.
set_Bk([K|[K1|H1]],Bk-Bk1,Is,F):-
    set_Bk([K1|H1],Bk1-_,Is,F),
    K is K1 + 1,
    findall(A,
      (
       member(A,Bk1),
       (
        scc_defined_state(S,F),
        scc(F,S,V),
        (
         forall(member(J,Is),maximal(A,Bk1,[J,S,_R]))
         -> member(A,V);true
        )
       )
      ),
    B0),sort(B0,Bk).

% the sets C_k and C_star.

test_Ck(K,C,A):- generate_scc(scc1,_),set_Ck([K|_],C,A,[1,2,3],scc1).
test_C_star(K,C,A):- generate_scc(scc1,_),set_C_star(C,K,A,[1,2,3],scc1).

set_C_star(Cstar,Kmin,[[J,S,R],A,Bstar],Is,F):-
   (scc(F)->true;(!,fail)),
   scc(F),
   subset_of_agents(Is,_),
    member(J,Is),
    preference(J,S,R),
    scc(F,S,V),
    member(A,V),
   set_Ck([Kmin|_],Ck-Ck,[[J,S,R],A,Bstar],Is,F),
  % subset_of_alt(Bstar,_),  <--- never before set_Ck because of using !.
  % subset_of_alt(Ck,_),  <--- never before set_Ck because of using !.
   Cstar=Ck,!.

set_Ck([1|[]],C1-[],[[J,S,R],A,Bstar],Is,F):-
   (scc(F)->true;(!,fail)),
    subset_of_agents(Is,_),%wn([F,Is]),
    member(J,Is),%wn(J),
    preference(J,S,R),%wn([J,S,R]),
    scc(F,S,V),%wn([F,S,V]),
    member(A,V),
   %wn(A),
    lcc([J,S,R],A,Lcc),%wn([A,Lcc]),
    set_B_star(Bstar,_,Is,F),%wn(Bstar),
    intersection(Lcc,Bstar,C1).
set_Ck([K|[K1|H1]],Ck-Ck1,[[J,S,R],A,Bstar],Is,F):-
    length([K|[K1|H1]],K),  % <-miso
    set_Ck([K1|H1],Ck1-_,[[J,S,R],A,Bstar],Is,F),
    K is K1 + 1,
    findall(B,
      (
       member(B,Ck1),
       (
        scc_defined_state(S,F),
        scc(F,S,V),
        (
         (maximal(B,Ck1,[J,S,R]),
          forall((member(J1,Is),J1\=J),
            maximal(B,Bstar,[J1,S,R])
          )
         )
         -> member(B,V);true
        )
       )
      ),
    C0),sort(C0,Ck).

/*
    %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
    %%%  re_definition: B / C_stars  %%
    %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
*/
% see Sjostrom(1991), p.335.
% the code bellow replicate the original definition for B_star and C_star
% these definitions for Bx and Cx are yet incomplete, til 020820. (pending)

% test routine
test_Bx1(C,Bx):-
   generate_scc(scc1,C),definition_of_B_star(Bx,[1,2,3],scc1).
test_Bx2(C,Bx):-
   Is=[1,2,3],
   generate_scc(scc1,C),
   set_B_star(Bx,_,Is,scc1),
   wn(['found Bx:',Bx]),
   definition_of_B_star(Bx,Is,scc1).
test_Cx1(C,Cx,A):-
   generate_scc(scc1,C),definition_of_C_star(Cx,A,[1,2,3],scc1).
test_Cx2(C,Cx,A):-
   Is=[1,2,3],
   generate_scc(scc1,C),
   set_C_star(Cx,_,[[J,S,R],A,Bx],Is,scc1),
   wn(['found Cx:',Cx,prof,[J,S,R],outcome,A,'Bx:',Bx]),
   definition_of_C_star(Cx,[[J,S,R],A,Bx],Is,scc1).


definition_of_B_star(B_star,Is,F):-
   subset_of_agents(Is,_),
   subset_of_alt(B_star,_),
   findall(B,
     (
       %condition_mju_iii in the sense of Moore-Repullo(1990)
       condition_mju(F,Is,B,[no,no],[iii])
     ),
   BA),
   all_members(BA,B_star),flatten(BA,BC),wn(BC).


 %% should be! equivalent to  set_C_star(Cstar,_K,[[J,S,R],A,Bstar],Is,F).
 %% notice: if scc satisfies nvp, C_star = Lcc.

definition_of_C_star(C_star,[[J,S,R],A,Bstar],Is,F):-
   subset_of_agents(Is,_),
   scc(F),
   (
     alternative(A),
     state(S),
     member(J,Is),
     preference(J,S,R),
     scc(F,S,C),member(A,C),  wn([[J,S,R],A])
   ),
   findall(C0,
     (
       lcc([J,S,R],A,Lcc),
       set_B_star(Bstar,_Kmin,Is,F),  % substituted for def of it. 
       intersection(Lcc,Bstar,C0),
       %condition_mju_ii in the sense of Moore-Repullo(1990)
       condition_mju_ii(F,Is,[Bstar,C0],A,[J,S,R]),wn([C0,Bstar])
     ),
   CA),
   all_members(CA,CA0),sort(CA0,C_star).


/*
    %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
    %%%    Conditions M and  M2   %%%
    %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
*/
% see Sjostrom(1991), p.335.
% modified: 27 Sep 2002.

condition_M(F,Is):-
      condition_mju(F,Is,_Bx,[yes,yes],[i]).

condition_M2(F,[J1,J2]):-
      condition_mju(F,[J1,J2],_Bx,[yes,yes],[i,iv]).


/*
    %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
    %%%   Condition μ: i,ii,iii  μ2: i〜iv %%%
    %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
*/
% Originally by Moore-Repullo(1990) and independently Dutta-Sen(1991).
% As for the formalization here, see Sjostrom(1991), pp.334-5.
% added: 21-3 Aug 2002.
% modified: 27 Sep 2002.
% modified: 10 Nov 2002.  suppressed write sentences.


condition_mju2(F,[J1,J2],Bx,[GoBx,GoCx]):-
   condition_mju(F,[J1,J2],Bx,[GoBx,GoCx],[i,ii,iii,iv]).

condition_mju(F,Is,Bx,[GoBx,GoCx],Mju):-
   T=no,
   subset_of(Mju,_,[i,ii,iii,iv]),
   scc(F),
   subset_of_agents(Is,_),
   (GoBx=yes -> set_B_star(Bx,_,Is,F);true),
   subset_of_alt(Bx,_),  % <-- note! it should be done after set_B_star/4.
   (T=yes->(wn([bx,Bx,mju,Mju]));true),
   forall(
     (
      alternative(A),state(S),
      collect_cx(A,S,F,Is,Bx,[GoBx,GoCx],Cxs)
     ),
     (
      % sub-conditions of mju and mju2 in Moore-Repullo(1990)
      forall(
        (member(M,Mju),member(M,[i,ii,iii])),
        (
         sub_condition_of_mju(M,F,Is,Bx,[A,S,Cxs]),
         (T=yes->(tab(2),wn([ok_mju,M]));true)
        )
      )
     )
   ),
   (member(iv,Mju)
    ->
     (sub_condition_of_mju(iv,F,Is,_,_),
      (T=yes->(tab(2),wn([ok_mju,iv]));true)
     )
    ;true
   ).



% utility for condition_mju /4
% modified: 28 Sep 2002.

collect_cx(A,S,F,Is,Bx,[GoBx,GoCx],Cxs):-
      T=no,
      alternative(A), scc(F,S,V),member(A,V),
      (T=yes->(tab(1),wn([A,in_scc(F,S,V)]));true),
      subset_of_agents(Is,_),
      (GoBx=yes,set_B_star(Bx,_,Is,F)),
      subset_of_alt(Bx,_),  % <-- it should be after set_B_star/4.
      bagof([J,A,S,Cx],
        R^Lcc^Wth^Nx^
        (
         agent(J), member(J,Is), preference(J,S,R),
          (GoCx=yes,set_C_star(Cx,Wth,[[J,S,R],A,Bx],Is,F)),
          (subset_of_alt(Cx,Nx)->true),
          member(A,Cx),
          lcc([J,S,R],A,Lcc),
          subset(Cx,Lcc),
          subset(Cx,Bx),
          (T=yes->(tab(2),wn([A,prefer(J,S,R),cx(Cx),lcc(Lcc),bx(Bx)]));true)
        ),
      Cxs).

% only for 2 person case. 
make_set_Cx_for([[J,S,R],A],Cx,Lcc,Bx,[J1,J2],F,yes):-
     member(J,[J1,J2]),
     set_C_star(Cx,_,[[J,S,R],A,Bx],[J1,J2],F),  %wn([cx,Cx,bx,Bx]),
     subset_of_alt(Cx,_),member(A,Cx),   %wn(A),
     lcc([J,S,R],A,Lcc),    %write([lcc,Lcc]),
     subset(Cx,Lcc),
     subset(Cx,Bx).

/*
    %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
    %%%   subsidiary conditions for μ and μ2   %%%
    %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
*/
% see Sjostrom(1991).


sub_condition_of_mju(i,F,Is,_Bx,[A,S,Cxs]):-
% this condition corresponds to mju (i), (strong) monotonicity
% of the Moores-Repullo's condition. 
   T=no,
   scc(F),
   subset_of_agents(Is,_),
   alternative(A),
%   subset_of_alt(Bx,_), 
   forall(
     (
      scc_defined_state(S1,F),
      prefer_profile(Is,S1,Rs),
      (T=yes->(tab(4),wn([profile(S1),Rs]));true),
      forall(
        (agent(J),member(J,Is)),
        (
         member([J,A,S,Cx],Cxs),  % Cx for state S, not for S1.
         maximal(A,Cx,[J,S1,_R]),
         (T=yes->(tab(5),wn([is_max_for_Cx(A,Cx),agent(J),state(S1)]));true)
       % ------- a substitute for maximal(A,Cx,[J,S1,_R])----------
       % preference(J,S1,R),
       % lcc([J,S1,R],A,Lcc),subset(Cx,Lcc)
       % ,tab(5),wn([A,is_maximal_for,J,in_state,S1,lcc,Lcc,wrt_Cx,Cx])
       % ---------------------------------------------------------
        )
      )
     ),
     (
      scc(F,S1,V), %tab(6),write(scc(S1,V)),
      member(A,V) %,wn(in_scc(A))
     )
   ).


sub_condition_of_mju(ii,F,Is,Bx,[C,S,Cxs]):-
% this corresponds to Moores-Repullo's condition, mju (ii), rvp. 
   T=no,
   scc(F),
   subset_of_agents(Is,_),
   alternative(C),
   subset_of_alt(Bx,_), 
   forall(
     (
      scc_defined_state(S1,F),
      prefer_profile(Is,S1,Rs),
      (T=yes->(tab(4),wn([profile(S1),Rs]));true),
      member([J0,A,S,Cx],Cxs),  % state S, not S1.
      agent(J0),member(J0,Is),
      state(S1),alternative(C),
      lcc([J0,S1,_R0],C,Lcc),subset(Cx,Lcc),
      (T=yes->(tab(5),wn([is_max_for_Cx(A,Cx),agent(J0),state(S1)]));true),
      %-------
      subtract(Is,[J0],Is1),
      forall(
        (agent(J),member(J,Is1)),
        (
         maximal(A,Bx,[J,S1,_R]),
         (T=yes->(tab(5),wn([is_max_for_Bx(A,Bx),agent(J),state(S1)]));true)
        )
      )
     ),
     (
      scc(F,S1,V), %tab(6),write(scc(S1,V)),
      member(A,V)  %,wn(in_scc(A))
     )
   ).


sub_condition_of_mju(iii,F,Is,Bx,[C,_S,_Cxs]):-
% this corresponds to Moores-Repullo's condition, mju (iii), 
% (restricted) unanimity. 
   T=no,
   scc(F),
   subset_of_agents(Is,_),
   alternative(C),
   subset_of_alt(Bx,_), 
   forall(
     (
      scc_defined_state(S1,F),
      prefer_profile(Is,S1,Rs),
      (T=yes->(tab(4),wn([profile(S1),Rs]));true),
      %-------
      forall(
        (agent(J),member(J,Is)),
        (
         maximal(A,Bx,[J,S1,_R]),
         (T=yes->(tab(5),wn([is_max_for_Bx(A,Bx),agent(J),state(S1)]));true)
        )
      )
     ),
     (
      scc(F,S1,V), %tab(6),write(scc(S1,V)),
      member(A,V)  %,wn(in_scc(A))
     )
   ).


sub_condition_of_mju(iv,F,[J1,J2],_,_):-
% this corresponds to Moores-Repullo's condition, mju (iv),for N=2. 
   T=no,
   forall(
     (
      alternative(A),alternative(B),
      %you may not use instead 'subset_of_alt([A,B],2)'
      preference(J1,S1,R1),
      preference(J2,S2,R2),
      scc(F,S1,V1),member(A,V1),
      scc(F,S2,V2),member(B,V2),
      (T=yes->(tab(4),wn([scc_pair,[J1,S1,A],[J2,S2,B]]));true)
     ),
     (% ----- the 'self-selection constraint' in the term of Dutta-Sen(1991).
      make_set_Cx_for([[J1,S1,R1],A],Cx1,_L1,Bx,[J1,J2],F,GoCx),
      make_set_Cx_for([[J2,S2,R2],B],Cx2,_L2,Bx,[J1,J2],F,GoCx),
      intersection(Cx1,Cx2,MR),
      member(Phi,MR),
      (T=yes->(tab(5),wn([mr,Phi,in_C1xC2,MR]));true),
      forall(
        (
         lcc([J1,Sp,_R1p],Phi,Lp1),
         lcc([J2,Sp,_R2p],Phi,Lp2),
         subset(Cx1,Lp1),
         subset(Cx2,Lp2),
         (T=yes->(tab(6),write([for_lcc_pair,Lp1,Lp2]));true)
        ),
        (
         scc(F,Sp,Vp),member(Phi,Vp) %,tab(2),wn(in_scc)
        ) 
      )
     )
   ).


/*
    %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
    %%%  MR outcomes in M-R mechanism  %%%
    %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
*/
% this is used in the cases of gMR bellow.
% added 25 Aug 2002.
% modified 27 Sep 2002.

mre(Y,F,[[X1,X2],[J1,J2],[S1,S2],[R1,R2]],[Cx1,Cx2],T):-
    %alternative(X1),
    %alternative(X2),
    (T=yes->(tab(1),wn([mre_start,[X1,X2],[J1,S1,R1],[J2,S2,R2],F]));true),
    %-----------
     preference(J1,S1,R11),
     scc(F,S1,V1),
     member(X1,V1),
    (T=yes->(tab(2),wn([[J1,S1,R11],scc,V1,X1]));true),
    %-----------
     preference(J2,S2,R21),
     scc(F,S2,V2),
     member(X2,V2),
    (T=yes->(tab(2),wn([[J2,S2,R21],scc,V2,X2]),
    %-----------
    tab(4),wn([for_scc_pair,[J1,S1,X1],[J2,S2,X2]]));true),
     set_C_star(Cx1,_,[[J1,S1,R1],X1,Bx],[J1,J2],F),
     set_C_star(Cx2,_,[[J2,S2,R2],X2,Bx],[J1,J2],F),
     intersection(Cx1,Cx2,MR),
    (T=yes->(tab(6),wn([cx1,Cx1,cx2,Cx2,mre,MR]));true),
     member(Y,MR),
     alternative(Y),
    (T=yes->(tab(8),wn([mr_end,Y,'in_Cx1*Cx2']));true).



/*
    %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
    %%%    some tests for conditions μ and μ2   %%%
    %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
*/

test_mju_ud(F,Is,Bx,Mju):-
  subset(Mju,[i,ii,iii]),
  generate_scc(scc1,F),condition_mju(scc1,Is,Bx,[yes,yes],Mju).

test_mju_ud(F,[J1,J2],Bx,iv):-
  generate_scc(scc1,F),
  condition_mju2(F,[J1,J2],Bx,[yes,yes]).

tell_test_mju(Mju):-
  subset_of(Mju,_,[i,ii,iii,iv]), 
  open('mju.txt',write,S),
  tell('mju.txt'),
  condition_mju(mr,[1,2],_B,[yes,yes],Mju),
  tell(user),wn(end),
  current_stream('mju.txt',write,S),
  close(S).


tell_test_mju2:-
  open('mju2.txt',write,S),
  tell('mju2.txt'),
  condition_mju2(mr,[1,2],_B,[yes,yes]),
  tell(user),wn(end),
  current_stream('mju2.txt',write,S),
  close(S).


/*
    %%%%%%%%%%%%%%%%%%%%%%%%%%%%%
    %%%    awkward outcomes   %%%
    %%%%%%%%%%%%%%%%%%%%%%%%%%%%%
*/
% added and modified 23-4 Aug 2002.
% see Maskin and Sjostrom(2002).


is_awkward(C,[[J,S,R],A],[S1,C,Lcc1],Is,F):-
    alternatives(As),
    subset_of_agents(Is,_),
    member(J,Is),
    scc_defined_state(S,F),
    alternative(A),
    scc(F,S,V),member(A,V),
    preference(J,S,R),
    lcc([J,S,R],A,Lcc),
    alternative(C),member(C,Lcc),
    scc_defined_state(S1,F),
    scc(F,S1,V1),\+member(C,V1),
   %
    preference(J,S1,R1),
    lcc([J,S1,R1],C,Lcc1),
    subset(Lcc,Lcc1),
    wn([[scc,V,S],[agent,J,[lcc,A,Lcc]]]),
    write('->'),wn([[scc,V1,S1],[agent,J,[lcc1,C,Lcc1]]]),
    forall(
      (nth1(_K,Is,I),I\=J),
      (lcc([I,S1,_Rk],C,As))
    ).


% C_star has been excluded all higher order awkward outcomes. 
awk(W,[[J,S,R],A],Is,F):-
   alternative(A),
   state(S),
   agent(J),
   set_C_star(C,_K,[[J,S,R],A,_B],Is,F),
   lcc([J,S,R],A,L),
   (subset(C,L)->wn(ok);wn(ng)),
   subtract(L,C,W).

test_awk1(C,[[J,S,R],A],L):-
    is_awkward(C,[[J,S,R],A],B,[1,2],suh),
    \+numbervars(B,v,0,0),
    awk(W,[[J,S,R],A],[1,2],suh),
    \+member(C,W),
    lcc([J,S,R],A,L).
test_awk2(Cw1,Cw2,[[J,S,R],A],L,Bx,Cx,[DCk,Ck1,K1]):-
    awk(Cw1,[[J,S,R],A],[1,2],suh),
    findall(C,
      is_awkward(C,[[J,S,R],A],_,[1,2],suh),
    C2 ),
    sort(C2,Cw2),
    lcc([J,S,R],A,L),
    set_C_star(Cx,K,[[J,S,R],A,Bx],[1,2],suh),
    K1 is K -1,
    set_dCk(K1,DCk,_Ck,Ck1,[[J,S,R],A,Bx],[1,2],suh).

set_dCk(K,DCk,Ck,Ck1,[[J,S,R],A,Bstar],Is,F):-
    set_Ck([K|_],Ck-Ck1,[[J,S,R],A,Bstar],Is,F),
    subtract(Ck,Ck1,DCk).




% -----------------------------------------------------------  %
% Strong Implementation  
% -----------------------------------------------------------  %
% reference: Suh(1996).

/*
   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
   %%%% lower contour set for coalition of agents %%%%%
   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
   % 24 Aug 2002.
*/

lcc_c([T,S,Rs],A,Lcc) :-
   subset_of_agents(T,_),
   T \=[],
   state(S),
   prefer_profile(T,Rs),
   alternative(A),
   findall(L,
     (
      nth1(K,T,J),
      nth1(K,Rs,R),
      lcc([J,S,R],A,L)
     ),
   LX),
   all_members(LX,Lcc).


suh(S,J,[A,R]):-
    alternative(A),
    agent(J), state(S), preference(J,S,R).

suh_profile(Is,S,Prf):-
    subset_of_agents(Is,_N),
    state(S),
    my_maplist(suh(S),Is,Prf).

tau(Tau,[P,T,J],Is):-
   subset_of_agents(Is,_),
   state(S),
   suh_profile(Is,S,P),
   subset_of_agents(T,_),
   T \= Is,
   subset(T,Is),
   subtract(Is,T,Tc),
   member(J,Tc),
   nth1(KJ,Is,J),
   nth1(KJ,P,[A,R]),
   findall(I,
    (
     member(I,Tc),
     nth1(KI,Is,I),
     nth1(KI,P,[A,R])
    ),
   Tj),
   sort(Tj,Tau).



/*
  %%%%%%%%%%%%%%%%%%%%%%%%%%%%
  %%%   Condition  gamma  %%%%
  %%%%%%%%%%%%%%%%%%%%%%%%%%%%
  % postponed. 
*/





/*   the mechanisms part   */
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% A mechanism, (M,g), consists of a message space, M=M[1]x...xM[n],
% that is a Cartesian product of n individual message space, one for
% each agent, and an outcome function, g:M-->A. 
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% edited from: Sep 2001.

% mechanism(GameForm(rule,scc),Environments,MessageSpace,Outcomes).
% Environments=[Scc,Agents,States,Alternatives,PreferenceProfiles].
% MessageSpace=[M(I,1),...,M(I,#M(I))].
% The outcome of the mechanism is a subset of A for each M(k), a 
% message profile for each agent.


% -----------------------------------------------------------  %
%%%% the common main part for several mechanisms  %%%%%%%%%%%%%%
% unified: 17 Aug, 2002
% -----------------------------------------------------------  %
mechanisms([gM,gD,gMR,gMR2,gDict]).

% modified: 3 Dec 2002. change the order of setup in the top.
% modified: 5 Dec 2002. abolish setup in mechanism /4.
% modified: 8 Jan 2003. extended to generate outputs if unbounded input arguments and to neglect if the fact mechanism /3 exists.

mechanism(G,M,C):-
    \+ clause(mechanism(G,M,C),true),
    (var(G)->
     (wn('mechanism must be specified.'),
      hear(game_form,GF)
     );true
    ),
    G =.. [GF,_P,Scc],
    (var(Scc)->
     (wn('scc must be specified.'),
      hear(scc,Scc)
     );true
    ),
    !,
    E =.. [environment,[Is,_Ss,_As],_,_],
    E,
    mtest(GF, Scc,M,Is),
    mechanism(G,E,M,C).
    %lpom(set,M,[GF,Scc,Is],_Zs).

mechanism(G,E,Msg,Z):-
    %setup(G,Scc,E),
    E =.. [environment,[Is,_Ss,_As],[_N,_K,_L],_Rs],
    G =.. [GF,_P,Scc],
    mtest(GF, Scc,Msg,Is),%wn(main(Msg)),read(y),
    game_form(G,E,Msg,Z),!.

   % cut (!) above means that the message Msg can be enumerated
   % by preceeding mtest(gM, Msg,Is) to the parent goal mechanism().

setup(G,Scc,E):-
    scc(Scc),
    mechanisms(GFs),
    member(GF,GFs),
    game_forms(GF,Ps),
    member(P,Ps),
    G =.. [GF,P,Scc],
    subset_of_agents(Is,N),
    states(Ss),
    alternatives(As),
    E=environment([Is,Ss,As],[N,_K,_L],_Rs),
    E.

check_gD_outcomes(P,C,Scc,[M,M1],[Z,Z1],[B,B1]):-
   mechanism(gD(P,Scc),[(M,Z),(M1,Z1)],C),
   (is_blocked_by(M,1,[1,2],mr)->B=yes;B=no),
   (is_blocked_by(M1,2,[1,2],mr)->B1=yes;B1=no).

chk_gD_r2(C1,Scc,[M,M1],[Z,Z1],Jd):-
   check_gD_outcomes(gD,_P,C,Scc,[M,M1],[Z,Z1],Y),
   (member(Y,[[yes,yes],[no,no]])->fail;
    (
     (Y=[no,yes]->Jd=2;true),
     (Y=[yes,no]->Jd=1;true),wn([[(M,Z),(M1,Z1)],Y,C]),!,
     game_form(gD(2,Scc),_,[(M,Z),(M1,Z1)],C1)
    )
   ).


/*
   %%%%%%%%%%%%%%%%%%%%%%%%
   %% the message spaces %%
   %%%%%%%%%%%%%%%%%%%%%%%%
*/

% -----------------------------------------------------------  %
% message space for gDict, a simple dictatorial mechanism. 
% -----------------------------------------------------------  %
% gDict のメッセージ空間はAlt.
% any outcomes, not including [].
% added: 22 Sep 2002.
% modified: 2 Jan 2003. mtest /5

mtest(Z0,GF,Scc,Msg,Is):-
    var(Z0),
    mtest(GF,Scc,Msg,Is).

mtest(0,GF,Scc,Msg,Is):-
    mtest_z0(GF,Scc,Msg,Is).

mtest(gDict,Scc,Msg,[J1,J2]):-
    scc(Scc),
    range(Scc,B),
    two_person([J1,J2]),
    Msg = [X1,X2],
    alternative(X1),
    alternative(X2),
    subset([X1,X2],B).

mtest(gDict,Scc,Msg,Js):-
    scc(Scc),
    range(Scc,B),
    subset_of_agents(Js,N),N>2,
    bag0(Msg,B,N).


% -----------------------------------------------------------  %
% the message space for gD, the Danilov mechanism. 
% -----------------------------------------------------------  %
% gD のメッセージ空間はAltの部分集合
% any subset of outcomes, including [].

mtest(gD,Scc,Msg,[J1,J2]):-
    scc(Scc),
    two_person([J1,J2]),
    Msg = [(X1,Z1),(X2,Z2)],
    subset_of_alt(X1,_),   member(Z1,[0,1]),
    subset_of_alt(X2,_),  member(Z2,[0,1]).


% -----------------------------------------------------------  %
% message space for gM, gMR, gMR2
% -----------------------------------------------------------  %
% edited from: Sep 2001.
% modified by using maplist: 24 Aug 2002.
% modified: 29 Dec 2002. abolish maplist and unified for the three mechanisms.

mtest(GF, Scc,Msg,Is):-
    member(GF,[gM,gMR,gMR2]),
    subset_of_agents(Is,_),
    messages(GF, Scc,Msg,Is,Is).


% -----------------------------------------------------------  %
% message profiles in gM, gMR, gMR2.
% -----------------------------------------------------------  %
% modified: 24 Aug 2002. it is useless now.
% modified: 29 Dec 2002. to include gMR, gMR2.

% message profile for N agents in mechanism gM.
messages(GF, Scc,[],[],Is):-
    member(GF,[gM,gMR,gMR2]),
    scc(Scc),
    subset_of_agents(Is,_N),!.

messages(GF, Scc, [M|Msg],[I|Is],Agents):-
    member(GF,[gM,gMR,gMR2]),
    messages(GF, Scc,Msg,Is,Agents),
    agent(I), \+member(I,Is),
    G=..[GF,_,Scc],
    message(G,Agents,I,M,true).

% modified: 10 Nov 2002.
% modified: 29 Dec 2002.

message(gM(_,F),Is,I,M,C):- maskin_msg(gM(_,F),Is,I,M,C).
message(gMR(_,F),Is,I,M,_):- mr_msg(Is,F,I,M).
message(gMR2(_,F),Is,I,M,_):- mr2_msg(Is,F,I,M).

maskin_msg(gM(_,F),Is,I,(Rs,A,Z),Consistency):-
   environment([Is,_Ss,_As],[N,_K,_L],_Rks),
   subset_of_agents(Is,N),
   member(I,Is),
   scc(F),
    (
      Consistency = true
     -> (
         state(S),
         prefer_profile(Is,S,Rs)
	 % bug fixed. 10 Nov 2002.
         %scc(F,S,V),member(A,V)
        )
     ;  prefer_profile(Is,Rs)
    ),
   alternative(A),
   asc_nnseq(Aseq,N),member(Z,Aseq).

mr_msg(Is,F,J,M):-
    M=(R,A,B,Z),
    subset_of_agents(Is,N),
    member(J,Is),
    scc_defined_state(S,F),
   %  <-- if you restrict agent-set, shoudn't use "state(S)" instead.
    prefer_profile(Is,S,R),
    scc(F,S,V),
    alternative(A),member(A,V),
    alternative(B),
    asc_nnseq(Aq,N),member(Z,Aq).

mr2_msg([J1,J2],F,J,M2):-
    mr_msg([J1,J2],F,J,M),
    M=(R,A,B,Z),
    M2=(R,A,B,Z,Obj),
    member(Obj,[0,1]).


messages0(G,Is,I,Ms,(Con,Show)):-
   subset_of_agents(Is,_N),
   member(I,Is),
   member(Con,[true,_]), 
   member(Show,[yes,_]), 
   findall(M,message(G,_,I,M,Con),Ms),
   (Show = yes -> writeMessages(Ms,I);true).

writeMessages(Ms,I):-
    length(Ms,L),
    tab(10),write('There are '),
    write(L),write(' strategies for agent '),
    write(I),write('.'), nl,
    prompt(_,' Display those variables? (y/n) '),
    read(Y), (Y == 'y' -> true; fail).



% -----------------------------------------------------------  %
% message profiles which has fixed all-0-integer game 
% -----------------------------------------------------------  %
% modified: 27 Nov 2002. 
% modified: 4 Dec 2002. 
% debug mtest_z0 of gMR and gMR2, as for its wrong argument of 0.

mtest_z0(GF, Scc,Msg,Is):-
    mtest(GF,Scc,Msg,Is),
    mtest_z0(GF, Scc,Msg,Is,Is).
mtest_z0(GF,Scc,[],[],Is):-
    mechanisms(Mxs),
    member(GF,Mxs),
    scc(Scc),
    subset_of_agents(Is,_N),!.
mtest_z0(GF, Scc,[M|Msg],[I|Is],Agents):-
    (member(GF,[gM]) -> M = (_,_,0); true),
    (member(GF,[gMR]) -> M = (_,_,_,0); true),
    (member(GF,[gMR2]) -> M = (_,_,_,0,_); true),
    (member(GF,[gD]) -> M = (_,0); true),
    mtest_z0(GF, Scc, Msg,Is,Agents),
    agent(I), \+member(I,Is).

%mtest_z0(gD,F,Msg,Is):-Msg = [(_X1,0),(_X2,0)],mtest(gD,F, Msg,Is).



% -----------------------------------------------------------  %
% setting the integer elements for profile
% -----------------------------------------------------------  %
% a utility for extracting integer elements from message profile
% modified: 6 Sep 2002.
% modified: 12 Nov 2002.  

lpom(O,Msg,[GF,Scc,Is],Zs):-
    last_part_of_mtest(O,Msg,[GF,Scc,Is],Is,Zs).

lpom(O,Msg,[GF,Scc,Is],I,Zk):-
    last_part_of_mtest(O,Msg,[GF,Scc,Is],I,Zk).

% abolished: 15 Oct 2002
%last_part_of_mtest(Msg,[GF,Scc,Is],Is,Zs):-
%    maplist(last_part_of_mtest(Msg,[GF,Scc,Is]),Is,Zs).

% edited: 6 Sep 2002
last_part_of_mtest(_,_,_,[],[]).
last_part_of_mtest(O,Msg,[GF,Scc,Is],[J|Js],[Z|Zs]):-
    last_part_of_mtest(O,Msg,[GF,Scc,Is],J,Z),
    last_part_of_mtest(O,Msg,[GF,Scc,Is],Js,Zs).

% edited: 15 Oct 2002. 4 Dec 2002.
% modified: 5 Jan 03.
last_part_of_mtest(O,Msg,[GF,_Scc,Is],I,Zk):-
    %mtest(GF,Scc,Msg,Is),
    subset_of_agents(Is,N),
    (O=set->(asc_nnseq(Aseqn,N),member(Zk,Aseqn));true),
    nth1(K,Is,I),%wn([K,I]),
    member([GF,M],
	[[gM,(_R,_X,Zk)],
	 [gD,(_X,Zk)],
	 [gMR,(_R,_X,_Y,Zk)],
	 [gMR2,(_R,_X,_Y,Zk,_)]]
    ),
    nth1(K,Msg,M).

% moved from best_response. (29 Dec) 
mutate_lpom_set(Isz,Msg,Mz,[GF,Scc,Is]):-
   lpom(set,Msg,[GF,Scc,Is],Z1),
   lpom(set,Mz,[GF,Scc,Is],Z2),
   forall(member(K,Isz),
    (
     nth1(Nk,Is,K),
     nth1(Nk,Z1,Zk),
     nth1(Nk,Z2,Zk)
    )
   ).
% added: 29 Dec.
lpomeq(GF,P,_Scc,_Is,Msg,Mz):-
    (
     member(GF, [gMR,gMR2]),
     P = 1
    )
    ->
    (
     lpom(set,Msg,[GF,Scc,Is],Z),
     lpom(set,Mz,[GF,Scc,Is],Z)
    ).


% -----------------------------------------------------------  %
% truth-telling strategy
% -----------------------------------------------------------  %
% modified: 30 Dec 2002, 2 Jan 2003.
% modified: 7 Jan 2003. a bug fix.
check_truth_telling(_M,gDict,_Scc,_Is, _S,_M).
check_truth_telling(truthful,GF,Scc,Is, S,Msg):-
      member(GF,[gM,gMR,gMR2]),
      subset_of_agents(Is,N),
      length(Msg,N),
      state(S), 
      prefer_profile(Is,S,R),
      scc(Scc,S,V),
     %member(A,V),
     %alternative(A),
      forall(member(X,Msg),A^(X=(R,A,_),member(A,V))),
      write('--> truth telling.').
check_truth_telling(truthful,gD,Scc,Is,_S,[(X1,0),(X2,0)]):-
    subset_of_agents(Is,2),
    unblocked_pair([X1,X2],Is,Scc).
check_truth_telling(M,GF,_,_,_,_):-
      member(GF,[gM,gMR,gMR2,gD]),
      sim_mode(M),
      M \= truthful.
ctt(M,GF,Scc,Is, S,Msg):-
      check_truth_telling(M,GF,Scc,Is, S,Msg).


% modified: 24 Aug 2002. 4 Sep 2002.
ttm(gM,Scc,Msg,Is,S):-
    scc(Scc),
    subset_of_agents(Is,N),
    state(S),
    tt_gM_profile(Scc,Is,S,Msg),
    length(Msg,N).

% the following is questionable.
ttm(gD,Scc,Msg,[J1,J2],S):-
    scc(Scc),
    state(S),
    two_person([J1,J2]),
    Msg = [(X1,Z1),(X2,Z2)],
    subset_of_alt(X1,_), X1\=[],   member(Z1,[0,1]),
    subset_of_alt(X2,_), X2\=[],   member(Z2,[0,1]),
    \+is_blocked_by(X2,J1,[J1,J2],Scc),
    \+is_blocked_by(X1,J2,[J1,J2],Scc),!.



%%% a sole testing for the mechanism gM, N>=3.

test_gM(Scc,P,M,C,Is):-
    E = environment([Is,_Ss,_As],[N,_K,_L],_Rs),
    subset_of_agents(Is,N),
    E,
    mtest(gM,Scc, M,Is),
    mechanism(gM(P,Scc),E,M,[C]).


%%% sole testings for the mechanism gD, N=2.

test_gD(Scc,Is,[P,C,M]):-
    E = environment([Is,_Ss,_As],[2,_K,_L],_Rs),
    E,
    mtest(gD, Scc,M,Is),
    mechanism(gD(P,Scc),E,M,[C]).

test_gD(F,[I,J],[P,Out,C,[M1,M2],[Block1,Block2],[Ess1,Ess2]],MR):-
    E = environment([[I,J],_Ss,_As],[2,_K,_L],_Rs),
    E,
    M = [M1,M2],
    M = [(X1,_Z1),(X2,_Z2)],
    mtest(gD, F,M,[I,J]),
    (is_blocked_by(X2,1,[I,J],F)->Block1=block;Block1=unblock),
    (is_blocked_by(X1,2,[I,J],F)->Block2=block;Block2=unblock),
    ess(F,1,X1,Ess1),ess(F,2,X2,Ess2),
    is_MR_elements(MR,[X2,X1],[I,J],F),
 %   wn([block_1_2,Block1,Block2,m,M]),
    (mechanism(gD(P,F),E,M,[C])->Out=gD_ok;Out=not_found).


%%% sole testings for the mechanism gMR.

test_gMR(Scc,Is,[P,C,M]):-
    E = environment([Is,_Ss,_As],[_N,_K,_L],_Rs),
    E,
    mtest(gMR, Scc,M,Is),
    mechanism(gMR(P,Scc),E,M,[C]).

test_gMR2(Scc,Is,[P,C,M]):-
    E = environment([Is,_Ss,_As],[2,_K,_L],_Rs),
    E,
    mtest(gMR2, Scc,M,Is),wn([new_message,M]),
    mechanism(gMR2(P,Scc),E,M,[C]).


/*
   %%%%%%%%%%%%%%%%%%%%%%%%
   %%  the  game  forms  %%
   %%%%%%%%%%%%%%%%%%%%%%%%
*/

/*  available game forms in this system */

game_forms(gDict,[_D]).
game_forms(gM,[1,2,3]).
game_forms(gD,[1,2,3]).
game_forms(gMR,[1,2,3]).
game_forms(gMR2,[1,2,3,4,5,6]).

/*  unused
game_forms(GF,Ps):-
    mechanisms(GFs),
    member(GF,GFs),
    setof(P,
      M^(
       G=..[GF,P,_Scc]
       clause(game_form(G,_,M,_),_),
      ),
    Ps).
*/


% -----------------------------------------------------------  %
%%%%%  dictatorship   (almost same as maximal )
% -----------------------------------------------------------  %
% edited : 29 Aug 2002. to be used in roullete in gD and so on.
% modified: 7 Sep 2002. 
% gD has a bug in the new version of this system with pre-verified messages.   

dictatorship(J,S,X,D):-
  % J: dictator
  % S: state
  % X: range of choice
  % D: choiced outcome
   agent(J),
   subset_of_alt(X,_),
   true_state(T),
   %  <-- of course, you shoudn't use "scc_defined_state(S,Scc)" instead.
   (state(T)-> S=T; 
     state(S),
     %wn(['warnig: state',S, 'is not the updated state.']),
     true
   ),
   maximal(D,X,[J,S,_RJ]).
   % dictatorship to be computed over all possible preferences of the dictator,
   % from the view point of mechanism designer, isn't it?

% an elementary computation version
dictatorship_0(J,S,X,C):-
    agent(J),
    subset_of_alt(X,_),
    member(C,X),
    preference(J,S,_W),
    subset_of_alt(X,_),
    \+ (member(Other,X),
        is_prefer_to(J,S,Other,C),
        \+is_prefer_to(J,S,C,Other)
       ).


% true stateは引数渡ししない。DB内の節としてユニファイする。


% -----------------------------------------------------------  %
% the roulette of modulo N
% -----------------------------------------------------------  %
% added: Aug 2002.
% modified: 6 Sep 2002.


% for 2-person
% modified: 4 Sep 2002. dictatorship has separated from roulette.
roulette(Dictator,[Z1,Z2],[J1,J2]):-
    subset_of_agents([J1,J2],2),
    member(Z1,[0,1]),
    member(Z2,[0,1]),
    SumZ is Z1 +  Z2,
    K is SumZ mod 2 + 1,
    nth1(K,[J1,J2],Dictator).%wn(Dictator),read(Y),
   %wn([roulette,dict,Dictator]).


% for n-person
roulette(Dictator,Zs,Is):-
    subset_of_agents(Is,N),
    N >2,
    subset_of_agents(Is,N),
    asc_nnseq(Aseqn,N),
    bag0(Zs,Aseqn,N),
    sum(Zs,SumZ),%wn(SumZ),
    K is SumZ mod N + 1,%wn(K),
    nth1(K,Is,Dictator).


% -----------------------------------------------------------  %
% gDict, a very simple dictatorial mechanism. 
% -----------------------------------------------------------  %
% added: 22 Sep 2002.

% the game form of gDict %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
game_form(gDict(Dict,_Scc),E,Msg,[C]):-
    E = environment([Is,_Ss,_As],[N,_K,_L],_Rs),
    length(Msg,N),
    nth1(K,Is,Dict),
    nth1(K,Msg,C).


%%%%%%%%%%%%%%%%% the game forms. for N (>)= 3 cases  %%%%%%%%%%%%



% -----------------------------------------------------------  %
% The canonical Mechanism for 3 or N agents. 
% (Maskin-Vind mechanism, modified by using Ess):
% -----------------------------------------------------------  %
% reference: Maskin(1999,1985), Danilov(1992), Yamato(1992), Saijo(1988).
% the earlier version only for 3 players has created 29-30 Sep 2001.  
% gD, Danilov's two-person mechanism added 23 Jan 2002.

% modified: Feb 2002,May 2002, and by using ess, Aug 2002.
% modified: 3 Sep 2002. Abolish the pattern match of the exceptional rule 3.
% modified: 10 Nov 2002. To use lcc instead of ess if empty.
% modified: 26 Nov 2002. Undo above irrelevant modification.
% modified: 10 Dec 2002. Correct the check for in-scc on agreed outcome and the position of cut in P=1,2. This error might have occurred during above modifications.
% modified: 29 Dec 2002.  A bug in the third gameform that allows multiple application for the same message profile has fixed.

%%%%%%%%%%%%%%%%% the game forms. for N (>)= 3 cases  %%%%%%%%%%%%
% The outcome function of the Maskin mechanism.
% The Maskin-Vind mechanism ( cannonical mechanism)
%   g((pi、ci、mi)i∈N)=ck、
%   ただし、piは選好プロフィールで、
%   kの選出は以下のルール1〜3に従う。

% -----------------------------------------------------------  %
%%%% the rule 1 of the Maskin-Vind mechanism gM. %%%%%%%%%%%%
% -----------------------------------------------------------  %
% ルール1:
%   整数miの部分を除き全員一致、
%   (pi、ci)=(p、c)、
%   かつcがf(≧、p)に含まれている  ==> k=1。

game_form(gM(1,Scc),E,Msg,[C]):-%wn(rule1),
    E = environment([Is,_Ss,_As],[N,_K,_L],_Rs),
    length(Msg,N),
  %  Msg = [(R,C,_Z1),(R,C,_Z2),(R,C,_Z3)],
  % extended for N >= 3
    setof((Rx,X,0),Z^member((Rx,X,Z),Msg),[(R,C,0)]),
  % wn([m,Msg]),
    state(S),
    prefer_profile(Is,S,R),
    scc(Scc,S,Obj),
    alternative(C),
    member(C,Obj),
    !.




% -----------------------------------------------------------  %
%%%% the rule 2 of gM.  %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% -----------------------------------------------------------  %
% ルール2:
%   個人jを除いてルール1の全員一致が成り立つ 
%      (もちろんc∈f(≧、p)の部分も!)==>
%   N−{j}が一致して表明したpにおける個人jの好みp[j]、
%   およびj自身が表明した選択対象cjとすると、
%   c(≧、p[j])cj のとき、k=j; それ以外は任意のk≠j。


% modified: 27 Nov 2002. bug fix.
% modified: 4 Dec 2002. a simplified version and bug fix so that C2 in scc.
% modified: 10 Dec 2002. a bug fix. an irrelevant scc-range constraint. And an alternative pattern match by bagof and subtract.
% modified: 6,8 Jan 2003. to modify the above pattern match. 

game_form(gM(2,Scc),E,Msg,[C]):-%wn(rule2),
      E = environment([Is,_Ss,_As],[N,_,_],_Rs),
      length(Msg,N),
/*
  % extended for N >= 3. if N=3,
    (Msg = [(R1,C1,Z1),(R2,C2,Z2),(R2,C2,Z3)] -> (K is 1,true);
    Msg = [(R2,C2,Z1),(R1,C1,Z2),(R2,C2,Z3)] -> (K is 2,true);
    Msg = [(R2,C2,Z1),(R2,C2,Z2),(R1,C1,Z3)] -> (K is 3,true)),
    nth1(K,Is,J),
*/
  % the agreed preference, R2J, except for, J, the deviancy who has a unique 
  % and distinctive opinion.
  %wn((rule,2,[J,K],Msg)),read(y),
      nth1(K,Is,J),
      nth1(K,Msg,MJ),
      MJ = (R1,C1,_Z1),
     % the necessary condition of a unilateral deviator.
      bagof((R0,X),Z^(member((R0,X,Z),Msg)),MD),
      counter(1,(R1,C1),MD),
      subtract(Msg,[MJ],Msg1),
      setof((R,X),Z^(member((R,X,Z),Msg1)),[(R2,C2)]),
     % check in_scc for the agreed outcome.
     %state(S),
      prefer_profile(Is,S,R2),
      scc(Scc,S,Obj),
      alternative(C2),
      member(C2,Obj),
      !,
      nth1(K,R2,R2J),
      preference(J,S,R2J),
      lcc([J,S,R2J],C2,Lcc),
      ess(Scc,J,Lcc,Ess),
      (member(C1,Ess)-> C = C1; C = C2).
      %range(Scc,Range),member(C,Range).

% -----------------------------------------------------------  %
%%%% the rule 3 of gM.   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% -----------------------------------------------------------  %
% ルール3: 上の2ルールいずれにも該当しない ==> 
%   miの総和のnの剰余k=mod(Σmi、n)+1。
% modified: 26 Nov 2002. a bug which occurred 9-12 Nov fixed.
% modified: 29 Dec 2002. to prohibit non-exclusive application.
% modified: 2,4 Jan 2003. a bug fix. to re-activte roulette by using lpom.


game_form(gM(3,Scc),E,Msg,[C]):-%wn(rule3),
    E = environment([Is,_Ss,_As],[N,_K,_L],_Rs),
    length(Msg,N),
    \+ game_form(gM(1,Scc),E,Msg,_),
    \+ game_form(gM(2,Scc),E,Msg,_),
   %setof((R,X,0),Z^member((R,X,Z),Msg),Mx),%wn([m,Mx]),read(y),
   %length(Mx,Lm), Lm > 2, %wn(rule(3,Msg)),
    lpom(refer,Msg,[gM,Scc,Is],Zs),
   %Msg = [(_,_C1,Z1),(_,_C2,Z2),(_,_C3,Z3)],
   %SumZ is (Z1 + Z2 + Z3),
   %K is SumZ mod 3 + 1,
   %Zs=[Z1,Z2,Z3],
    length(Zs,N),
    roulette(Jd,Zs,Is), %wn(stop(Jd,Msg)),   
    nth1(K,Is,Jd),
    nth1(K,Msg,(_R,C,_Z)),
    !.


%%%% end of rules.


/*
    % 2エージェントの場合
    %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
    %% the Mechanism part for two-person cases:  %%
    %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
    % edited 23-24 Jan 2002; 1-5 May 2002. Aug 2002.
*/

% -----------------------------------------------------------  %
% Danilov's mechanism μ(F), which assumes unristricted domain.
% -----------------------------------------------------------  %


% the game forms of gD %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% -----------------------------------------------------------  %
%%%% the case 1 of the Danilov mechanism gD. %%%%%%%%%%%%%%
% -----------------------------------------------------------  %
% Case 1: 1がX2をブロックせず、2がX1をブロックしないとき
% ルーレット(modullo game)によってMR(F;X2,X1)≠[]から結果を選ぶ。
% modified: 4 Sep 2002. dictatorship has separated from roulette.
% modified: 7 Sep 2002. 

game_form(gD(1,Scc),E,Msg,[C]):-%wn([r1]),
    E = environment([[J1,J2],_Ss,_As],[2,_K,_L],_Rs),
    two_person([J1,J2]),
    mtest(gD, Scc,Msg,[J1,J2]),
    Msg=[(X1,Z1),(X2,Z2)],
    \+is_blocked_by(X2,J1,[J1,J2],Scc),
    \+is_blocked_by(X1,J2,[J1,J2],Scc),!,
    %intersection(X1,X2,Y1),
    /*  caution: the MR set is of the pair [X2,X1]. */
    is_MR_elements(Y,[X2,X1],[J1,J2],Scc),%wn([mr,Y]),
    roulette(Jd,[Z1,Z2],[J1,J2]),%wn([dict,Jd]),
    member(C,Y),%wn([member,C]),
    dictatorship(Jd,_S,Y,C).

% -----------------------------------------------------------  %
%%%% the case 2 of gD. %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% -----------------------------------------------------------  %
% Case 2: iがXjをブロックし、jがXiをブロックしないとき
%   Ess(F;i,Xi)≠[]に含まれる結果についてjの独裁を認める。

game_form(gD(2,Scc),E,Msg,[C]):-%write([r2]),
    E = environment([[J1,J2],_Ss,_As],[2,_K,_L],_Rs),
    %E,
    two_person([J1,J2]),
    mtest(gD, Scc,Msg,[J1,J2]),
    Msg=[(X1,_),(X2,_)],%wn([X1,X2,[J1,J2]]),
    (
     (
      is_blocked_by(X2,J1,[J1,J2],Scc),
      \+is_blocked_by(X1,J2,[J1,J2],Scc),
      X0=X1, J0=J2
     );
     (
      \+is_blocked_by(X2,J1,[J1,J2],Scc),
      is_blocked_by(X1,J2,[J1,J2],Scc),
      X0=X2, J0=J1
     )
    ),!,
    ess(Scc,J0,X0,Ess0),%wn([J0,X0,Ess0]),
    member(C,Ess0),
    dictatorship(J0,_S,Ess0,C).
%, wn([dict,J0,scc,Scc,X0,ess,Ess0,[S,C]]).


% -----------------------------------------------------------  %
%%%% the case 3 of gD.  %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% -----------------------------------------------------------  %
% Case 3: 1がX2をブロックし、2がX1をブロックするとき
%   ルーレット(modullo game)によってIM(F)から結果を選ぶ。
%
% modified: 4 Sep 2002. dictatorship has separated from roulette.

game_form(gD(3,Scc),E,Msg,[C]):-%wn([r3]),
    E = environment([[J1,J2],_Ss,_As],[2,_K,_L],_Rs),
    two_person([J1,J2]),
    mtest(gD, Scc,Msg,[J1,J2]),
    Msg=[(X1,Z1),(X2,Z2)],
    is_blocked_by(X2,J1,[J1,J2],Scc),
    is_blocked_by(X1,J2,[J1,J2],Scc),
    !,
     %wn(Msg),read(Y),
    range(Scc,Range),
    roulette(Jd,[Z1,Z2],[J1,J2]),
    member(C,Range),
    dictatorship(Jd,_S,Range,C).


%%%% end of rules.

/*
    %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
    %% the Mechanism for 2 (or more) person cases  %%
    %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
    % edited 9, 26 Aug 2002.modified: 2 Sep 2002.
*/

% -----------------------------------------------------------  %
% the mechanisms of Moore-Repullo, Dutta-Sen: 
% Augmented by Sjostrom's algorithm
% -----------------------------------------------------------  %
% reference: see the proof of Moore-Repullo(1990), in the appendix. 
% The message of i-th agent is (Rs[j],A[j],B[j],Z[j]) as noted previously.
% See also Yamato(1992) as for the cases N>=3.
% Dutta-Sen(1991) is almost same but only for N=2.  Whereas they 
% did not use  B[j]s, instead did use "the objection flag", noted in 
% their footnote 3, the former enlarged element is need to device 
% more precise construction for the message space.


%    the game forms for the mechanism gMR,gMR2   %


% -----------------------------------------------------------  %
%%%% the case 1 of the Moore-Repullo mechanism gMR for N>=3. %%%
% -----------------------------------------------------------  %

game_form(gMR(1,_Scc),E,Msg,[C]):-
      E = environment([_Is,_Ss,_As],[N,_K,_L],_Rs),
      length(Msg,N),N>2,
      setof((R,X),Y^Z^member((R,X,Y,Z),Msg),[(_,C)]),!.


% -----------------------------------------------------------  %
%%%% the case 2 of gMR  for N>=3.          %%%%%%%%%%%%%%
% -----------------------------------------------------------  %
% the case (2) in the MR's proof for N-person, N>=3. 
% modified: 6,8 Jan 2003.

game_form(gMR(2,Scc),E,Msg,[C]):-
      E = environment([Is,_Ss,_As],[N,_K,_L],_Rs),
      length(Msg,N),N>2,
      nth1(K,Is,J),
      nth1(K,Msg,MJ),
      MJ = (R1,A1,B1,_O1),  % disagreed message.
     % the necessary condition of a unilateral deviator
     % and the semi-agreed component.
      bagof((R0,X),Y^Z^(member((R0,X,Y,Z),Msg)),MD),
      counter(1,(R1,A1),MD),
      subtract(Msg,[MJ],Msg1),
      setof((R2,X),Y^Z^(member((R2,X,Y,Z),Msg1)),[(R,A)]),
     % check in_scc for the agreed outcome.
      nth1(K,R,RJ),
      nth1(K,Is,J),   % the deviator has specified.
      preference(J,S,RJ),  % estimated state from agreed profile.
      prefer_profile(Is,S,R),
      scc(Scc,S,Obj),
      member(A,Obj),
      !,
      set_C_star(Cx1,_,[[J,S,RJ],A,_Bx],Is,Scc),
      (member(B1,Cx1)-> C = B1; C = A).


% -----------------------------------------------------------  %
%%%% the case 3 of gMR   for N >= 3.       %%%%%%%%%%%%%%%%%%%%%
% -----------------------------------------------------------  %
% the case (3) in the MR's proof for N-person, N>=3. 
% modified: 30 Dec 2002, 2,4,7 Jan 2003.

game_form(gMR(3,Scc),E,Msg,[C]):-
    E = environment([Is,_Ss,_As],[N,_K,_L],_Rs),
    length(Msg,N),
    \+ game_form(gMR(1,Scc),E,Msg,_),
    \+ game_form(gMR(2,Scc),E,Msg,_),
   %setof((R,X),Y^Z^member((R,X,Y,Z),Msg),Mx),%wn([m,Mx]),
   %length(Mx,Lm),  Lm > 2, 
    length(Zs,N),
   %lpom(refer,Msg,[gMR,Scc,Is],Zs),
    roulette(Jd,Zs,Is),    
    nth1(K,Is,Jd),
    nth1(K,Msg,(_R,_A,C,_Z)),
    !.



%%%% end of rules.



% -----------------------------------------------------------  %
%%%% the case 1 of the Moore-Repullo mechanism gMR2 for N=2. %%%
% -----------------------------------------------------------  %
% edited 9, 26 Aug 2002.


game_form(gMR2(1,_Scc),E,Msg,[C]):-
      E = environment([_Is,_Ss,_As],[2,_K,_L],_Rs),
      Msg = [(R,C,_,_,_),(R,C,_,_,_)],!.

% -----------------------------------------------------------  %
%%%% the cases 2 ... 6 of gMR2 for N=2.   %%%%%%%%%%%%%%
% -----------------------------------------------------------  %
% modified: 3 Sep 2002.

% the cases (2),(3), ...,(6) in the MR's proof for 2-person. 
% --------
% Z, the integer part of Moore-Repullo's message is able to interpreted as 
% is decomposed into Bz * Zr, where Bz is 0 or 1,
% and we regard each nonzero Bz as an appealing objection by that agent.
% Zr is an integer that will be used if the integer game has invoked.


game_form(gMR2(P,Scc),E,Msg,[C]):-
      E = environment([[J1,J2],_Ss,_As],[2,_K,_L],_Rs),
      Msg=[MJ1,MJ2],
      MJ1 = (R1,A1, B1,Z1,O1),
      MJ2 = (R2,A2, B2,Z2,O2), 
      [R1,A1] \= [R2,A2],
     % ------------------------ %
      member(P,[2,3,4,5,6]),
     % ------------------------ %
      ((O1=0,O2=0) -> P=2  ;true),
      ((O1>0,O2=0) -> P=3  ;true),
      ((O1=0,O2>0) -> P=4  ;true),
      member(Z1,[0,1]),member(Z2,[0,1]),
       Sum is Z1 + Z2,
       Mod is Sum mod 2,% wn([[Z1,Z2],Sum,Mod]), 
      ((O1>0,O2>0,Mod = 0) -> P=5; true),
      ((O1>0,O2>0,Mod = 1) -> P=6; true),!,
     % ------------------------ %
  % note(1): If you handle P5, as follows, as the case 2, [s2,c] is in scc mr.
     % ((O1=1,O2=1) -> P=2  ;true),!,
  % note(2): the original Moore-Repullo construction uses shouting game.
     % ((O1>=O2,O2>0) -> P=5 ; true), 
     % ((O1>0,O2>O1) ->  P=6 ; true),% <-originally shouting, but intractable.
     %tab(1),wn(['gMR2',P,'AB:',[A1,A2]]),
      alternative(C),
      R1 = [_R11,R12], prefer_profile([J1,J2],S1,R1),
      R2 = [R21,_R22], prefer_profile([J1,J2],S2,R2),
      (
       %notice that the each pair of A,S,R has transposed between agents.
       mre(MR,Scc,[[A2,A1],[J1,J2],[S2,S1],[R21,R12]],[Cx1,Cx2],no)
      ->true;MR=non
      ),
     %tab(1),wn([gMR2,P,mre,MR,[S1,S2],cxs,[Cx1,Cx2]]),
      ((P=2) -> C = MR ;true),
      ((P=3) -> (member(B1,Cx1)-> C = B1; C=MR);true),
      ((P=4) -> (member(B2,Cx2)-> C = B2; C=MR);true),
      ((P=5) -> C = B1 ; true),
      ((P=6) -> C = B2 ; true).
     % wn([gMR2,P,end]).



%%%% end of gMR2 rules.


/*
% consistency check for any game form.
game_form(_,E,Msg,[non]):-
      E = environment([Is,_,_],[N,_,_],_),
      wn('inconsistentency_in_process.'),
      length(Is,N1),
      length(Msg,N2),
      (sort([N,N1,N2],[N])->true;
      wn(this_message_is_inconsistent_and_cannot_processed)),!.
*/


%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%  Nash equilibrium for N players 
%  using the mechanism gM, gMR (N>=3) or gD, gMR2 (N=2):
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% edited from: Sep--Oct 2001.


% -----------------------------------------------------------  %
%%% checking best response via Lcc. 
% -----------------------------------------------------------  %
% modified: 31 Aug 2002.
% modified: 4 Dec 2002.
% modified: 29 Dec 2002.
% modified: 2-7 Jan 2003.

best_response:-
    wn('best_response([Scc,E,Is],[GF,S,C,Msg],I,[Pzs,Czs,Lcc],Br)').

best_response([Scc,E,Is],[GF,S,C,Msg],I,[Pzs,Czs,Lcc],Br):-
    E = environment([Is,_Ss,_As],[N,_K,_L],_Rs),
    E,
    scc(Scc),
   %  <-- of course, you shoud'nt use "scc_defined_state(S,Scc)" instead.
    agent(I), subset_of_agents(Is,N),
    member(I,Is),
    alternative(C),
   %game_forms(GF,Ps),
    mtest(GF, Scc,Msg,Is),
    write([I]),
  % the mutation set is included in the lower contuor set 
  % and so any unilateral deviation can not improve the Nash outcome.
    findall((P1,Cz),
         (
	  mutate(GF,Scc,I,Is,Msg,Mz),
	  % modified: 3 Dec 2002, 7 Jan 2002. 
          % If you use the following two, it brings about multiplicity of 
          % rules appied, which is caused by backtracks in mechanism /3.
	  % alternative(Cz),
	  % member(P1,Ps), 
	  G =.. [GF,P1,Scc],
	  mechanism(G,Mz,[Cz])
         ),
       PCzs1),
    sort(PCzs1,PCzs),
    findall(P1,Cz^(member((P1,Cz),PCzs)),Pzs1),
    sort(Pzs1,Pzs),
    findall(Cz,P1^(member((P1,Cz),PCzs)),Czs1),
    sort(Czs1,Czs),
    lcc([I,S,_],C,Lcc),
    (subset(Czs,Lcc)-> Br = yes; Br = no).


% -----------------------------------------------------------  %
% mutated profile when unilateral deviation has occured
% -----------------------------------------------------------  %
% modified: 03 Sep 2002.
% modified: 10 Dec 2002.

mutate(GF,Scc,J,Is,Msg,Mz):-
   subset_of_agents(Is,N),
   length(Is,N),
   nth1(Nj,Is,J),
   subtract(Is,[J],Isz),
   mtest(GF, Scc,Msg,Is),length(Msg,N),
   mtest(GF, Scc,Mz,Is),length(Mz,N),
   nth1(Nj,Msg,MJ),
   nth1(Nj,Mz,MJz),
   MJz \= MJ,
   forall(member(K,Isz),
    (
     nth1(Nk,Is,K),
     nth1(Nk,Msg,Mk),
     nth1(Nk,Mz,Mk)
    )
   ).
   % We might have to permit null-mutation case 
   % for the cases of roulette. 
   % But it is not the case  if we gave up to use 
   % lpom in order for delayed resolution. (29 Dec)


% mutate mechanism outcome via strategy profile of a unilateral deviator J.

mutate_mechanism(GF,Scc,J,Is,[P,P1],[C,C1],[M,M1]):-
   G=..[GF,P,Scc],
   %game_forms(GF,Ps),
   alternative(C),
   mechanism(G,M,[C]),
   member(J,Is),
   mutate(GF,Scc,J,Is,M,M1),
   G1=..[GF,P1,Scc],
   alternative(C1),
   mechanism(G1,M1,[C1]);
   (mechanism(G1,M1,non),C1=n).


% -----------------------------------------------------------  %
%%% nash equilibrium (best response check via Lcc for all agents). 
% -----------------------------------------------------------  %
% modified: 31 Aug 2002.
%  The best response for the agent is an action that his/her 
% lower contour set (LCC) includes the possible outcomes (Czs)
% by means of his/her own action against the fixed profile of actions 
% of others.
%  cf.,
%  Action profile m is an h-Nash equilibrium of a mechanism (M,g) 
%  at s if H(g(m),s,h)R[i](s)H(g(m^[i],m-[i]),s,h) for all i, m^[i] in M[i].

% modified: 6,20 Sep 2002.
% modified: 10 Nov 2002.
% modified: 4, 30 Dec 2002.
% modified: 2 Jan 2003.  the arity Mode and so nash /9 has abolished.
% modified: 8 Jan 2003.  to succeed even if mechanism not specified.

nash(C,S,Msg,G,H,E,Is,Result):-
    E = environment([Is,_,_],[_N,_,_],_),
    E,
    reversions(V),    member(H,V),
    state(S),
 %  update_state(S),   % update_state should be done before mechanism.
    alternative(C),    % alternative should be done before mtest.
    mechanism(G,Msg,[C]),
    G =.. [GF,P,Scc],
    scc(Scc),
    % !,
    nl,
    write_message(S,C,P,Msg,Scc),
    write(' .. checking the message profile, '),
    check_br_of_profile(Is,E,[GF,Scc,S,C,P,Msg]),
    collect_br_members([S,C,GF,Scc,Is,Msg],BrMembers0),
    sort(BrMembers0,BrMembers),
    display_br_results([S,C,GF,Scc,Is,Msg],BrMembers),
    write_nash_equilibrium(BrMembers,Is),
    ( BrMembers = Is -> Result=yes ; Result=no).


nash:-
    wn('nash(C,S,Msg,G,H,E,Is,Result)').


true_state(init).

init_state:-abolish(true_state,1),
    assert(true_state(init)).

update_state(S):-
   state(S),
   abolish(true_state,1),
   assert(true_state(S)),
   wn(['--------  the state has updated ---------- ',S]).

% modified: 20 Sep 2002.
% modified: 30 Dec 2002, 2 Jan 2002.
check_br_of_profile(Is,E,[GF,Scc,S,C,P,Msg]):-
    forall( 
      member(I,Is),
      (
       BrRecord = [Br,S,C,I,GF,P,Scc,Is,Msg,Pzs,Czs,Lcc],
       (br_result(BrRecord)->true;
	(
         best_response([Scc,E,Is],[GF,S,C,Msg],I,[Pzs,Czs,Lcc],Br),
         assert(br_result(BrRecord))
	)
       )
      )
    ).

br_member(0,no).

collect_br_members([S,C,GF,Scc,Is,Msg],BrMembers):-
    findall(I,
     (
      BrRecord0 = [yes,S,C,I,GF,_P,Scc,Is,Msg,_Pzs,_Czs,_Lcc],
      br_result(BrRecord0)
     ),
    BrMembers).

% modified: 30 Dec 2002, 2 Jan 2002. 
display_br_results([S,C,GF,Scc,Is,Msg],_BrMembers):-
    forall(
      (
       BrRecord0 = [Br,S,C,I,GF,_P,Scc,Is,Msg,Pzs,Czs,Lcc],
       br_result(BrRecord0)
      ),
      write_nash(I,[Pzs,Czs,Lcc],Br)
    ).


% -----------------------------------------------------------  %
%  display results (or output to file)  %%%%%%%%%%%%%%%
% -----------------------------------------------------------  %
% modified: 7 Jan 2003. to be compatible with swi-prolog 5.

write_message(S,C,P,Msg,Scc):-
    nl,
    write('For state '),write(S),
    write(', outcome '),write(C),
    ((scc(Scc,S,V),member(C,V))->Flag=in;Flag=out),
    tab(2),write([Flag,Scc]),
    write(', rule '),write(P),wn('  '),
    wn('and message profile: '),!,
    forall(member(M,Msg), (tab(5),wn(M))),
    (impl_stream(_File,write,Strm)
    -> write_message(Strm,S,C,P,Msg,Scc)
    ;wn(' no output file stream has opened.')).

write_message(Strm,S,C,P,Msg,Scc):-
  %  current_stream(_File,write,Strm),
  %  write(Strm,'Checking best response outcomes.'),
    nl(Strm),
    write(Strm,'For state '),write(Strm,S),
    write(Strm,',outcome='),write(Strm,C),
    ((scc(Scc,S,V),member(C,V))->Flag=in;Flag=out),
    tab(Strm,2),write(Strm,[Flag,Scc]),
    write(Strm,', rule='),write(Strm,P),nl(Strm),
    write(Strm,'message profile is'),nl(Strm),
    forall(member(M,Msg), 
      (tab(Strm,5),write(Strm,M),nl(Strm))).

write_nash(I,[Pzs,Czs,Lcc],Result):-
    nl,
    write(' agent='),write(I),
    write(',Pzs='),write(Pzs),
    write(',Czs='),write(Czs),
    write(',Lcc='),write(Lcc),
    ( Result=yes
    -> write('  ')
    ;  write('  ')),
    (impl_stream(_File,write,Strm) 
    -> write_nash(Strm, I,[Pzs,Czs,Lcc],Result)
    ; true),
    !.

write_nash(Strm, I,[Pzs,Czs,Lcc],Result):-   
  %  current_stream(_File,write,Strm),
    nl(Strm),
    write(Strm,' agent='),write(Strm,I),
    write(Strm,',Pzs='),write(Strm,Pzs),
    write(Strm,',Czs='),write(Strm,Czs),
    write(Strm,',Lcc='),write(Strm,Lcc),
    ( Result=yes -> write(Strm,'  ');
       write(Strm,'  ')),!.

write_nash_equilibrium(Br_Members,Is):-
  %  agents(Is),
    nl,write('Br_Members='),wn(Br_Members),
    (Br_Members = Is
   ->
    ( nl,wn('This action profile is a Nash equilibrium.'))
   ;true),
    (impl_stream(_File,write,Strm)
    ->
     write_nash_equilibrium(Strm, Br_Members,Is)
   ;true),!.

write_nash_equilibrium(Strm,Br_Members,Is):-
  %  agents(Is),
    nl(Strm),write(Strm,'Br_Members='),wn(Strm,Br_Members),
    (Br_Members = Is
   ->
    ( nl(Strm), wn(Strm,'This action profile is a Nash equilibrium.'))
   ;true),!.


write_best_response(Br_Members0,Br_Results):-
    forall(member(I,Br_Members0),
       (member([I,Pzs,Czs,Lcc,Br],Br_Results),
       write_nash(I,[Pzs,Czs,Lcc],Br))),!.



% -----------------------------------------------------------  %
%%% checking Nash outcomes with (non)zero-integer messages. 
% -----------------------------------------------------------  %
% modified: 31 Aug 2002.
% modified: Oct 2002.
% modified: 29 Dec 2002 -- 4 Jan 2003.
%-----
% modified: 27 Nov 2002. 
%  test_nash /0 refers the predifined environment 
%  and mechanism /3, as for Is, GF, and Scc.
%-----
% modified: 30 Dec 2002. check_truth_telling added.
% modified: 1-8 Jan 2002. a debug so that by 
% using mtest appropriately to generate truth telling message. 

% manual restrictions for the forms in order for computational efficiency.
% this is not used in the current version.

restrict_forms(GF,P):-
    mechanisms(Mxs),
    member(GF,Mxs),
    (member(GF, [gM,gMR]) -> member(P,[1,2,3]);true),
  % As for gM, P=3 (integer-game) may be excluded for simplicity, 
  % although it is not exact simulation, since it never brings about NE. 
    (member(GF,[gD]) -> (member(P,[1,2,3]),N = 2);true),
    (member(GF,[gMR2]) -> (member(P,[1,2,3,4,5]),N = 2);true).


test_nash(Mode,GF,[C,S],[P,Scc,H],Msg,Is,Result):-
   % find a legitimate outcome for nash/6 to reduce backtrack.
    E = environment([Is,_,_],[N,_,_],_),
    (
     E -> true; 
     (
      write('agents specified not match with the current model.'),
      write('Will you update the current model? (y/n) '),
      (read(y)->(hear(domain,D),setup_domain(D));fail)
     )
    ),
    G =.. [GF,P,Scc],
    scc(Scc),            %wn(Scc),
   %  <-- of course, you shoud'nt use "scc_defined_state(S,Scc)" instead.
    reversion(H,S,_,_),
   % reversion/4 is not used in this version. identity h0 assumed. 
    subset_of_agents(Is,N),
    state(S),
    alternative(C),
   % frame of discernment: verify game forms sequentially!
   % restrict_forms(GF,P),        %wn([GF,P]),
   % --->
    Mode=..[MX,Z0],
    sim_mode(MX),
    mtest(Z0,GF,Scc, Msg,Is),
   %(mtest(Z0,GF,Scc, Msg,Is)->true;fail),
    mechanism(G,Msg,[C]),
    check_truth_telling(MX, GF, Scc, Is, S,Msg), % added: 30 Dec. 
   % <--
    nash(C,S,Msg,G,H,E,Is,Result).


test_nash(_Mode,GF,[C,S],[P,Scc,_H],null,_Is,null):-
    G =.. [GF,P,Scc],
    wn(['no message to yield',C,by,G,state,S]).
     % When the mechanism use the integer roulette, there must exist an 
     % such outcome via mtest insted mtest_z0, and then
     % the process thereafter will be skipped. 


% a cui predicate for test_nash.
% modified: 29,30 Dec 2002. 2-3,8 Jan 202.
% to permit a change of the default model parms and env.
% a local utility read_alt, hear_sim_parms, and user_update_env has added.


test_nash:-
   wn(' goal format: '),
   wn('  test_nash(Mode,GF,[C,S],[P,Scc,H],Msg,Is,Result)'),
   wn('-----------------------------------------------------'),
   (
    (
     clause(default_model([GF,Scc,Is,E]),true),
     E=environment([Is,_,_],[_N,_,_],_)
    )
    ->true;
     (write('The model has not yet built.'),fail)
   ),
   (
    G=..[GF,_,Scc],
    (clause(mechanism(G,_,_),true)->Mode=full,Zero=0;Mode=truthful,Zero=0),
    wn('I guess your goal may be ...'),
    tab(3),
    write('test_nash('),write(Mode),write('('),
    write(Zero),write('),'),
    write(GF),write(',[C,S],[P,'),
    write(Scc),write(', h0],Msg,'),
    write(Is),wn(', yes).'),
    wn(' -----------------------'),
    wn(' do this? (y/n) '),read(U)
   ),
   (
     Result =yes,
     Mode0=..[Mode,Zero],
     U=y->
      (
       test_nash(Mode0,GF,[C,S],[P,Scc,h0],Msg,Is, yes),
       wn([mes,Msg,[C,S],yield,[rule,P,scc,Scc]])
      );
      (
       hear_sim_parms(
         [Mode,Zero,GF,C,S,P,Scc,Is,Result],
         [Mode1,Zero1,GF1,C1,S1,P1,Scc1,Is1,Result1],
         [yes,yes,yes,yes,yes,yes,yes,yes,yes]
       ),
       user_update_env([GF1,Scc1,Is1,_E1]),
       Mode2 =.. [Mode1,Zero1], 
       Goal=test_nash(Mode2,GF1,[C1,S1],[P1,Scc1,h0],Msg,Is1,Result1),
       do_and_update_goal(Goal),
       wn([mes,Msg,[C1,S1],yield,[rule,P1,scc,Scc1]])
      )
   ).

% this position is sensitive.
test_nash:-hear(domain,D),setup_domain(D),test_nash.

do_and_update_goal(Goal):-
   Goal,
   abolish(last_goal,1),
   assert(last_goal(Goal)).

last_goal(non).

hear_sim_parms(Defaults,Users,Choices):-
   Choices = [X1,X2,X3,X4,X5,X6,X7,X8,X9],
   Defaults = [Mode,Zero,GF,C,S,P,Scc,Is,Result],
   Users = [Mode1,Zero1,GF1,C1,S1,P1,Scc1,Is1,Result1],
   write('(You may type `default` instead if default as above.)'),nl,
   %----------------------------------------------------------------
   (X1=yes->
      (
       write('truncate if not best response? (full/truthful)'),
       read_alt(Mode,Mode1,choice(Mode1,sim_mode(Mode1)))
      )
   ;true),
   (X2=yes->(write('all zero?(0/Var)'),read_alt(Zero,Zero1,[0,var(1)]));true),
   (X3=yes->(write('mechanism? '),mechanisms(GFs),read_alt(GF,GF1,GFs));true),
   (X4=yes->(write('outcome? '),alternatives(As),read_alt(C,C1,As));true),
   (X5=yes->(write('state? '),states(Ss),read_alt(S,S1,Ss));true),
   (X6=yes->(write('rule? '),game_forms(GF,Ps),read_alt(P,P1,Ps));true),
   (X7=yes->(write('scc? '),sccs(Sccs),read_alt(Scc,Scc1,Sccs));true),
   (X8=yes->(write('agents? '),read_alt(Is,Is1,choice(Is,subset_of_agents(Is,_))));true),
   (X9=yes->(write('nash? (yes/no/V) '),read_alt(Result,Result1,[yes,no,var(2)]));true),
   %----------------------------------------------------------------
   write([Mode,Zero,GF,C,S,P,Scc,Is,Result]),nl,
   write([Mode1,Zero1,GF1,C1,S1,P1,Scc1,Is1,Result1]),
   nl.


read_alt(Default,Y,choice(Y,X)):-
   read(User),
   % caution: read must  be separated from below.
   (
    (var(User), Y = Default);
    (User = default, Y = Default);
    (X, Y = User);
    (
     write('not regular input. please re-enter. '),
     read_alt(Default,Y,choice(Y,X))
    )
   ). 

read_alt(Default,Y,Menu):-
   read(User),
   % caution: read must  be separated from below.
   (
    (var(User), member(var(_),Menu));
    (User = default, Y = Default);
    (member(Y,Menu), Y = User);
    (
     write('please select from : '),
     write(Menu),
     read_alt(Default,Y,Menu)
    )
   ). 

user_update_env([GF1,Scc1,Is1,_E1]):-
   write('Are you make another environment and default? (y/n) '),
   read(Env),
   (
    (Env = y, update_env([GF1,Scc1,Is1,_E1]));
    (Env = n, true);
    (
     write('please type either y or n. '),
     user_update_env([GF1,Scc1,Is1,_E1])
    )
   ).


% -----------------------------------------------------------  %
% another tesing for Nash equilibria %
% -----------------------------------------------------------  %
% nec /1, ne /4, br /6 added: 25 Oct 2002.

% modified: 7 Jan 2003.
br(IN,M,[S,O],G,J,Is,[Pzs,Czs,Lcc]):-
    ((scc(Scc,S,In_Scc),member(O,In_Scc))-> IN = in; IN = out),
    br_result([yes,S,O,J,GF,P,Scc,Is,M,Pzs,Czs,Lcc]),
    G=..[GF,P,Scc].

nec(NC):- setof(B,A^P^ne(A,B,[1,2,3],gM(P,f)),NC).

ne(M,[S,O],Is,G):-
	br(IN,M,[S,O],G,J,Is,_L0),
	forall(
		member(J,Is),
		L^br(IN,M,[S,O],G,J,Is,L)
	).

test_ne(mes(B),alt(C),state(S),game(gM,f,P),nash(R)):- 
	mtest(gM,f,B,[1,2,3]),
	mechanism(gM(P,f),B,[C]),
	nash(full(_),C,S,B,gM(P,f),h0,_,[1,2,3],R).


test_ne:-
   wn('test_ne(mes(B),alt(C),state(S),game(gM,f,P),nash(R))'),
   write('ok?(y/n) '),read(y),
   test_ne(mes(_B),alt(C),state(S),game(gM,f,P),nash(R)),
   /*
   wn('Now finding a Nash equilibrium. wait.'),
   tab(3),wn('mes(B):B='),
   forall(member(D,B),(tab(5),wn(D))),
   */
   tab(3),write(alt(C)),
   tab(1),write(state(S)),
   tab(1),write(game(gM,f,P)),
   tab(1),wn(nash(R)),
   write('find another?(y/n) '),
   (read(y)->fail;true).


% -----------------------------------------------------------  %
% tesing implementability %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% -----------------------------------------------------------  %
% test_impl/5 the simulation of Nash implementation with output file. 
% edited from: Dec 2001.
% modified: 10 Nov 2002.

% A SCC F is h-Nash implementable if 
% there exists a mechanism, (M,g), such that, for all s: 
% (1) For each a in F(s) there exists an h-Nash equilibrium, m in M, 
% such that H(g(m),s,h)=a.
% (2) If m in M is an h-Nash equilibrium at s, then H(g(m),s,h) in F(s).

% modified: 29,30 Dec 2002. 2-4,8 Jan 2003.
test_impl:-
   wn(' goal format:'), wn('  test_impl(GF,Scc,Is,Mode,Summary)'),
   wn('-------------------------------------------------------'),
   (
    clause(default_model([GF,Scc,Is,E]),true),
    E = environment(_,_,_),
    clause(E,true)
    ->true;
     (write('The model has not yet built.'),fail)
   ),
   (
    G=..[GF,_,Scc],
    (clause(mechanism(G,_,_),true)->Mode=full,Zero=0;Mode=truthful,Zero=0),
    Mode0=..[Mode,Zero],
    V=test_impl(GF,Scc,Is,Mode0,Summary),
    write('I guess that your goal may be..'),nl,
    write( V),nl,
    write('do this? (y/n) '),
    (read(y)->do_and_update_goal(V);
      (
       write('Will you change the model? (y/n) '),
       read(y)
        ->(setup_domain,test_impl);
         (
          Defaults = [Mode,Zero,GF,_C,_S,_P,Scc,Is,_],
          Users = [Mode1,Zero1,GF1,_C1,_S1,_P1,Scc1,Is1,_],
          Choices = [yes,yes,yes,no,no,no,yes,yes,no],
          hear_sim_parms(Defaults,Users,Choices),
          Mode2=..[Mode1,Zero1],
          V1=test_impl(GF1,Scc1,Is1,Mode2,Summary),
          do_and_update_goal(V1)
         )
      )
    )
   ).

test_impl:-hear(domain,D),setup_domain(D),test_impl.

% modified: 1-2 jan 2002.  time stamp, Mode. 
test_impl(GF,Scc,Is,Mode,Summary):-
    trim_stacks,
    Mode=..[Mod1,_],
    sim_mode(Mod1),
    ( \+ (scc(Scc,_,_))
    -> (wn('no such Scc.'),fail);true),
    subset_of_agents(Is,N),\+ member(N, [0,1]),
    open_output_file(Strm,Scc),
    write(Strm,test_impl(GF,Scc,Is,Mode,Summary)),
    nl(Strm),
    G=..[GF,_P,Scc],
    % to check the online / batch mode of mechanism/3.
    (clause(mechanism(G,_,_),true)
     ->(write(Strm,'mechanism/3 loaded from a file.'),nl(Strm))
     ;true),
    write(Strm,'start ---------------------'),
    tstamp(Strm),
    init_summary(Scc),
    clear_br_results,
    H = h0,
    display_scc(Strm,Scc,Is,GF),
    display_domain(Strm),
    test_for_model(Strm,Scc,Is),
%
    collect_statistics(Stat1),
    init_state,
    check_on_scc(GF,Is,Scc,H,Mode,Strm),
    check_off_scc(GF,Is,Scc,H,Mode,Strm),
    write(Strm,'end <-----------------------'),
    tstamp(Strm),
    init_state,
    collect_statistics(Stat2),
%
    write_summary(Strm,Summary),
    write_statistics(Strm,Stat1,Stat2),
    close_output_file(Strm),
    write('save br_results? (y/n) '),read(Save),
    (Save = y -> save_br_results(_BFile,_BStrm);true),
    wn('end'),
    trim_stacks.


% added: 30 Dec 2002.
% modified: 2 Jan 2002.
sim_mode(Mode):-
    member(Mode,[full,truthful]).
%   member(Mode,[full(_),part(_),truthful(_)]).


% modified: 7 Jan 2003. to be compatible with swi-prolog 5.
open_output_file(Strm,Scc):-
    scc(Scc,_,_),
    wn('create output file for this Scc.'),
    concat('imp_',Scc,File1),
    concat(File1,'.txt',File),
    open(File,write,Strm),
    abolish(impl_stream,3),
    assert(impl_stream(File,write,Strm)).

impl_stream(dummy,write,_):- fail.

close_output_file(Strm):-
    close(Strm),
    abolish(impl_stream,3).


check_on_scc(GF,Is,F,H,Mode,Strm):-
    % check the outcomes on the domain of the scc.
    % By this part, you can verify the completeness of the mechanism.
    wn('checking the on-SCC patterns:'),
    wn(Strm,'checking the on-SCC patterns:'),
    findall((S,O),
         D^(state(S),alternative(O),scc(F,S,D),member(O,D)),
      ONp),
    sort(ONp,ON),
    forall(member((S,O),ON),
     (
       write([S,O]),  write(Strm,[S,O])
     )),nl,  nl(Strm),!,
    forall(member((S,O),ON),
     (
      (%ttm(GF,F,Msg,Is,S),wn([S,Msg]),  %?% truth-telling imposed.
       update_state(S),   % update_state should be done before mechanism.
       restrict_forms(GF,P),
       test_nash(Mode,GF,[O,S],[P,F,H],_Msg,Is,yes)->Yes=nash_yes;Yes=nash_no),
       update_summary([S,O,Yes,scc_in])
     )),nl,  nl(Strm),!.

check_off_scc(GF,Is,F,H,Mode,Strm):-
    % check the outcomes off the domain of the scc.
    % By this part, you can verify the soundness of the mechanism.
    wn('checking the off-SCC patterns:'),
    wn(Strm,'checking the off-SCC patterns:'),
    findall((S,O),
         D^(state(S),alternative(O),scc(F,S,D),\+member(O,D)),
      OFFp),
    sort(OFFp,OFF),
    forall(member((S,O),OFF),
     (
       write([S,O]),  write(Strm,[S,O])
     )),nl,  nl(Strm),!,
    forall(member((S,O),OFF),
     (
      (
       update_state(S),   % update_state should be done before mechanism.
       restrict_forms(GF,P),
       test_nash(Mode,GF,[O,S],[P,F,H],_M,Is,yes)->No=nash_yes;No=nash_no),
       update_summary([S,O,No,scc_out])
     )),nl,  nl(Strm),!.


display_scc(Scc,Is,GF):-
   nl,
   wn('Testing Nash implementability via prolog simulation'),
   nl,
   wn(' **** the model specification ****** '),
   nl,
   write('the members of this society: '),wn(Is),
   nl,write('game form: '),wn(GF),
   nl,wn('scc: '),
   forall(scc(Scc,S,D),
       (   write(Scc),write('('),write(S),write(')'),
           write(' = '), write(D),tab(3)
       )),
   nl,
   (  monotone(Scc,Is)->wn('is Maskin-monotone.');
      wn('is not Maskin-monotone.')),
   (  ess_monotone(Scc,Is)->wn('is Essentially-monotone.');
      wn('is not Essentially-monotone.')),
   (member(GF,[gD,gMR2,gDict])
    ->disp_mr_ir(Scc,Is);true).



display_scc(Strm,Scc,Is,GF):-
    display_scc(Scc,Is,GF),
    current_stream(_File,write,Strm),
    nl(Strm),
    wn(Strm,'Testing Nash implementability via prolog simulation'),
    nl(Strm),
    wn(Strm,' **** the model specification ****** '),
    nl(Strm),
    write(Strm,'game form: '),wn(Strm,GF),
    write(Strm,'members of society: '),
    write(Strm,Is),nl(Strm),
    nl(Strm),write(Strm,'Scc: '),nl(Strm),
    forall(scc(Scc,S,D),
       (   write(Strm,Scc),write(Strm,'('),
           write(Strm,S),write(Strm,')'),
           write(Strm,' = '), write(Strm,D),tab(Strm,3)
       )),
    nl(Strm),
    (monotone(Scc,Is)->wn(Strm,'is Maskin-monotone.');
     wn(Strm,'is not Maskin-monotone.')),
    (ess_monotone(Scc,Is)->wn(Strm,'is Essentially-monotone.');
     wn(Strm,'is not Essentially-monotone.')),
    (member(GF,[gD,gMR2,gDict])
    ->disp_mr_ir(Strm,Scc,Is);true),
    !.

disp_mr_ir(Scc,[I,J]):-
    (has_MR_property(Scc,[I,J])->wn('has Moore-Repullo property.');
     wn('does not have Moore-Repullo property.')),
    (test_irat_n2(Scc,[I,J])->wn('is individually-rational.');
     wn('is not individually-rational.')),wn(end),true.

disp_mr_ir(Strm,Scc,[I,J]):-
    (has_MR_property(Scc,[I,J])
    ->wn(Strm,'has Moore-Repullo property (defined by Danilov).');
     wn(Strm,'does not have Moore-Repullo property  (defined by Danilov).')),
    (test_irat_n2(Scc,[I,J])->wn(Strm,'is individually-rational.');
     wn(Strm,'is not individually-rational.')).


% display_domain is decribed in the preference part.

test_for_model(Strm,Scc,Is):-
   tests_for_scc(Scc,Is,G0),
   test_mju(Scc,Is,Gm), append(G0,Gm,G),
   nl,wn('other tests for this model:'),wn(G),
  (var(Strm)->true;
   (
    nl(Strm),
    wn(Strm,'other tests for this model'),
    wn(Strm,G)
   )
  ).


init_summary(F):-
    abolish(summary,1),
    assert(summary([])),
    forall((state(S),alternative(O),scc(F,S,D),member(O,D)),
     (
       update_summary([S,O,default,scc_in])
     )),nl,
    forall((state(S),alternative(O),scc(F,S,D),\+member(O,D)),
     (
       update_summary([S,O,default,scc_out])
     )).

update_summary([S,O,Result,InScc]):-
     summary(Summary0),
     subtract(Summary0,[[S,O,default,InScc]],Summary2),
     append(Summary2,[[S,O,Result,InScc]],Summary3),
     sort(Summary3,Summary1), 
     retract(summary(Summary0)),
     assert(summary(Summary1)).

% modified: 10 Nov 2002. The stream to be unified with Strm.

write_summary(Strm,Summary):-
    summary(Summary),
    current_stream(_File,write,Strm),
    nl(Strm),
    wn('Summary Results'),
    wn(Strm,'Summary Result'),
    forall(member([S,O,Result,InScc],Summary),
     (
       write([S,O,Result,InScc]),nl,
       write(Strm,[S,O,Result,InScc]),nl(Strm)
     )),
    nl,wn('completed.').

stat_keys(a,[cputime,inferences,heapused,
          localused,globalused,trailused]).
stat_keys(b,[atoms,functors,predicates,modules,codes]).
stat_keys(Keys):-
    stat_keys(a,KeysA),
    stat_keys(b,KeysB),
    append(KeysA,KeysB,Keys),!.

collect_statistics(Stat):-
    stat_keys(Keys),
    bagof(Value,
        Key^(member(Key,Keys),
             statistics(Key,Value)),Stat),!.

write_statistics(Strm,Stat1,Stat2):-
  %  stat_keys(a,KeysA),
  %  stat_keys(b,KeysB),
    stat_keys(Keys),
    current_stream(_File,write,Strm),
    nl(Strm),
    wn(Strm,'Statistics'),
    forall(member(Value1,Stat1),
      (
         nth1(Nth,Stat1,Value1),
         nth1(Nth,Stat2,Value2),
         nth1(Nth,Keys,Key),
         write(Strm,Key),
         write(Strm,'= '),
         %(member(Key,KeysA)->(ValueD is Value2 - Value1;ValueD is 0)),
         ValueD is Value2 - Value1,
         wn(Strm,[ValueD, 'increased from',Value1])
      )
    ),!.




% -----------------------------------------------------------  %
%  save results of best response checkings (or output to file) %
% -----------------------------------------------------------  %
%br_result([Br,S,C,I,GF,P,Scc,Is,Msg,Pzs,Czs,Lcc])

% modified: 7 Jan 2003. to be compatible with swi-prolog 5.

br_result(dummy).

br_stream(dummy,_):- fail.

save_br_results(File,Strm):-
    br_result(BR),nth1(5,BR,GF),nth1(7,BR,Scc),
    wn('..saving to file :'),
    % modified: 27 Nov 2002.
    (br_stream(_File0,write,Strm)->close(Strm);true),
   % listing(br_result),
    open_br_file(Scc,GF,File,Strm),
    abolish(br_stream,2),
    assert(br_stream(File,Strm)),
    write_br_results(File,Strm).

open_br_file(Scc,GF,File,Strm):-
    scc(Scc,_,_),
    concat('br',Scc,FN1),
    concat(FN1,'_',FN2),
    concat(FN2,GF,FN3),
    concat(FN3,'.txt',File),
    open(File,write,Strm).

open_br_file(Scc,_GF,_File,_Strm):-
    \+ scc(Scc,_,_),
    wn('no such Scc.').

% modified: 10 Nov 2002.
% modified: 7 Jan 2003.
write_br_results(File,Strm):-
    current_stream(File,write,Strm),
    br_result(BR),
   %nth1(2,BR,S),nth1(3,BR,C),nth1(7,BR,Scc),
   %((scc(Scc,S,In_Scc),member(C,In_Scc))-> IN = in; IN = out),
   %write(Strm,br(IN,BR)),wn(Strm,'.'),
    write(Strm,br_result(BR)),wn(Strm,'.'),
    fail.
 % older version:
 %   forall(member(R,BR),(write(Strm,R),write(Strm,', '))),
 %   write(Strm,'eor'),nl(Strm),
 %   fail.

write_br_results(File,Strm):-
    current_stream(File,write,Strm),
    close(Strm),
    abolish(br_stream,2),
    wn('no more br_result in this DB. '),
    clear_br_results.

% modified: 1 Sep 2002.
clear_br_results:-
    write('clear br_result records?(y/n) '),
    read(U),
    (U=y
    ->
      (abolish(br_result,1),
       assert(br_result(dummy))
      );true
    ).




%%%%%  several tests for constructing nash equilibrium messege
% added: Aug 2002.
 
test_abn(M,D,[Pzs,Czs,Lcc,Br]):-
    D=[([x],0),([x,y],0)],
    test_nash(full,gD,[x,s2],[1,udd1,h0],D,[1,2],_F),
    best_response([udd1,_E,[1,2]],[gD,s2,x,D],2,[Pzs,Czs,Lcc],Br),
    mutate(gD,udd1,2,[1,2],D,M), 
    test_gD(udd1,[1,2],[2,y,M]).

test_abn1(F):-
    D=[([x,y],0),([x,y],0)],
    test_nash(full,gD,[y,s4],[1,umd5,h0],D,[1,2],F).



/*
% iteratively remove non best responses. edited: 8 Sep 2002.
% this code is pending.

irmv_nbr(GF,Scc,Is):-
    iterative_removal_of_nbr(GF,Scc,Is).
iterative_removal_of_nbr(GF,Scc,Is):-
    G=..[GF,_P,Scc],
    (mechanism(G,_,_)->true;(wn('no verified messages.'),fail)),
    forall(
      (
       mechanism(G,M,Z),wn([G,M,Z])
      ),
      (
        (
         member(C,Z),%wn([C]),
         alternative(C),
         state(S),%wn([S]),
         agent(I),%wn([I]),
         member(I,Is),
         best_response([Scc,_E,Is],[GF,S,C,M],I,Results,Br),
         wn([state(S),agent(I),br,Results,Br]),Br=no
        )
       ->
        (
         retract(mechanism(G,M,Z)),wn(this_message_has_removed_from_db)
        )
       ;true
      )
    ).

*/



%--------------------------------------%
% time stamp
%--------------------------------------%
% added: 1 Jan 2003. 

tstamp(S):-
  get_time(U),
  convert_time(U,A,B,C,D,E,F,_G),
  T = [date(A/B/C), time(D:E:F)],
  write(S,T),nl.


% -----------------------------------------------------------  %
% start_up %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% -----------------------------------------------------------  %


init_prompt:-prompt(_,'input by user:').%prolog-based mechanism design theory.

:- welcome,nl.

   %init_prompt.
   % edit_history,init_prompt, reference_list.





% -----------------------------------------------------------  %
%  END of the program
% -----------------------------------------------------------  %

% trash:
% the tomb of some bugs once lived in the brain which has killed by me.
/*
 % -----  abolished 28 Sep 2002 ------- %
sub_condition_of_mju(ii,F,Is,Bx,[A,S,Cxs]):-
% this corresponds to Moores-Repullo's condition, mju (ii), rvp. 
   scc(F),
   subset_of_agents(Is,_),
   subset_of_alt(Bx,_), 
   forall(
     (
      member([J,A,S,Cx],Cxs),
      agent(J),member(J,Is),
      state(S1),alternative(C0),
      lcc([J,S1,R1],C0,Lcc),subset(Cx,Lcc),
      forall(
        (member(J1,Is), J1 \= J),
        (
         preference(J1,S1,R1),
         lcc([J1,S1,R1],C0,Lcc1),subset(Bx,Lcc1),
         tab(4),wn([C0,J1,S1,lcc,Lcc1,includesBx])
        )
      )
     ),
     (
      scc(F,S,V),member(C0,V),tab(6),wn([C0,in_scc])
     )
   ).
sub_condition_of_mju(iii,F,Is,Bx,[_A,_S,_Cxs]):-
% this corresponds to Moores-Repullo's condition, mju (iii), unanimity. 
   scc(F),
   subset_of_agents(Is,_),
   subset_of_alt(Bx,_),
   forall(
    (
     scc_defined_state(S,F),
     prefer_profile(Is,S,Rs),
     tab(4),wn([profile(S),Rs]),
    %----
     member(C0,Bx),
     forall(
       member(J1,Is),
       (
        preference(J1,S,R1),
        lcc([J1,S,R1],C0,Lcc),
        subset(Bx,Lcc),
        tab(5),wn([C0,J1,S,lcc,Lcc,includesBx])
       )
     )
    ),
    (
     scc(F,S,V),member(C0,V),tab(6),wn([C0,in_scc])
    )
   ).

 % -----  abolished 10 Dec 2002 ------- %
game_form(gM(2,Scc),E,Msg,[C]):-%wn(rule2),
      E = environment([Is,_Ss,_As],[N,_K,_L],_Rs),
      length(Msg,N),
/*
  % extended for N >= 3. if N=3,
    (Msg = [(R1,C1,Z1),(R2,C2,Z2),(R2,C2,Z3)] -> (K is 1,true);
    Msg = [(R2,C2,Z1),(R1,C1,Z2),(R2,C2,Z3)] -> (K is 2,true);
    Msg = [(R2,C2,Z1),(R2,C2,Z2),(R1,C1,Z3)] -> (K is 3,true)),
    nth1(K,Is,J),
*/
  %wn((rule,2,[J,K],Msg)),read(y),
  % the agreed preference, R2J, of the agent J who has the unique, 
  % and distinctive opinion. estimated same by other two simultaneously.
      setof((R,X,0),Z^(member((R,X,Z),Msg)),MD),length(MD,2),
    %  wn(MD),read(y),
    % find a single deviator's message (by sure thing reasoning).
      member(MJ,Msg),   
      counter(1,MJ,Msg),  % <--MJ has to be specified. 
      nth1(K,Msg,MJ),
      nth1(K,Is,J),
    % which message is that sent from the deviator.
      MJ = (R1,C1,_Z1),
      member(MJ1,MD),
      MJ1 = (R1,C1,0), % match with MJ partially (if ignore integer).
      member(MJ2,MD),
      \+ MJ2 = MJ1,
      MJ2 = (R2,C2,0),
     % check in_scc for the agreed outcome.
      state(S),          %wn(state(S)),
      prefer_profile(Is,S,R2),
      scc(Scc,S,Obj),
      alternative(C2),
      member(C2,Obj),
      !,
      nth1(K,R2,R2J),
      preference(J,S,R2J),
      lcc([J,S,R2J],C2,Lcc),
      ess(Scc,J,Lcc,Ess),
      %(Ess\=[]->true;wn('at rule 2, the ess is empty.'),read(y)),
      % modified: 27 Nov 2002.
      % Since a code previously modified beneath (10 Nov 2002) was wrong.
      %(Ess\=[]->DictRange=Ess;DictRange=Lcc),
      (member(C1,Ess)-> C = C1; C = C2),
     %lpom(Msg,[gM,Scc,Is],_Zs),%write(lpom),read(y),
      range(Scc,Range),member(C,Range).


/*
game_form(gM(old(2),Scc),E,Msg,[C]):-%wn(rule2),
      E = environment([Is,_Ss,_As],[N,_,_],_Rs),
      length(Msg,N),
/*
  % extended for N >= 3. if N=3,
    (Msg = [(R1,C1,Z1),(R2,C2,Z2),(R2,C2,Z3)] -> (K is 1,true);
    Msg = [(R2,C2,Z1),(R1,C1,Z2),(R2,C2,Z3)] -> (K is 2,true);
    Msg = [(R2,C2,Z1),(R2,C2,Z2),(R1,C1,Z3)] -> (K is 3,true)),
    nth1(K,Is,J),
*/
  % the agreed preference, R2J, except for, J, the deviancy who has a unique 
  % and distinctive opinion.
  %wn((rule,2,[J,K],Msg)),read(y),
      nth1(K,Is,J),
      nth1(K,Msg,MJ),
      MJ = (R1,C1,_Z1),
      bagof((R,X,0),Z^(member((R,X,Z),Msg)),MD),
      subtract(MD,[(R1,C1,0)],[(R2,C2,0),(R2,C2,0)]),
     % check in_scc for the agreed outcome.
      state(S),
      prefer_profile(Is,S,R2),
      scc(Scc,S,Obj),
      alternative(C2),
      member(C2,Obj),
      !,
      nth1(K,R2,R2J),
      preference(J,S,R2J),
      lcc([J,S,R2J],C2,Lcc),
      ess(Scc,J,Lcc,Ess),
      (member(C1,Ess)-> C = C1; C = C2).
      %range(Scc,Range),member(C,Range).
*/

% -----------------------------------------------------------  %
   %%%  equilibrium outcomes correspondence  %%
% -----------------------------------------------------------  %
% added: 25 Aug 2002. modified: 31 Aug 2002. 
% abolished: 2 Jan 2003. 

nash_correspondence([GF,Scc,E],S,Ncc):-   
    agents(Is),
    E = environment([Is,_,_],[_N,_,_],_),
    E,
    scc(Scc),
    state(S),
    findall(C,
      (
	G=..[GF,_P,Scc],
        alternative(C),wn([for,C]),
        nash(part,C,S,_M,G,h0,E,Is,yes),wn(ok)
      ),
    NEs),
    sort(NEs,Ncc).
nash_correspondence0([GF,Scc,E],S,Ncc0):-   
    E = environment([Is,_,_],[_N,_,_],_),
    E,
    alternative(C),state(S),
    findall([C,P,M],
      (
	G=..[GF,P,Scc],
	P^M^nash1([Is,G,E],[C,S,P,M])
      ),
    Ncc0).

nash0([Is,G,E],[C,S,P,M]):-
   G =..[GF,P,Scc],
   mtest_z0(GF,Scc, M,Is),
   nash(part,C,S,M,G,h0,E,Is,yes).



% some test routines

test_mes_mr(M):-
   M1= ([[a,c,d,b,z],[b,d,c,a,z]], c, a, 0),
   M2= ([[a,d,c,b,z],[b,c,d,a,z]], c, a, 0),
   M=[M1,M2].

test_mut_mr([M,M1],J,[P,P1],[C,C1]):-
   test_mes_mr(M),
   mutate_mechanism(gMR2,J,[P,P1],[C,C1],[M,M1]).

te_mr(M,[V1,V2],[Br1,Br2]):-
   M1= ([[a,c,d,b,z],[b,d,c,a,z]], c, a, 0),
   M2= ([[a,d,c,b,z],[b,c,d,a,z]], c, a, 0),
   M=[M1,M2],
   mechanism(gMR2(2,mr),M,[c]),wn([M,c]),
   best_response([mr,_E,[1,2]],[gMR2,s2,c,M],1,V1,Br1),
   best_response([mr,_E,[1,2]],[gMR2,s2,c,M],2,V2,Br2).



%---------


% -----------------------------------------------------------  %
% abolished message profiles
% -----------------------------------------------------------  %

%abolished: 28 Dec 2002.
mtest(gM,Scc,Msg,Is):-
    scc(Scc),
    subset_of_agents(Is,N),
    gM_profile(Scc,Is,Msg),
    length(Msg,N).
mtest(gMR, F,M,Is):-
    scc(F),
    subset_of_agents(Is,_N),
    mr_profile(Is,F,M).
mtest(gMR2, F,M,Is):-
    scc(F),
    subset_of_agents(Is,2),
    mr2_profile(Is,F,M).
% test for mr
mtest(gMR2,[[A,B],[R1,R2],[S1,S2],[V1,V2]]):-
   mtest(gMR2,mr,[[R1,A,_,_],[R2,B,_,_]],[1,2]),
   prefer_profile([1,2],S1,R1),
   prefer_profile([1,2],S2,R2),
   scc(mr,S1,V1),
   scc(mr,S2,V2).

% alternative code for message profiles those which
% were abolished because of state-dependence.
/*
% modified: 04 Sep 2002.(abolished)
gM_profile(F,Is,Prf):-
    scc(F),
    subset_of_agents(Is,_N),
    my_maplist(maskin(F,Is,_S),Is,Prf).

mr_profile(Is,F,Prf):-
    subset_of_agents(Is,_N),
    scc(F),
    my_maplist(mr_msg(Is,F),Is,Prf).

mr2_msg([J1,J2],F,J,M2):-
    mr_msg([J1,J2],F,J,M),
    M=(R,A,B,Z),
    M2=(R,A,B,Z,Obj),
    member(Obj,[0,1]).

mr2_profile([J1,J2],F,Prf):-
    subset_of_agents([J1,J2],2),
    scc(F),
    my_maplist(mr2_msg([J1,J2],F),[J1,J2],Prf).

% a version in pending
maskin(F,Is,S,J,(R,A,Z)):-
    scc(F),
    subset_of_agents(Is,N),
    agent(J), member(J,Is),
    alternative(A),
    state(S), 
    prefer_profile(Is,S,R),%wn([Is,S,R]),
    scc(F,S,V),%wn([scc,Obj]),
    member(A,V),
    asc_nnseq(Aq,N),%wn([Aq,N]),
    member(Z,Aq).

tt_gM_profile(F,Is,S,Prf):-
    scc(F),
    subset_of_agents(Is,_N),
    state(S),
    my_maplist(maskin(F,Is,S),Is,Prf).
*/



% ---------------------------- % */



return to front page.