You selected impl0903.pl



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



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



welcome:-
 nl,
 wn(' %****************************************************%'),
 wn(' %*    Nash implementation theory on SWI-prolog.     *'),
 wn(' %*              version impl09                      *'),
 wn(' %****************************************************%'),
 wn(' % Sep 2001--Aug 2002.'),
 wn(' % author: Kenryo INDO (Kanto Gakuen University)'),
 wn(' % Dept of Management, Faculty of Economics, '),
 wn(' % Kanto Gakuen University. Ota, Gunma, 373-8515 Japan.'),
 wn(' % -------------------------------------------------- %'),
 wn(' % To explain more, try goals bellow.'),
 wn(' % explain_me/0, edit_history/0, reference_list/0.'),
 wn(' % To display this again, welcome/0.').

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,3,O) and return key if 3-person case, '),
  wn('%   test_impl(gD,F,[I,J],2,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(01),
	'E. Maskin and T. Sjostrom',
	2001,
	'Implementation theory.',
	'url:http//www.???',
	'???',
	'To be appeared in ???').
ref(m(98),
	'E. Maskin',
	1998,
	'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(su(96),
	'S.-C. Su',
	1996,
	'An algorithm for checking strong Nash implementability.',
	'Journal of Mathematical Economics',
	'25:109-22.',_).


edit_history:-
  wn(H1),H1='% editing 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 result_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('% end of the edition history %').



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


% -----------------------------------------------------------  %
%%%%%% 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.) 

%--

/*  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).
*/


% projection(3rd ar) of vector(2nd ar) using a sequence of digits(1st ar). 
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).

% 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
% -----------------------------------------------------------  %
seteq(X,Y,L):-
   length(X,L),
   length(Y,L),
   forall(member(Z,X),member(Z,Y)),
   forall(member(Z,Y),member(Z,X)).


% 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
% -----------------------------------------------------------  %
bag1([],_A,0).
bag1([C|B],A,N):-length([C|B],N),bag1(B,A,_N1),%N is N1 + 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. 


poa(P,APs):-
   alternatives(A),
   permutation_of(A,P,APs).
permutation_of(A,P,APs):-
   length(A,M),
   ordering(P,A,M),
   asc_nnseq(Qm,M),
   my_maplist(nth_of_permutation(A,P),Qm,APs).
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).

% 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


results_to_file:-
   tab(5),write(' input your goal'),read(U1),
   tab(5),write(' output file'),read(U2),
   concat(U2,'.txt',File),
   U1=..Goal,
   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).
results_to_file(Goal,File,S):-
  current_stream(File,write,S),
  %Goal=[_G,_A,_B,_Is],
  Goal1=..Goal,
  Goal1,
  wn(Goal),
  write(S,Goal),nl(S),
  fail.
results_to_file(_Goal,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'),
  G=..Goal,G,
  tell(user),wn(end),
  current_stream('tell.txt',write,S),
  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).
*/

alternative(A):-alternatives(As),member(A,As).
agent(I):-agents(N),member(I,N).
state(S):-states(Ss),member(S,Ss).

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


% エージェントの選好 *********************
% -----------------------------------------------------------  %
%  *****  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)

prefer_to(I,S,X,Y):-
  preference(I,S,Order),
  nth1(J,Order,X),
  nth1(K,Order,Y),
  J =< K. 
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):-
  prefer_to(I,S,X,Y),
  prefer_to(I,S,Y,X).

% strict ordering.
strict_prefer_to(I,S,X,Y):-
  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.
%strict_prefer_to(I,S,X,Y):-
%  prefer_to(I,S,X,Y),
%  \+indifferent_to(I,S,X,Y).
% but next one is erroneous.
%strict_prefer_to(I,S,X,Y):-
%  prefer_to(I,S,X,Y),
%  \+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 example 2 of Moore-Repullo(1990).
% 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    */

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)
     )
    ),
   display_domain(_S),
   update_message_file.

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



  %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
  %% 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 as 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).
% extended relations as 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 2 of Moore-Repullo(1990). another elementary coding.
stock_of(mr0,preference,1,s1,[a,c,d,b,z]).
stock_of(mr0,preference,1,s2,[a,d,c,b,z]).
%stock_of(mr0,preference,1,s1,[a,c,d,b,z]).
stock_of(mr0,preference,1,s3,[a,c,d,b,z]).
stock_of(mr0,preference,1,s4,[a,d,c,b,z]).
stock_of(mr0,preference,2,s1,[b,c,d,a,z]).
stock_of(mr0,preference,2,s2,[b,d,c,a,z]).
stock_of(mr0,preference,2,s3,[b,d,c,a,z]).
stock_of(mr0,preference,2,s4,[b,c,d,a,z]).
%
% indifferenceの実現方法:選好種類の追加。prefer_toだけ直せばよい。
% 末尾のzとの比較はいずれも無差別
stock_of(mr0,difference,1,s1,[s,s,s,e,end]).
stock_of(mr0,difference,1,s2,[s,s,s,e,end]).
stock_of(mr0,difference,1,s3,[s,s,s,e,end]).
stock_of(mr0,difference,1,s4,[s,s,s,e,end]).
stock_of(mr0,difference,2,s1,[s,s,s,e,end]).
stock_of(mr0,difference,2,s2,[s,s,s,e,end]).
stock_of(mr0,difference,2,s3,[s,s,s,e,end]).
stock_of(mr0,difference,2,s4,[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.
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 as 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,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,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^(
      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 prefer_to(I,S1,Y,X),
  prefer_to(I,S1,X,Y),
  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), 
       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), 
       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).
    

