/*======= prolog code for dynamic check =======*/


/*
 *  permissions (static) 
 */ 
permission(subsender, perm(subs, subscribe)).
permission(subsender, perm(sender, receive)).
permission(subs, perm(fors, forward)).
permission(fors, perm(subs, checklogin)).
permission(subreceiver, perm(subs, subscribe)).
permission(subreceiver, perm(receiver, receive)).


/*
 *  delegation (static) 
 */ 
delegate(subsender, perm(sender, receive),[forwarder]).
delegate(subs, perm(fors, forward),[instantmessenger]).
delegate(subreceiver, perm(receiver, receive),[forwarder]).


/*
 *  class mapping 
 */ 
isOf(subsender, subscriptionclient).
isOf(subs, subscriptionserver).
isOf(receiver, instantmessenger).
isOf(fors, forwarder).
isOf(sender, instantmessenger).
isOf(subreceiver, subscriptionclient).


/*
 *  class needing no permissions 
 */ 





 :- dynamic(noPermission/3).
 


/*
 *  messages (dynamic) 
 */ 

msg(0, subsender, subs, 'subscribe', [perm(subs , subscribe)], [] ).

msg(1, subreceiver, subs, 'subscribe', [perm(subs , subscribe)], [cert(subreceiver, null,perm(receiver, receive), null, -1, -1)] ).

msg(2, subs, subsender, 'subscriptionConfirmation', [], [cert(subs, null,perm(fors, forward), null, -1, -1)] ).

msg(3, subsender, sender, 'create', [], [cert(subs, null,perm(fors, forward), null, -1, -1)] ).

msg(4, sender, fors, 'forward', [perm(fors , forward)], [] ).

msg(5, fors, subs, 'checkLogin', [perm(subs , checklogin)], [] ).

msg(6, fors, subs, 'checkLogin', [perm(subs , checklogin)], [] ).

msg(7, subs, fors, 'true', [], [cert(subreceiver, null,perm(receiver, receive), null, -1, -1)] ).

msg(8, subreceiver, receiver, 'create', [], [] ).

msg(9, fors, receiver, 'receive', [perm(receiver , receive)], [] ).

/*
 * helpclauses: addEntry( List1, List2, ListOut )  
 */

addEntry( [] , EntryList, EntryList ).
addEntry( EntryList, [] , EntryList ).
addEntry( [X|L1] , L2 , [X|L3] ) :- addEntry(L1, L2, L3).

/*
*:- dynamic hasCert/2.
*:- dynamic usedCert/1.
 */

 
:- dynamic(hasCert/2).
:- dynamic(usedCert/1).

/*
 *  helpclauses: isElement( Element , List )
 */

isElement( Element , List ):- addEntry( _ , [Element|_], List).

/*
 *  helpclauses: allElements( ElementList , List )
 */

allElements( [], _).

allElements( [First|Rest], List):-
	isElement(First, List),
	allElements( Rest, List).

/*
 *   caller has all permissions needed for one message
 */

hasAllPermissions(_, _, _,_ , []).

hasAllPermissions(Step, Sender, Object, M, [P_First|P_Rest]):-
	permission(Sender, P_First),
	hasAllPermissions(Step, Sender, Object, M, P_Rest).

hasAllPermissions(Step, Sender, Object, M, [P_First|P_Rest]):-
	hasCert(Sender, cert(E, D, P_First, _, V, Sq)),
	canUseCert(Step, Sender, cert(E, D, P_First, _, V, Sq)),
	hasAllPermissions(Step, Sender, Object, M,  P_Rest).

hasAllPermissions(_, Sender, Object, Message, _):-
	isOf(Sender, Class),
	noPermission(Message, Object, Class).

	
/*
 * GNU- Prolog syntaxclauses
 */

not(X) :-
	\+ X.
	
assert(A) :-
   assertz(A).	


	
	
/*
 *   object can make use of a cert; cert is marked after being used
 *   certificate will be marked as used, if sequence number != -1, so that 
 *   reusing is not possible.
 */

canUseCert(Step, Sender, cert(E, Sender, P, _, V, Sq)):-
	permission(E, P), (Step =< V; V == -1) ,

	((not(usedCert(cert(E, Sender, P, _, V, Sq))),
	assert(usedCert(cert(E, Sender, P, _, V, Sq))));
	Sq == -1).

