%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%% SOME EXAMPLES
num(0).
num(s(X)) :- num(X).
sum(X,0,X).
sum(X,s(Y),s(Z)) :- sum(X,Y,Z).
automata([X|T],S) :-
delta(S,X,S1),
automata(T,S1).
delta(s0,a,s1).
delta(s1,b,s2).
delta(s2,c,s3).
delta(s2,e,s0).
delta(s3,d,s0).
inf_list(X,[X|L]) :-
inf_list(s(X),L).
%%%%% AUTOMATA AS TERMS %%%%%%%%%%%%
%%%%% state=adjacency list [(symbol_1,state_1),…,(symbol_n,state_n)] %%%%%%%%%%%%
%%% simplest case: omega-automata with b\”uchi acceptance condition, all states implicitly final
accept(Al,[X|L]) :- member((X,Al2),Al), accept(Al2,L).
test1(L) :- S0=[(a,S1)],S1=[(b,S2)],S2=[(e,S0),(c,S3)],S3=[(d,S0)],meta(accept(S0,L)).
%%% more interesting case: deterministic omega-automata with b\”uchi acceptance condition, where final states are
%%% allowed to be a subset of all states
inductive(member(_,_)).
comember(X,[Y|L]) :- member(X,[Y|L]), comember(X,L).
coaccept(S,L) :- coaccept(S,L,FL), comember(f,FL).
coaccept((F,Al),[X|L],[F|FL]) :- member((X,S),Al), coaccept(S,L,FL).
test2(L) :- S0=(f,[(a,S1)]),S1=(f,[(b,S2)]),S2=(f,[(e,S0),(c,S3)]),S3=(f,[(d,S0)]),meta(coaccept(S0,L)).
test3(L) :- S0=(nf,[(a,S1)]),S1=(nf,[(b,S2)]),S2=(nf,[(e,S0),(c,S3)]),S3=(f,[(d,S0)]),meta(coaccept(S0,L)).
% test4(L) :- S0=(nf,[(a,S0),(b,S1),(c,S0)]),S1=(f,[(b,S1)]),meta(coaccept(S0,L)).
%%%%%%%%%% graph bisimulation
bisim(G1,G2) :- sim(G1,G2), sim(G2,G1).
sim(_,[]).
sim(G1,[(X,G2)|L]) :- member((X,G3),G1),sim(G3,G2),sim(G1,L).
testbisim1 :- S=[(a,S),(b,S)],S1=[(a,S2),(b,S2)],S2=[(b,S1),(a,S1)],meta(bisim(S,S1)). %% grafi bisimili
testbisim2 :- S1=[(a,S2)],S2=[(b,S1),(c,S1)],S3=[(a,S4),(a,S5)],S4=[(b,S3)],S5=[(c,S3)],meta(sim(S1,S3)). %% s1 simula s3, ma non viceversa
testbisim3 :- S1=[(a,S2)],S2=[(b,S1),(c,S1)],S3=[(a,S4),(a,S5)],S4=[(b,S3)],S5=[(c,S3)],meta(sim(S3,S1)). %% fallisce
testbisim4 :- S1=[(a,S2)],S2=[(b,S1),(c,S1)],S3=[(a,S4),(a,S5)],S4=[(b,S3)],S5=[(c,S3)],meta(bisim(S1,S3)). %% fallisce
%%%%%%%%%% Example 4.4
inf_list(X,[X|L]) :- inf_list(s(X),L).
p(0) :- inf_list(0,L).
%%%%%%%%%% Example 5.4
notnullable(terminal(X)).
notnullable(NT1*NT2):- notnullable(NT1).
notnullable(NT1*NT2):- notnullable(NT2).
notnullable(NT1|NT2):- notnullable(NT1),notnullable(NT2).
testGramm :- A=((A*B)|terminal(a)), B=((B*C*D)|(C*D)), C=((C*B*terminal(c))|epsilon), D=((terminal(d)*B*D)|epsilon), meta(notnullable(B)).
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%% META INTERPRETER FOR CO-LP
%% SWI PROLOG
%% JANUARY 2013
%% A.D. & D.A.
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%% Call as :- meta(( A1,…,An )).
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
meta(INPUT) :-
add_hyps(INPUT,[],GOAL),
colp(GOAL).
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%% colp
%%
colp( [] ).
colp( [(A = B,_)| R] ):-
A = B,!,
colp(R).
colp( [ (A,_) | R] ):-
inductive(A),
!,
A,
colp(R).
colp( [(Atom,Hyp)| R] ):-
colp_step(Atom,Hyp),
colp(R).
colp( [(Atom,Hyp)| R] ):-
res_step(Atom,Hyp,R1),
colp(R1),
colp(R).
res_step(Atom,Hyp,HypBody) :-
clause(Atom,Body),
add_hyps(Body,[Atom|Hyp],HypBody).
colp_step(Atom,Hyp) :-
member(Atom,Hyp).
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
add_hyps(true, _,[]) :- !.
add_hyps((A,R),Hyps,[(A,Hyps)|S]) :- !,
add_hyps(R,Hyps,S).
%%% Base case: a single atom:
add_hyps(A,Hyps,[(A,Hyps)]).
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%