% -----------------------------------------------------------  %
%%%%%  dictatorship   (almost same as maximal )
% -----------------------------------------------------------  %
% edited : 29 Aug 2002. to be used in roullete in gD and so on.

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 shoud'nt use "scc_defined_state(S,Scc)" instead.
   state(S),(T = S -> true; 
     %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, is'nt 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),
        prefer_to(J,S,Other,C),
        \+prefer_to(J,S,C,Other)
       ).


% -----------------------------------------------------------  %
% Condition D  :
%  checking the domain restriction whether it is near universal.
% -----------------------------------------------------------  %
% 20 Aug 2002. modified 25 Aug 2002.
% reference: Yamato(1992), p.487.

%      %%%%%%%%%%%%%%%%%%%%%%%%%
%      %%%    condition D    %%%
%      %%%%%%%%%%%%%%%%%%%%%%%%%

condition_D(Is,Rs):-
   alternatives(As),
   subset_of_agents(Is,_),
   prefer_profiles(Is,Ss,Rs),
   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),wn([J,S1,B,Lcc]),
      forall((nth1(_L1,Is,J1),J1\=J),
        (
         wn([J,S1,B,Lcc]),lcc([J1,S1,_RJ2],B,As)
        )
      )
     )
   ).


% -----------------------------------------------------------  %
% 社会選択対応  (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]).


% King Solomon's choice function.
scc(ks,s1,[a]).
scc(ks,s2,[b]).



% 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 ud2.
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]).


% pareto corr for ud2.
scc(par,s1,[x]).
scc(par,s2,[x,y]).
scc(par,s3,[x,y]).
scc(par,s4,[y]).
%range(par,[x,y]).

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

gen_test_sccs(SC_tuples,Is,Goals):-
  generate_scc(scc1,SC_tuples),
  tests_for_scc(scc1,Is,Goals).

gen_test_mr(SC_tuples,Is,G3):-
  generate_scc(scc1,SC_tuples),
  (has_MR_property(scc1,Is) -> G3 = mr; G3 = no).

% gen_test_neutral has added: 1 Sep 2002.
gen_test_neutral(SC_tuples,Is,Neu):-
  generate_scc(scc1,SC_tuples),
  (is_neutral(scc1,Is) -> Neu = neutral; Neu = no).

% gen_test_mju has added: 1 Sep 2002.
gen_test_condMju(SC_tuples,Is,[Gm1,Gm2,Gm3,Gm4]):-
  generate_scc(scc1,SC_tuples),
  (condition_mju(scc1,Is,Bx,[yes,yes],[i]) -> Gm1 = mju1; Gm1 = no),
  (condition_mju(scc1,Is,Bx,[yes,yes],[ii]) -> Gm2 = mju2; Gm2 = no),
  (condition_mju(scc1,Is,Bx,[yes,yes],[iii]) -> Gm3 = mju3; Gm3 = no),
  (condition_mju(scc1,Is,Bx,[yes,yes],[iv]) -> Gm4 = mju4; Gm4 = no).


% gen_test_mju has added: 2 Sep 2002.
gen_test_condition_M(SC_tuples,Is,[M1,M2]):-
  generate_scc(scc1,SC_tuples),
  (condition_M(scc1,Is) -> M1 = cnd_M; M1 = no),
  (condition_M2(scc1,Is) -> M2 = cnd_M2; M2 = no).

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

scc_tuple([],0,[]).
scc_tuple([[S,X]|Cr],K,[S|Sc]):-
  scc_tuple(Cr,K1,Sc),
  K is K1 + 1,
  states(Ss),reverse(Ss,Sr),nth1(K,Sr,S),
  subset_of_alt(X,_N1).
  %X \= [].

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

% -----------------------------------------------------------  %
% testing the major properties for scc.
% -----------------------------------------------------------  %
% edited : Aug 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]):-
  scc(F),
  subset_of_agents(Is,_),
  (monotone(F,Is) -> G1 = mm; G1 = no),
  (ess_monotone(F,Is) -> G2 = em; G2 = no),
  (has_MR_property(F,Is) -> G3 = mr; G3 = no),
  (test_irat_n2(F,Is) -> G4 = ir; G4 = no),
  %---------------------------------------------------------%
  ((bad_outcome(Bad,F,Is)) ->BO = bad(Bad); BO = no),
  (nvp(F,Is) -> G5 = nvp; G5 = no),
  (rvp(F,Is) -> G6 = rvp; G6 = no),
  (unanimity(F,Is) -> G7 = unan; G7 = no),
  (has_pareto_property(F,Is) -> G8 = po; G8 = no),
  (has_condorcet_property(F,Is) -> G9 = co; G9 = no),
  (dictatorial(F,Is) -> G10 = dict; G10 = no),
  (neli(F,Is) -> G11 = neli; G11 = no),
  (mlib(F,Is) -> G12 = mlib; G12 = no),
  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 as 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),
      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),
   \+ 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, resp., in 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 as 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., 