canUseCert(Step, Sender, cert(E, null, P, Class, V, Sq)):-
	permission(E, P),	
	delegate(E, P, DelegationList),
	isElement(Class, DelegationList),
	isOf(Sender, ClassX),
	isElement(ClassX, [Class]),
	(Step =< V; V == -1),
	((not(usedCert(cert(E, null, P, Class, V, Sq))),
	assert(usedCert(cert(E, null, P, Class, V, Sq))));
	Sq == -1).

/*
 *  one specific certificate may be sent.
 */

sendCert(Sender, Receiver, Cert):-			
	hasCert(Sender, Cert),
	assert(hasCert(Receiver, Cert)),
	write(Sender), write(' can send '), write(Cert), 
     write(' to '), write(Receiver), write('\n').

sendCert(Sender, Receiver, cert(Sender, null, P, Class, V, Sq)):-
	permission(Sender, P),
	delegate(Sender, P, DelegationList),
	isElement(Class, DelegationList),
	assert(hasCert(Receiver, cert(Sender, null, P, Class, V, Sq))),
	write(Sender), write(' is able to create '), 
	write(cert(Sender, null, P, Class, V, Sq)),
	write(' and to send it to '), write(Receiver), write('\n').

sendCert(Sender, Receiver, cert(Sender, Delegat, P, C, V, Sq)):-
	permission(Sender, P),
	delegate(Sender, P, _),	
	assert(hasCert(Receiver, cert(Sender, Delegat, P, C, V, Sq))),
	write(Sender), write(' is able to create '), 
	write(cert(Sender, Delegat, P, C, V, Sq)),
	write(' and to send it to '), write(Receiver), write('\n').

/*
 *  all certificates in one message will be sent as far as possible
 */

sendAllCerts(_, _, _, []).

sendAllCerts(Step, From, To, [F_Cert|Rest]):-
	sendCert(From, To, F_Cert),
	sendAllCerts(Step, From, To, Rest).

sendAllCerts(Step, From, To, [F_Cert|Rest]):-
	not(sendCert(From, To, F_Cert)),
	sendAllCerts(Step, From, To, Rest),
	write('ERROR: '),
	write(From), write(' is not able to send '),
	write(F_Cert), write(' to '), 
	write(To), write('\n').

/*
 *  program
 */ 
run(Steps):- run(0,Steps).

run(Step, MaxSteps):- Step < MaxSteps,
	msg(Step, Sender, Receiver, Name , P_List, C_List),

	hasAllPermissions(Step, Sender, Receiver, Name, P_List),
	sendAllCerts(Step, Sender, Receiver, C_List),	

	write(Sender), write(' can send message '), 
	write(Name), write(' to '), write(Receiver), write('\n'),
	IPlus1 is Step + 1, run(IPlus1, MaxSteps).

run(Step, MaxSteps):- Step < MaxSteps,
	msg(Step, Sender, Receiver, Name , P_List, C_List),
	not(hasAllPermissions(Step, Sender, Receiver, Name, P_List)),
	sendAllCerts(Step, Sender, Receiver, C_List),	
	write('ERROR: '),
	write(Sender), write(' can not send message '), 
	write(Name), write(' to '), write(Receiver), write('\n'),
	IPlus1 is Step + 1, run(IPlus1, MaxSteps).

run(Step, MaxSteps):- Step < MaxSteps,
	msg(Step, Sender, Receiver, Name , P_List, C_List),
	hasAllPermissions(Step, Sender, Receiver, Name, P_List),
	not(sendAllCerts(Step, Sender, Receiver, C_List)),
	write(Sender), write(' can send message '), 
	write(Name), write(' to '), write(Receiver), write('\n'),
	IPlus1 is Step + 1, run(IPlus1, MaxSteps).

run(Step, MaxSteps):- Step < MaxSteps,
	msg(Step, Sender, Receiver, Name , P_List, C_List),
	not(hasAllPermissions(Step, Sender, Receiver, Name, P_List)),
	not(sendAllCerts(Step, Sender, Receiver, C_List)),
	write('ERROR: '),
	write(Sender), write(' can not send message '), 
	write(Name), write(' to '), write(Receiver), write('\n'),
	IPlus1 is Step + 1, run(IPlus1, MaxSteps).

run(Step, MaxSteps):-
	Step < MaxSteps,
    not(msg(Step, _, _, _, _,_ )),
	IPlus1 is Step + 1, run(IPlus1, MaxSteps).

run(MaxSteps, MaxSteps).

run:-run(0,12).