DEMO CILC 2013

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

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

Comments are closed.