% 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),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),prefer_to(J,S,A,B)),Jas),
   bagof(J,(member(J,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 the 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),
       \+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),
     \+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)
     ),
   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),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.

/*   --------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 )----------*/

is_neutral(F,Is):-
   scc(F),
   subset_of_agents(Is,_),
   forall( % -----forall (1)---------
     (
      poa(_,PoA),
      permutated_prefer_profile(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)---------
   ).

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






% -----------------------------------------------------------  %
% 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(2001),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).


% お詫び。
% 以下は試作の段階状態です。
%  early morning, 21 Aug 2002.


    %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
    %%%   Condition μ: i,ii,iii  μ2: i〜iv %%%
    %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% added: Aug 2002.

% By Moore-Repullo(1990) and independently Dutta-Sen(1991).
% Also see Sjostrom(1991), pp.334-5.
% 21-3 Aug 2002


condition_mju(F,Is,Bx,[GoBx,GoCx],Mju):-
   subset_of_agents(Is,_),
   scc(F),
   (GoBx=yes -> set_B_star(Bx,_,Is,F);true),
   subset_of_alt(Bx,_),  % <-- note! it should be done after set_B_star/4.
   subset_of(Mju,_,[i,ii,iii,iv]),   wn([bx,Bx,mju,Mju]),
   forall(
    (
     state(S), agent(J), 
     member(J,Is), preference(J,S,R),
     alternative(A), scc(F,S,V),member(A,V)
     ,tab(1),wn([[agent_state_pref,J,S,R],A])
    ),
    (
     (GoCx=yes -> set_C_star(Cx,_,[[J,S,R],A,Bx],Is,F);true),
     subset_of_alt(Cx,_),member(A,Cx),
     preference(J,S,R),
     lcc([J,S,R],A,Lcc),
     subset(Cx,Lcc),
     subset(Cx,Bx),tab(2),wn([cx_A,Cx,A,lcc,Lcc,bx,Bx]),
     % sub-conditions of mju and mju2 in Moore-Repullo(1990)
     forall(
      (member(M,Mju),M\=iv),
      (
       sub_condition_of_mju(M,F,Is,[J,A,Bx,Cx])
       ,tab(3),wn([ok_mju,M])
      )
     ),
     (member(iv,Mju)->
       (sub_condition_of_mju(iv,F,Is,[J,A,Bx,GoCx])
       ,tab(3),wn([ok_mju,iv]));true
     )
    )
   ).


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


    %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
    %%%   subsidiary conditions for μ and μ2   %%%
    %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

% see Sjostrom(1991).

sub_condition_of_mju(i,F,Is,[J,A,_Bx,Cx]):-
% this corresponds to Moores-Repullo's condition, mju (i), monotonicity. 
   scc(F),
   subset_of_agents(Is,_),
   agent(J),member(J,Is),
   alternative(A),
%   subset_of_alt(Bx,_), 
   subset_of_alt(Cx,_), 
   forall(
     (
      scc_defined_state(S,F),
      prefer_profile(Is,S,Rs),
      tab(4),wn([profile,Rs,S]),
      forall(
         member(J1,Is),
        (
         preference(J1,S,R1),
         lcc([J1,S,R1],A,Lcc),subset(Cx,Lcc)
         ,tab(5),wn([A,J1,S,lcc,Lcc,includesCx,Cx])
        )
      )
     ),
     (
      scc(F,S,V), write([scc,V]),member(A,V),tab(6),wn([A,in_scc])
     )
   ).

sub_condition_of_mju(ii,F,Is,[J,_A,Bx,Cx]):-
% this corresponds to Moores-Repullo's condition, mju (ii), rvp. 
   scc(F),
   subset_of_agents(Is,_),
   agent(J),member(J,Is),
   subset_of_alt(Bx,_), 
   subset_of_alt(Cx,_), 
   forall(
    (
     scc_defined_state(S,F),
     prefer_profile(Is,S,Rs),
     tab(4),wn([profile,Rs,S]),
    %----
     member(C0,Cx), 
     preference(J,S,R),
     lcc([J,S,R],C0,Lcc), subset(Cx,Lcc),
     tab(5),wn([C0,J,S,lcc,Lcc,includesCx]),
    %----
     forall((member(J1,Is), J1 \= J),
       (
        preference(J1,S,R1),
        lcc([J1,S,R1],C0,Lcc1),subset(Bx,Lcc1)
        ,tab(6),wn([C0,J1,S,lcc,Lcc1,includesBx])
       )
     )
    ),
    (
      scc(F,S,V),member(C0,V),tab(6),wn([C0,in_scc])
    )
   ).

sub_condition_of_mju(iii,F,Is,[_J,_A,Bx,_Cx]):-
% 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,Rs,S]),
    %----
     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])
    )
   ).



