dawrehxyz

SSLELE

Dec 11th, 2016
702
0
Never
Not a member of Pastebin yet? Sign Up, it unlocks many cool features!
Prolog 1.72 KB | None | 0 0
  1. verify(Input) :-
  2.   see(Input), read(T), read(L), read(S), read(F), seen,
  3.   check(T, L, S, [], F).
  4.  
  5. check(T, L, S, U, F) :-
  6.   verifyState(F, S, L), ! ;
  7.   (
  8.     (neg(_) = F , neg(T, L, S, U, F)) ;
  9.     (or(_) = F , or(T, L, S, U, F)) ;
  10.     (and(_) = F , and(T, L, S, U, F)) ;
  11.     (ax(_) = F , ax(T, L, S, U, F)) ;
  12.     (ag(_) = F , ag(T, L, S, U, F)) ;
  13.     (af(_) = F , af(T, L, S, U, F)) ;
  14.     (ex(_) = F , ex(T, L, S, U, F)) ;
  15.     (eg(_) = F , eg(T, L, S, U, F)) ;
  16.     (ef(_) = F , ef(T, L, S, U, F))
  17.   ), !.
  18.  
  19. af(T, L, S, U, F) :-
  20.   not(member(S, U)),
  21.   af(NewF) = F,
  22.   (
  23.     member([S, Nodes], T), !,
  24.     nextState(S, T, SS),
  25.   )
  26.  
  27.  
  28. ef(T, L, S, U, F) :-
  29.   not(member(S, U)),
  30.   ef(NewF) = F,
  31.   nextState(S, T, NextS),
  32.   check(T, L, NextS, [S|U], NewF), !.
  33.  
  34. %For all paths, the next state must contain a valid formula
  35. ax(T, L, S, U, F) :-
  36.   not(member(S, U)),
  37.   ax(NewF) = F,
  38.   (
  39.     member([S, Nodes], T), !,
  40.     nextState(S, T, SS),
  41.     setof(SS, checkFormula(L, SS, NewF), Nodes), !
  42.   ),
  43.   nextState(S, T, NextS),
  44.   check(T, L, NextS, [S|U], NewF), !.
  45.  
  46. neg(T, L, S, U, F) :-
  47.   neg(NewF) = F,
  48.   not(check(T, L, S, U, NewF)).
  49.  
  50. and(T, L, S, U, F) :-
  51.   and(X, Y) = F,
  52.   (
  53.     check(T, L, S, U, X),
  54.     check(T, L, S, U, Y)
  55.   ), !.
  56.  
  57. or(T, L, S, U, F) :-
  58.   or(X, Y) = F,
  59.   (
  60.     check(T, L, S, U, X);
  61.     check(T, L, S, U, Y)
  62.   ), !.
  63.  
  64. verifyState(F, S, L) :-
  65.   member([S, A], L),
  66.   member(F, A).
  67.  
  68. nextState(S, T, NextS) :-
  69.   member([S, A], T),
  70.   member(NextS, A).
  71.  
  72. checkFormula(L, S, F) :-
  73.   verifyState(F, S, L), ! ;
  74.   (
  75.     neg(_) = F ;
  76.     or(_)  = F ;
  77.     and(_) = F ;
  78.     ax(_)  = F ;
  79.     ag(_)  = F ;
  80.     af(_)  = F ;
  81.     ex(_)  = F ;
  82.     eg(_)  = F ;
  83.     ef(_)  = F
  84.   ), !.
Advertisement