sat(true,_E).
sat(false,_E):-fail.
sat(ap(Property),E) :- check_ap(Property,E).
sat(p(Property),E) :- check_ap(Property,E).
sat(and(F,G),E) :- sat(F,E), sat(G,E).
sat(or(F,_G),E) :- sat(F,E).
sat(or(_F,G),E) :- sat(G,E).
sat(implies(F,G),E) :- sat(or(not(F),G),E).
sat(not(F),E) :- probformula(_,_,_)\=F,sat_not(F,E).
sat(probformula(Operator,P,Ctl_formula),E) :-
Ctl_formula = u(F,G) ->
prob_calc(u(F,G),E,P_phi),
against(P_phi,P,Operator)
; Ctl_formula = f(G) ->
sat(probformula(Operator,P,u(true,G)),E)
; Ctl_formula = fk(K,G) ->
sat(probformula(Operator,P,uk(true,K,G)),E)
; sat_dynamic(probformula(Operator,P,Ctl_formula),E)
.
sat(not(probformula(Operator,P,Ctl_formula)),E) :-
sat(probformula(not(Operator),P,Ctl_formula),E).
sat(probformula(Operator,P,gk(K,F)),E) :-
Q is 1-P,
sat(not(probformula(Operator,Q,fk(K,not(F)))),E).
sat(probformula(Operator,P,g(F)),E) :-
Q is 1-P,
sat(not(probformula(Operator,Q,f(not(F)))),E).