sub_condition_of_mju(iv,F,[J1,J2],[_J,_A,Bx,GoCx]):-
   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)
     ,tab(4),wn([for_scc_pair,[J1,S1,A],[J2,S2,B]])
    ),
    (
     % ----- the 'self-selection constraint' in the term of Dutta-Sen(1991).
     make_set_Cx_for([[J1,S1,R1],A],Cx1,Bx,[J1,J2],F,GoCx),
     make_set_Cx_for([[J2,S2,R2],B],Cx2,Bx,[J1,J2],F,GoCx),
     intersection(Cx1,Cx2,MR),
     % -----
     member(Phi,MR),tab(5),wn([mr,Phi,in_C1xC2,MR]),
     forall(
       (
        lcc([J1,Sp,_R1p],Phi,Lp1),
        lcc([J2,Sp,_R2p],Phi,Lp2),
        subset(Cx1,Lp1),
        subset(Cx2,Lp2),tab(6),write([for_lcc_pair,Lp1,Lp2])
       ),
       (scc(F,Sp,Vp),member(Phi,Vp),tab(2),wn(in_scc)) 
     )
    )
   ).

make_set_Cx_for([[J,S,R],A],Cx,Bx,[J1,J2],F,GoCx):-
     member(J,[J1,J2]),
     (GoCx=yes -> (
        set_C_star(Cx,_,[[J,S,R],A,Bx],[J1,J2],F)
     );true),  %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).


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

mre(Y,F,[[X1,X2],[J1,J2],[S1,S2],[R1,R2]],[Cx1,Cx2],T):-
    % Of cause, you cannot use 'subset_of_alt([X1,X2],2)' instead.
    %alternative(X1),
    %alternative(X2),
    % These are of the definition, and no harm with or without them, 
    % but it is better for you to omit these alternative/1s in order 
    % for the computational efficiency. 
    %
    (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]]),read(_U));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),
    % make_set_Cx_for([[J1,S1,R1],X1],Cx1,Bx,[J1,J2],F,yes),
    % make_set_Cx_for([[J2,S2,R2],X2],Cx2,Bx,[J1,J2],F,yes),
     intersection(Cx1,Cx2,MR),
    (T=yes->(tab(6),wn([cx1,Cx1,cx2,Cx2,mre,MR]));true),
     alternative(Y),
     member(Y,MR),
    (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).


    %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
    %%%    Conditions M and  M2   %%%
    %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% see Sjostrom(1991), p.335.

condition_M(F,Is):-
   subset_of_agents(Is,_),
   scc(F),
   forall(
     (
      alternative(A),
      state(S),
      member(J,Is),
      preference(J,S,R),
      scc(F,S,C),member(A,C),  wn([[J,S,R],A])
     ),
     (
      set_C_star(Cx,_,[[J,S,R],A,Bx],Is,F),
      member(A,Cx),
      condition_mju(F,Is,Bx,[yes,yes],[i])
     )
   ).


condition_M2(F,[J1,J2]):-
   subset_of_agents([J1,J2],2),
   scc(F),
   forall(
     (
      alternative(A),
      state(S),
      member(J,[J1,J2]),
      preference(J,S,R),
      scc(F,S,C),member(A,C),  wn([[J,S,R],A])
     ),
     (
      set_C_star(Cx,_,[[J,S,R],A,Bx],[J1,J2],F),wn(Cx),
      member(A,Cx),
      condition_mju(F,[J1,J2],Bx,[yes,yes],[i,iv])
     )
   ).



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


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]).

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

   % cut (!) above means that the message Msg can be enumerated.


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.



/*  verify all messages */

update_message_file:-
   wn(' The domain model has changed.'),
   write(' Will you update message file?(y/n)'),
   read(U),
   U=y->(
	write('game_form?'),read(GF),
	write('scc?'),read(Scc),
	write('agents?'),read(Is),
	verify_messages(GF,Scc,Is,_E)
   );true.


verify_messages(GF,Scc,Is,E):-
   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(output_file_open),
   write('ファイルに書出しています。'),nl,
   forall(
     mtest(GF,Scc, M,Is),
    (
     G=..[GF,P,Scc],
     (mechanism(G,E,M,C)->true;(P=nul,C=non)),%wn([M,G,C]),
     write(Strm,mechanism(G,M,C)),wn(Strm,'.')
    )
   ),
   close(Strm).



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_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 gM, the Maskin-Vind mechanism.
% -----------------------------------------------------------  %
% edited from: Sep 2001.
% modified by using maplist: 24 Aug 2002.
% note:
% About this construction of messagge space and its reducability,
% see Saijo(1988).



% message profile for N agents in mechanism gM.
mtest(gM, Scc,[],[],Is):-
    scc(Scc),
    subset_of_agents(Is,_N),!.

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

mtest(gM, Scc,Msg,Is):-mtest(gM, Scc,Msg,Is,Is).


