Commit 647ab843 authored by SOLIMAN Sylvain's avatar SOLIMAN Sylvain

forgotten file

parent eeed383e
:- module(
ctl,
[
% grammar
ctl/1,
% command
normalize_query/3
]
).
:- grammar(ctl).
ctl('EX'(E)) :-
ctl(E).
ctl('EF'(E)) :-
ctl(E).
ctl('EG'(E)) :-
ctl(E).
ctl('EU'(E, F)) :-
ctl(E),
ctl(F).
ctl('AX'(E)) :-
ctl(E).
ctl('AF'(E)) :-
ctl(E).
ctl('AG'(E)) :-
ctl(E).
ctl('AU'(E, F)) :-
ctl(E),
ctl(F).
ctl(not(E)) :-
ctl(E).
ctl(E /\ F) :-
ctl(E),
ctl(F).
ctl(E \/ F) :-
ctl(E),
ctl(F).
ctl(E -> F) :-
ctl(E),
ctl(F).
ctl(reachable(E)) :-
ctl(E).
:- doc('reachable(φ) is equivalent to EF(φ)').
ctl(oscil(E)) :-
ctl(E).
:- doc('oscil(φ) is equivalent to AG((φ -> EF(not φ)) /\\\\ (not φ -> EF(φ))),
i.e. AG(EF(φ) /\\\\ EF(not φ))').
ctl(checkpoint(E, F)) :-
ctl(E),
ctl(F).
:- doc('checkpoint(φ, ψ) is equivalent to not EU(not φ, ψ)').
ctl(E) :-
object(E).
normalize_query(Query, NQuery, SLeaves) :-
normalize_query(Query, NQuery, [], Leaves),
sort(Leaves, SLeaves).
normalize_query(reachable(Q), QQ, L1, L2) :-
!,
normalize_query('EF'(Q), QQ, L1, L2).
normalize_query(oscil(Q), QQ, L1, L2) :-
!,
normalize_query('AG'('EF'(Q) /\ 'EF'(not(Q))), QQ, L1, L2).
normalize_query(checkpoint(A, B), QQ, L1, L2) :-
!,
normalize_query(not('EU'(not(A), B)), QQ, L1, L2).
normalize_query(Q, Q, L, [Q | L]) :-
atomic(Q),
!.
normalize_query(Q, QQ, L1, L2) :-
Q =.. [Functor | Args],
% maplist(normalize_query, Args, QArgs),
foldl(normalize_query, Args, QArgs, L1, L2),
QQ =.. [Functor | QArgs].
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment