Not a member of Pastebin yet?
Sign Up,
it unlocks many cool features!
- verify(Input) :-
- see(Input), read(T), read(L), read(S), read(F), seen,
- check(T, L, S, [], F).
- check(T, L, S, U, F) :-
- verifyState(F, S, L), ! ;
- (
- (neg(_) = F , neg(T, L, S, U, F)) ;
- (or(_) = F , or(T, L, S, U, F)) ;
- (and(_) = F , and(T, L, S, U, F)) ;
- (ax(_) = F , ax(T, L, S, U, F)) ;
- (ag(_) = F , ag(T, L, S, U, F)) ;
- (af(_) = F , af(T, L, S, U, F)) ;
- (ex(_) = F , ex(T, L, S, U, F)) ;
- (eg(_) = F , eg(T, L, S, U, F)) ;
- (ef(_) = F , ef(T, L, S, U, F))
- ), !.
- af(T, L, S, U, F) :-
- not(member(S, U)),
- af(NewF) = F,
- (
- member([S, Nodes], T), !,
- nextState(S, T, SS),
- )
- ef(T, L, S, U, F) :-
- not(member(S, U)),
- ef(NewF) = F,
- nextState(S, T, NextS),
- check(T, L, NextS, [S|U], NewF), !.
- %For all paths, the next state must contain a valid formula
- ax(T, L, S, U, F) :-
- not(member(S, U)),
- ax(NewF) = F,
- (
- member([S, Nodes], T), !,
- nextState(S, T, SS),
- setof(SS, checkFormula(L, SS, NewF), Nodes), !
- ),
- nextState(S, T, NextS),
- check(T, L, NextS, [S|U], NewF), !.
- neg(T, L, S, U, F) :-
- neg(NewF) = F,
- not(check(T, L, S, U, NewF)).
- and(T, L, S, U, F) :-
- and(X, Y) = F,
- (
- check(T, L, S, U, X),
- check(T, L, S, U, Y)
- ), !.
- or(T, L, S, U, F) :-
- or(X, Y) = F,
- (
- check(T, L, S, U, X);
- check(T, L, S, U, Y)
- ), !.
- verifyState(F, S, L) :-
- member([S, A], L),
- member(F, A).
- nextState(S, T, NextS) :-
- member([S, A], T),
- member(NextS, A).
- checkFormula(L, S, F) :-
- verifyState(F, S, L), ! ;
- (
- neg(_) = F ;
- or(_) = F ;
- and(_) = F ;
- ax(_) = F ;
- ag(_) = F ;
- af(_) = F ;
- ex(_) = F ;
- eg(_) = F ;
- ef(_) = F
- ), !.
Advertisement