/*  pending
mtest(gM,Scc,Msg,Is):-
    scc(Scc),
    subset_of_agents(Is,N),
    gM_profile(Scc,Is,Msg),
    length(Msg,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 profile for 2 or N agents in mechanism gMR2, gMR.
% -----------------------------------------------------------  %
% reference: Moore-Repullo(1990).
% 25 Aug 2002.


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

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


% -----------------------------------------------------------  %
% message profiles which has fixed all-0-integer game 
% -----------------------------------------------------------  %

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,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).



% -----------------------------------------------------------  %
% truth-telling strategy
% -----------------------------------------------------------  %
% 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),!.




% -----------------------------------------------------------  %
% message profiles in gM
% -----------------------------------------------------------  %
% modified: 24 Aug 2002. it is useless now.


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

% modified: 04 Sep 2002.
/*  gM_profile has abolished because of state-dependence.
gM_profile(F,Is,Prf):-
    scc(F),
    subset_of_agents(Is,_N),
    my_maplist(maskin(F,Is,_S),Is,Prf).
*/
tt_gM_profile(F,Is,S,Prf):-
    scc(F),
    subset_of_agents(Is,_N),
    state(S),
    my_maplist(maskin(F,Is,S),Is,Prf).


message(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),
         scc(F,S,V),
         member(A,V)
        )
     ;  prefer_profile(Is,Rs)
    ),
   alternative(A).
   % for delayed execution, the integer part to be open yet.
   %,asc_nnseq(Aseq,N),member(Z,Aseq).

messages(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).


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, shoud'nt use "state(S)" instead.
    prefer_profile(Is,S,R),
    scc(F,S,V),
    alternative(A),member(A,V),
    alternative(B).
  % delayed resolution for the integer part: 
  %  it will remains unspecified until the roulette has invoked.
  %  asc_nnseq(Aq,N),
  %  member(Z,Aq).

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):-
    M2=(R,A,B,Z,Obj),
    M=(R,A,B,Z),
    mr_msg([J1,J2],F,J,M),
    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 sole testing for the mechanism gM, N=3.

test_gM(Scc,P,M,C,Is):-
    E = environment([Is,_Ss,_As],[3,_K,_L],_Rs),
    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(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).
*/


% -----------------------------------------------------------  %
% the roulette of modulo N
% -----------------------------------------------------------  %
% added: Aug 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]).

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


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

% a utility for extracting integer elements from message profile

last_part_of_mtest(Msg,[GF,Scc,Is],Zs):-
    mtest(GF,Scc,Is,Msg),
    findall(Z,(member(M,Msg),last(Z,M)), Zs).


% -----------------------------------------------------------  %
% The canonical Mechanism for 3 or N agents. 
% (Maskin-Vind mechanism, modified by using Ess):
% -----------------------------------------------------------  %
% the earlier version only for 3 players has created 29-30 Sep 2001.  
% gD, Danilov's two-person mechanism added 23 Jan 2002.
% and modified Feb 2002,May 2002, and by using ess, Aug 2002.




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


game_form(gM(2,Scc),E,Msg,[C]):-
      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)] -> (J is 1,true);
  %  Msg = [(R2,C2,Z1),(R1,C1,Z2),(R2,C2,Z3)] -> (J is 2,true);
  %  Msg = [(R2,C2,Z1),(R2,C2,Z2),(R1,C1,Z3)] -> (J is 3,true)),
  % 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),
    % 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),!,
     %
      state(S),
      prefer_profile(Is,S,R2),
      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。

game_form(gM(3,_Scc),E,Msg,[C]):-
    E = environment([_Is,_Ss,_As],[N,_K,_L],_Rs),
    length(Msg,N),
    setof((R,X,0),Z^member((R,X,Z),Msg),Mx),%wn([m,Mx]),
    length(Mx,Lm),  Lm > 2, 
    !,
   % Msg = [(_,C1,Z1),(_,C2,Z2),(_,C3,Z3)],!,
   % SumZ is (Z1 + Z2 + Z3),
   %
    roulette(Jd,_Zs,Is),    % delayed execution
    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.


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,Y),
    roulette(Jd,[Z1,Z2],[J1,J2]),
    member(C,Y),
    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 gMR2 for N=2. %%%
% -----------------------------------------------------------  %

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),
       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.

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

game_form(gMR(2,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)),[M1,M2]),
      member((R1,A1),[M1,M2]),
      MJ = (R1,A1,B1,_O1),  % disagreed message.
      counter(1,MJ,Msg),   % a necessary condition of unilateral deviator.
      % the semi-agreed component.
      member((R,A),[M1,M2]),(R1,A1)\=(R,A),
      bagof((R,A),Y^Z^(member((R,X,Y,Z),Msg)),Agree),
      length(Agree,N1),
      N1 is N - 1, 
     !,%
      nth1(K,Msg,MJ),
      nth1(K,R,RJ),
      nth1(K,Is,J),   % the deviator has specified.
      preference(J,S,RJ),  % estimated state from agreed profile.
      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. 

game_form(gMR(3,_Scc),E,Msg,[C]):-
    E = environment([_Is,_Ss,_As],[N,_K,_L],_Rs),
    length(Msg,N),
    setof((R,X),Y^Z^member((R,X,Y,Z),Msg),Mx),%wn([m,Mx]),
    length(Mx,Lm),  Lm > 2, 
    !,
    roulette(Jd,_Zs,Is),    % delayed execution
    nth1(K,Is,Jd),
    nth1(K,Msg,(_R,_A,C,_Z)).



%%%% end of rules.



% consistency check for any game form.
game_form(_,E,Msg,[]):-
      E = environment([Is,_,_],[N,_,_],_),
      length(Is,N1),
      length(Msg,N2),
      \+sort([N,N1,N2],[N]),
      wn(this_message_is_inconsistent_and_cannnot_processed),!.



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

% -----------------------------------------------------------  %
   %%%  equilibrium outcomes correspondence  %%
% -----------------------------------------------------------  %
% added: 25 Aug 2002. modified: 31 Aug 2002.

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(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(C,S,M,G,h0,E,Is,yes).




%%%%%  several tests for constructing nash equilibrium messege
% added: Aug 2002.
 
test_abn(M,D,[P1s,Czs,Lcc,Br]):-
    D=[([x],0),([x,y],0)],
    test_nash(gD,[x,s2],[1,udd1,h0],D,[1,2],_F),
    best_response([udd1,_E,[1,2]],[gD,s2,x,D],2,[P1s,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(gD,[y,s4],[1,umd5,h0],D,[1,2],F).


% -----------------------------------------------------------  %
%%% checking Nash outcomes with zero-normalized messages. 
% -----------------------------------------------------------  %
% modified: 31 Aug 2002.

test_nash(GF,[C,S],[P,Scc,H],Msg,Is,Result):-
    E = environment([Is,_,_],[N,_,_],_),
    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. 
   % find a legitimate outcome for nash/6 to reduce backtrack.
   % frame of discernment: verify game forms sequentially!!
    subset_of_agents(Is,N),
   % xxx->  generate a 0-integer message profile to yield C.
    alternative(C),
    mtest_z0(GF,Scc, Msg,Is),     %wn(4),trace,
    restrict_forms(GF,P),         %wn([GF,P]),
    mechanism(G,Msg,[C]),
    state(S),
    nash(C,S,Msg,G,H,E,Is,Result).

test_nash(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. 


% manual restrictions for the forms in order for computational efficiency.
restrict_forms(GF,P):-
    mechanisms(Mxs),
    member(GF,Mxs),
    (GF = gM -> member(P,[1,2]);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,gMR]) -> (member(P,[1,2,3]),N = 2);true),
    (member(GF,[gMR2]) -> (member(P,[1,2,3,4,5]),N = 2);true).


% -----------------------------------------------------------  %
%%% 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].
%

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]).

true_state(init).


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


br_result(dummy).

save_br_results(Is,E,[GF,Scc,S,C,P,Msg]):-
    forall( 
      member(I,Is),
      (
       BrRecord = [Br,S,C,I,GF,P,Scc,Is,Msg,P1s,Czs,Lcc],
       (br_result(BrRecord)->true;
	(
         best_response([Scc,E,Is],[GF,S,C,Msg],I,[P1s,Czs,Lcc],Br),
         assert(br_result(BrRecord))
	)
       ),
       write_nash(I,[P1s,Czs,Lcc],Br)
      )
    ).

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



br_member(0,no).

nash0(C,S,Msg,G,H,E,Is,Result):-
    E = environment([Is,_,_],[_N,_,_],_),
    E,
    G =.. [GF,P,Scc],
    reversions(V),    member(H,V),
    scc(Scc),state(S),
 %  update_state(S),   % update_state should be done before mechanism.
    alternative(C),    % alternative should be done before mtest.
    mtest(GF,Scc, Msg,Is),%write(m),
    mechanism(G,Msg,[C]),
   % !,
    nl,wn(' Now checking whether the message profiles is a NE. '),
    write_message(S,C,P,Msg,Scc),
    abolish(br_member,2),
    forall( member(I,Is),
       (
         BrRecord = [Br,S,C,I,GF,P,Scc,Is,Msg,P1s,Czs,Lcc],
         (
	  br_result(BrRecord)->true;
	   (
            best_response([Scc,E,Is],[GF,S,C,Msg],I,[P1s,Czs,Lcc],Br),
            assert(br_result(BrRecord))
	   )
	 ),
         assert(br_member(I,Br)),
         write_nash(I,[P1s,Czs,Lcc],Br)
       )
    ),
    setof(J,br_member(J,yes),Br_members),
    write_nash_equilibrium(Br_members,Is),
    ( Br_members = Is -> Result=yes ; Result=no).

% -----------------------------------------------------------  %
%%% checking best response via Lcc. 
% -----------------------------------------------------------  %
% modified: 31 Aug 2002.

best_response([Scc,E,Is],[GF,S,C,Msg],I,[P1s,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('wait..'),
  % the mutation set is included in the lower contuor set 
  % and so any unilateral deviation can not improve the Nash outcome.
    findall((P1,Cz),
       %Mz^(
       ( mutate(GF,Scc,I,Is,Msg,Mz),
        alternative(Cz),
        member(P1,Ps),
        G =.. [GF,P1,Scc],
        mechanism(G,Mz,[Cz])
        %,wn([G,Mz,Cz])
       ),
       PCzs1),
    sort(PCzs1,PCzs),
    findall(P1,Cz^(member((P1,Cz),PCzs)),P1s1),
    sort(P1s1,P1s),
    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.

mutate(GF,Scc,J,Is,Msg,Mz):-
   subset_of_agents(Is,N),
   length(Is,N),
   nth1(Nj,Is,J),
   mtest(GF, Scc,Msg,Is),length(Msg,N),
   nth1(Nj,Msg,MJ),
   mtest(GF, Scc,Mz,Is),length(Mz,N),
   nth1(Nj,Mz,MJz),
   % We have need to permit null-mutation case 
   % for the cases of roulette. 
   MJz \= MJ,
%
   subtract(Is,[J],Isz),
   forall(member(K,Isz),
    (
     nth1(Nk,Is,K),
     nth1(Nk,Msg,Mk),
     nth1(Nk,Mz,Mk)
    )
   ).


% some test routines


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

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


% -----------------------------------------------------------  %
%  display results (or output to file)  %%%%%%%%%%%%%%%
% -----------------------------------------------------------  %

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 is '),!,
    forall(member(M,Msg), 
      (tab(5),wn(M))),
    (current_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,[P1s,Czs,Lcc],Result):-
    nl,
    write(' agent='),write(I),
    write(',P1s='),write(P1s),
    write(',Czs='),write(Czs),
    write(',Lcc='),write(Lcc),
    ( Result=yes
    -> write('  ')
    ;  write('  ')),
    (current_stream(_File,write,Strm) 
    -> write_nash(Strm, I,[P1s,Czs,Lcc],Result)
    ; true),
    !.

write_nash(Strm, I,[P1s,Czs,Lcc],Result):-   
  %  current_stream(_File,write,Strm),
    nl(Strm),
    write(Strm,' agent='),write(Strm,I),
    write(Strm,',P1s='),write(Strm,P1s),
    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),
    (current_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,P1s,Czs,Lcc,Br],Br_Results),
       write_nash(I,[P1s,Czs,Lcc],Br))),!.


%br_result([Br,S,C,I,GF,P,Scc,Is,Msg,P1s,Czs,Lcc])

save_br_results(File,Strm):-
    br_result(BR),nth1(5,BR,GF),nth1(7,BR,Scc),
    \+ current_stream(_File,write,Strm),
    wn('save to file as follows:'),
   % listing(br_result),
    open_br_file(Scc,GF,File,Strm),
    write_br_results(File,Strm).

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,IN),write(Strm,', '),
    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),
    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
    ).

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.').







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

% 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).



test_impl(GF,Scc,Is,N,Summary):-
    trim_stacks,
    ( \+ (scc(Scc,_,_))
    -> (wn('no such Scc.'),fail);true),
    subset_of_agents(Is,N),\+ member(N, [0,1]),
    open_output_file(Strm,Scc),
    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,Strm),
    check_off_scc(GF,Is,Scc,H,Strm),
    init_state,
    collect_statistics(Stat2),
%
    write_summary(Summary),
    write_statistics(Stat1,Stat2),
    close_output_file(Strm),
    write('save br_results? (yes)'),read(Save),
    (Save = yes -> save_br_results(_,_);true),
    wn('end'),
    trim_stacks.


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).
close_output_file(Strm):-close(Strm).


check_on_scc(GF,Is,F,H,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(GF,[O,S],[P,F,H],_Msg,Is,yes)->Yes=yes;Yes=no),
       update_summary([S,O,Yes,in])
     )),nl,  nl(Strm),!.

check_off_scc(GF,Is,F,H,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.
       test_nash(GF,[O,S],[_P,F,H],_M,Is,yes)->No=yes;No=no),
       update_summary([S,O,No,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])
    ->disp_mr_ir(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.

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])
    ->disp_mr_ir(Strm,Scc,Is);true),
    !.
disp_mr_ir(Strm,Scc,[I,J]):-
    (has_MR_property(Scc,[I,J])->wn(Strm,'has Moore-Repullo property.');
     wn(Strm,'does not have Moore-Repullo property.')),
    (test_irat_n2(Scc,[I,J])->wn(Strm,'is individually-rational.');
     wn(Strm,'is not individually-rational.')).

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

test_for_model(Strm,Scc,Is):-
   tests_for_scc(Scc,Is,G),
   nl,write('other tests for this model:'),wn(G),
  (var(Strm)->true;
   (
    nl(Strm),
    write(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,in])
     )),nl,
    forall((state(S),alternative(O),scc(F,S,D),\+member(O,D)),
     (
       update_summary([S,O,default,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)).


write_summary(Summary):-
    summary(Summary),
    current_stream(_File,write,Strm),
    nl(Strm),
    wn('Result Summary'),
    wn(Strm,'Result Summary'),
    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,externals,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(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])
      )
    ),!.



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


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


:-welcome.%,init_prompt.
   % edit_history,init_prompt, reference_list.



% -----------------------------------------------------------  %
%  END %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% -----------------------------------------------------------  %


/* trash 


pairwise_permutate(L1,L2,Len,[K,J],[X,Y]):-
   permutate(L1,L2,Len),
   nth1(K,L1,X),
   nth1(K,L2,Y),
   nth1(J,L1,Y),
   nth1(J,L2,X).

permutate(L1,L2,Len):-
   sort(L1,L),
   ordering(L1,L,Len),
   ordering(L2,L,Len).



% ud n=2 m=3 another implementation, but... 以下はうまくいかず。Abendする。
% the universal domain for 3 outcomes and two agents
stock_of(ud23_0,preference,1,s(1,S2),[x,y,z]):-member(S2,[1,2,3,4,5,6]).
stock_of(ud23_0,preference,1,s(2,S2),[x,z,y]):-member(S2,[1,2,3,4,5,6]).
stock_of(ud23_0,preference,1,s(3,S2),[y,z,x]):-member(S2,[1,2,3,4,5,6]).
stock_of(ud23_0,preference,1,s(4,S2),[y,x,z]):-member(S2,[1,2,3,4,5,6]).
stock_of(ud23_0,preference,1,s(5,S2),[z,y,x]):-member(S2,[1,2,3,4,5,6]).
stock_of(ud23_0,preference,1,s(6,S2),[z,x,y]):-member(S2,[1,2,3,4,5,6]).
stock_of(ud23_0,preference,2,s(S1,1),[x,y,z]):-member(S1,[1,2,3,4,5,6]).
stock_of(ud23_0,preference,2,s(S1,2),[x,z,y]):-member(S1,[1,2,3,4,5,6]).
stock_of(ud23_0,preference,2,s(S1,3),[y,z,x]):-member(S1,[1,2,3,4,5,6]).
stock_of(ud23_0,preference,2,s(S1,4),[y,x,z]):-member(S1,[1,2,3,4,5,6]).
stock_of(ud23_0,preference,2,s(S1,5),[z,y,x]):-member(S1,[1,2,3,4,5,6]).
stock_of(ud23_0,preference,2,s(S1,6),[z,x,y]):-member(S1,[1,2,3,4,5,6]).
% extended relations as for above example, optionally.
stock_of(ud23_0,difference,_,_,[s,s,end]).


has_MR_property(F,[J1,J2]):-
    scc(F),
    two_person([J1,J2]),
/*
    max_blocking(B1,[J1,_S1,_R1],[J1,J2],F),
    max_blocking(B2,[J2,_S2,_R2],[J1,J2],F),
    wn([for,[J1,J2],maximal_blockings,B1,B2, under_scc,F]),
*/
    forall(
      unblocked_pair([X1,X2],[J1,J2],F),
     (%nl,wn([X1,X2]),
      scc(F,S,C),
      member(A,C),
/*
      maximal(A,X1,[J1,S,_R1]),
      maximal(A,X2,[J2,S,_R2]),write([max,A]),
      member(A,C),write(yes),nl
      lcc([J1,S,_R1],A,X1),wn([lcc1,L1]),
      lcc([J2,S,_R2],A,X2),wn([lcc2,L2]),
*/
      is_MR_elements(MR,[X1,X2],[J1,J2],F),member(A,MR),MR\=[],
      wn([state,S,scc,C,'MRs',MR,unblocked_pair,[X1,X2]])
     )
   ).

condition_mju2(F,[J1,J2],Bx,[GoBx,GoCx]):-
   subset_of_agents([J1,J2],2),
   scc(F),
   (GoBx=yes -> set_B_star(Bx,_,[J1,J2],F);true),
   subset_of_alt(Bx,_),  % <-- note! it should not be done before set_B_star/4.
   condition_mju(F,[J1,J2],Bx,[GoBx,GoCx],[i,ii,iii]),wn('mju ok'),
   wn('It satisfies mju i,ii,and iii.'),
   wn(' To cotinue, type any key, period, and enter.'),
   read(_User),
   forall(
    (
     agent(J), member(J,Is),
     state(S), preference(J,S,R),
     alternative(A),
     scc(F,S,V),member(A,V),  tab(1),wn([[agent_state_pref,J,S,R],A])
    ),
    (
     (GoCx=yes -> set_C_star(Cx,_,[[J,S,R],A,Bx],Is,F);true),
     subset_of_alt(Cx,_),member(A,Cx),
     preference(J,S,R),
     lcc([J,S,R],A,Lcc),
     subset(Cx,Lcc),
     subset(Cx,Bx),tab(2),wn([cx_A,Cx,A,lcc,Lcc,bx,Bx]),
     % only one sub-conditions of mju2 is iv.
     sub_condition_of_mju(iv,F,Bx,[J1,J2],GoCx),tab(3),wn([ok_mju,iv])
    )
   ).


a_profile([Pred,Cnd2],Is,Prof):-
    subset_of_agents(Is,_N),
    state(S),
    goal_for_maplist([Pred,Cnd1,Cnd2],Is,M),
    Goal=..[Pred|Cnd2],
%    wn(Goal),trace,
    my_maplist(Goal,Is,Rs).

goal_for_maplist([suh,J,S,B]),S,B).
goal_for_maplist([Pred|Cnd1],C,Map):-
    Goal1=..[Pred|Cnd1],
    Goal1,
    subset_of(Cnd2,_,Cnd1),
    Goal2=..[Pred|Cnd2],
    subset_of([C,Map],2,Cnd1).




*/



return to front page.