:- op(750, xfy, (=>)). :- op(750, xfy, (<=>)). :- op(800, xfy, (/\)). :- op(900, xfy, (\/)). % Widening flag % widening(N) Enable widening on N steps % stop_widening Stop widening % Debug/optimization flags % For all flags, default: disabled % The predicate 'flagname'/0 enables the flag, the predicate 'flagname'_stop/0 disables it % % local_equality Perform local equality check during fixpoint computation % (default: full equality check) % hull_reasoning Perform hull reasoning % foctl_debug Print fix-point steps % print_progress Print progress for big unions and intersections % log_eval Print evaluated formula % log_time Print log time set_flag(Flag) :- ( call(Flag) -> true ; asserta(Flag) ). % Polyhedric union algebra: % universe_polyhedric_union/1 % empty_polyhedric_union/1 % atomic_polyhedric_union/1 % polyhedron_to_polyhedric_union/2 % polyhedric_union_inter/3 % polyhedric_union_union/3 % polyhedric_union_complement/2 % polyhedric_union_include_local/2 % polyhedric_union_equal_local/2 % polyhedric_union_include/2 % polyhedric_union_equal/2 % polyhedric_union_is_empty/1 % polyhedric_union_projection_dimension/2 % polyhedric_union_projection_dimensions/2 % polyhedric_union_big_inter/2 % This algebra is essential for the definition of the predicate % constraint_to_polyhedric_union/2 % Memory management is explicit % polyhedric_union_delete/1 % polyhedric_union_list_delete/1 % polyhedric_union_copy/2 % All polyhedra are of dimension(N) :- dynamic(dimension/1). initialize_ppl_library :- ['/home/ROCQ/contraintes/common/lib/ppl-0.11.2/lib/ppl/ppl_swiprolog']. set_toplevel_max_depth(N) :- current_prolog_flag(toplevel_print_options, Options0), ( select(max_depth(_), Options0, Options1) -> true ; Options1 = Options0 ), set_prolog_flag(toplevel_print_options, [max_depth(N) | Options1]). initialize_variables(V) :- numbervars(V, 0, Dim), retractall(dimension(_)), asserta(dimension(Dim)). universe_polyhedron(P) :- dimension(D), ppl_new_NNC_Polyhedron_from_space_dimension(D, universe, P). empty_polyhedron(P) :- dimension(D), ppl_new_NNC_Polyhedron_from_space_dimension(D, empty, P). % check_satisfiable(P) % Check that P is not empty. If P is empty, then P is deleted. % % P Polyhedron check_satisfiable(P) :- \+ ( ppl_Polyhedron_is_empty(P), ppl_delete_Polyhedron(P) ). % Polyhedric union are terms of the form union(Hull, List). :- dynamic(hull_reasoning_flag/0). % hull_reasoning % Enable hull reasoning on polyhedric union (tends to make things slower...) hull_reasoning :- set_flag(hull_reasoning_flag). % hull_reasoning_stop % Disable hull reasoning hull_reasoning_stop :- retractall(hull_reasoning_flag). % polyhedron_in_polyhedric_union_local(P, U) % Local inclusion test % % P Polyhedron % U Polyhedric union polyhedron_in_polyhedric_union_local(P, union(Hull, List)) :- ( hull_reasoning_flag, List \= [_] -> ppl_Polyhedron_contains_Polyhedron(Hull, P) ; true ), polyhedron_in_polyhedric_union_local_(P, List). polyhedron_in_polyhedric_union_local_(P, List) :- member(Q, List), ppl_Polyhedron_contains_Polyhedron(Q, P), !. % polyhedric_union_is_empty(U) % Succeeds if U is empty % % U Polyhedric union polyhedric_union_is_empty(union(_, [])). % polyhedric_union_delete(L) % Delete a polyhedric union. % % L Polyhedric union polyhedric_union_delete(union(Hull, List)) :- ( hull_reasoning_flag -> ppl_delete_Polyhedron(Hull) ; true ), polyhedric_union_delete_(List). polyhedric_union_delete_([]). polyhedric_union_delete_([H | T]) :- ppl_delete_Polyhedron(H), polyhedric_union_delete_(T). % polyhedric_union_list_delete(L) % Delete a list of polyhedric unions % % L List of polyhedric unions polyhedric_union_list_delete([]). polyhedric_union_list_delete([H | T]) :- polyhedric_union_delete(H), polyhedric_union_list_delete(T). % polyhedric_union_include_local(U, V) % Local inclusion test % % U Polyhedric union % V Polyhedric union polyhedric_union_include_local(U, V) :- U = union(HU, LU), V = union(HV, LV), ( hull_reasoning_flag, LU \= [_] -> \+ ppl_Polyhedron_is_disjoint_from_Polyhedron(HU, HV) ; true ), index_two_polyhedric_unions(LU, LV, CU, CV), \+ (enumerate_values(PU, PV, CU, CV), member(P, PU), \+ polyhedron_in_polyhedric_union_local(P, union(HV, PV))). % polyhedric_union_include(U, V) % Inclusion test % % U Polyhedric union % V Polyhedric union polyhedric_union_include(U, V) :- U = union(HU, LU), V = union(HV, LV), ( LV = [Q] -> \+ (member(P, LU), \+ ppl_Polyhedron_contains_Polyhedron(Q, P)) ; ( hull_reasoning_flag -> ppl_Polyhedron_contains_Polyhedron(HV, HU) ; true ), index_two_polyhedric_unions(LU, LV, CU, CV), \+ (enumerate_values(PU, PV, CU, CV), \+ ( polyhedric_union_complement(union(HV, PV), V_), polyhedric_union_inter(union(HU, PU), V_, W), polyhedric_union_delete(V_), polyhedric_union_delete(W), polyhedric_union_is_empty(W) % emptyness could be checked after deletion! )) ). test_polyhedric_union_include_local :- initialize_variables([X, A]), constraint_to_polyhedric_union(X = 1, P), constraint_to_polyhedric_union(A < 1 /\ X = 1, Q), polyhedric_union_include_local(Q, P). % polyhedric_union_equal_local(U, V) % Local equality test % % U Polyhedric union % V Polyhedric union polyhedric_union_equal_local(U, V) :- polyhedric_union_include_local(U, V), polyhedric_union_include_local(V, U). % polyhedric_union_equal(U, V) % Equality test % % U Polyhedric union % V Polyhedric union polyhedric_union_equal(U, V) :- polyhedric_union_include(U, V), polyhedric_union_include(V, U). test_polyhedric_union_equal :- \+ \+ ( initialize_variables([X, Y]), constraint_to_polyhedric_union((0 =< X /\ X =< 5 \/ 5 < X /\ X =< 10) /\ (0 =< Y /\ Y =< 10), P), constraint_to_polyhedric_union((0 =< Y /\ Y =< 5 \/ 5 < Y /\ Y =< 10) /\ (0 =< X /\ X =< 10), Q), polyhedric_union_equal(P, Q), polyhedric_union_delete(P), polyhedric_union_delete(Q) ), \+ \+ ( initialize_variables([P1, P2, X]), constraint_to_polyhedric_union(P1>=6/\P2>24/\P2=<34/\P1=<27/\X=11, P), constraint_to_polyhedric_union(P1>=6/\P2>=6/\P2=<24/\P1=<27/\X=11\/P1>=6/\P2>=24/\P2=<34/\P1=<27/\X=11, Q), \+ polyhedric_union_equal(P, Q), polyhedric_union_delete(P), polyhedric_union_delete(Q) ). % simplify(U, V) % Simplify the representation of U by removing subsumed polyhedra. % % U Polyhedric union % V Polyhedric union simplify(union(Hull, L), union(Hull, L_)) :- polyhedra_union_discrete_vars(L, Vars), index_polyhedra_union(L, Vars, Classes), findall( P, ( member(_Values - Class, Classes), simplify_(Class, Class_), member(P, Class_) ), L_ ). simplify_(L, L_) :- one_way_simplify(L, L__), one_way_simplify(L__, L_). % one_way_simplify(L, L_) % Iterate over L to suppress the polyhedra that are subsumed by a polyhedra % previously encountered in the list. Convex hull is used as a first check % to skip checking polyhedra that cannot be subsumed. % L_ contains the remaining polyhedra in reverse order. one_way_simplify(L, L_) :- empty_polyhedron(Hull), one_way_simplify(L, Hull, [], L_), ppl_delete_Polyhedron(Hull). one_way_simplify([], _, Acc, Acc). one_way_simplify([H | T], Hull, Acc, L) :- ( ( Acc = [_] -> true ; ppl_Polyhedron_contains_Polyhedron(Hull, H) ), member(P, Acc), ppl_Polyhedron_contains_Polyhedron(P, H) -> ppl_delete_Polyhedron(H), one_way_simplify(T, Hull, Acc, L) ; ppl_Polyhedron_poly_hull_assign(Hull, H), one_way_simplify(T, Hull, [H | Acc], L) ). :- dynamic(print_progress_flag/0). print_progress :- set_flag(print_progress_flag). print_progress_stop :- retractall(print_progress_flag). % call_predicate(Predicate, Args) % Call p(x1,...,xn,y1,...,ym) % where Args = [x1,...,xn] and OtherArgs = [y1,...,ym] call_predicate(Predicate, Args) :- Predicate =.. [P | OtherArgs], append(Args, OtherArgs, AllArgs), Predicate_ =.. [P | AllArgs], call(Predicate_). % polyhedric_union_big_inter(L, P) % Computes P the intersection of all polyhedric unions in L % % L Polyhedric union list % P Polyhedric union polyhedric_union_big_inter(L, P) :- polyhedric_union_big_operation( L, universe_polyhedric_union, polyhedric_union_inter, P ). % polyhedric_union_big_union(L, P) % Computes P the union of all polyhedric unions in L % % L Polyhedric union list % P Polyhedric union polyhedric_union_big_union(L, P) :- polyhedric_union_big_operation( L, empty_polyhedric_union, polyhedric_union_union, P ). polyhedric_union_big_operation(L, Neutral, Aggregator, P) :- ( L = [] -> call_predicate(Neutral, [P]) ; L = [P_] -> polyhedric_union_copy(P_, P) ; ( print_progress_flag -> length(L, N), write(big_inter(N)), flush ; true ), L = [H | T], polyhedric_union_big_operation_(T, Aggregator, H, 0, 0, N, P) ). polyhedric_union_big_operation_([], _, P, _L, _I, _N, P) :- ( print_progress_flag -> format(' 100%\n',[]) ; true ). polyhedric_union_big_operation_([H | T], Aggregator, P, L, I, N, P__) :- call_predicate(Aggregator, [H, P, P_]), ( print_progress_flag -> J is I + 1, L_ is J * 100 // N, ( L + 5 =< L_ -> format(' ~d', [L_]), flush, L__ = L_ ; L__ = L ) ; true ), polyhedric_union_big_operation_(T, Aggregator, P_, L__, J, N, P__). % constraint_negation(C, D) % Computes D the negation of X % % C Atomic constraint % D Atomic constraint constraint_negation(X = Y, X < Y). constraint_negation(X = Y, X > Y). constraint_negation(X < Y, X >= Y). constraint_negation(X > Y, X =< Y). constraint_negation(X =< Y, X > Y). constraint_negation(X >= Y, X < Y). % polyhedron_complement(P, D) % Computes D the complement of P % % P Polyhedron % D Polyhedric union polyhedron_complement(P, union(Hull, D)) :- ( hull_reasoning_flag -> empty_polyhedron(Hull) ; true ), ppl_Polyhedron_get_constraints(P, L), findall( Q, ( member(C, L), constraint_negation(C, N), universe_polyhedron(Q), ppl_Polyhedron_add_constraint(Q, N), ( hull_reasoning_flag -> ppl_Polyhedron_poly_hull_assign(Hull, Q) ; true ) ), D ). % polyhedric_union_complement(U, V) % Computes U the complement of V % % P Polyhedric union % D Polyhedric union polyhedric_union_complement(union(_, U), V) :- polyhedric_union_complement_(U, C), polyhedric_union_big_inter(C, V), polyhedric_union_list_delete(C). polyhedric_union_inter_complement(P, union(_, U), V) :- polyhedric_union_complement_(U, C), polyhedric_union_big_inter([P | C], V), polyhedric_union_list_delete(C). polyhedric_union_complement_([], []). polyhedric_union_complement_([P | T], [D | U]) :- polyhedron_complement(P, D), polyhedric_union_complement_(T, U). % universe_polyhedric_union(P) % Returns the full polyhedric union P universe_polyhedric_union(union(H, [P])) :- ( hull_reasoning_flag -> universe_polyhedron(H) ; true ), universe_polyhedron(P). % empty_polyhedric_union(P) % Returns the empty polyhedric union P empty_polyhedric_union(union(H, [])) :- ( hull_reasoning_flag -> empty_polyhedron(H) ; true ). test_integerize :- \+ \+ ( integerize(0.1 * '$VAR'(0) + 0.3 =< 0.05, C), C == (2 * '$VAR'(0) + 6 =< 1) ), \+ \+ ( integerize('$VAR'(0) = 0.5, C), C == (2 * '$VAR'(0) = 1) ). integerize(C, D) :- find_constraint_coef(C, E), coef_constraint(C, E, D). integerize_list([], []). integerize_list([H0 | T0], [H1 | T1]) :- integerize(H0, H1), integerize_list(T0, T1). coef_constraint(C, E, D) :- C =.. [Op, C1, C2], coef_expression(C1, E, D1), coef_expression(C2, E, D2), D =.. [Op, D1, D2]. coef_expression(A1 + A2, E, B1 + B2) :- !, coef_expression(A1, E, B1), coef_expression(A2, E, B2). coef_expression(A1 - A2, E, B1 - B2) :- !, coef_expression(A1, E, B1), coef_expression(A2, E, B2). coef_expression(A * X, E, B * X) :- number(A), var_number(X, _), !, B is truncate(A * E). coef_expression(X * A, E, X * B) :- number(A), var_number(X, _), !, B is truncate(A * E). coef_expression(A, E, B) :- number(A), !, B is truncate(A * E). coef_expression(X, E, B) :- var_number(X, _), !, B = E * X. find_constraint_coef(C, E) :- C =.. [_Op, A1, A2], find_expression_coef(A1, E1), find_expression_coef(A2, E2), E is E1 / gcd(E1, E2) * E2. find_expression_coef(A1 + A2, E) :- !, find_expression_coef(A1, E1), find_expression_coef(A2, E2), E is E1 / gcd(E1, E2) * E2. find_expression_coef(A1 - A2, E) :- !, find_expression_coef(A1, E1), find_expression_coef(A2, E2), E is E1 / gcd(E1, E2) * E2. find_expression_coef(A * X, E) :- number(A), var_number(X, _), !, find_number_coef(A, E). find_expression_coef(X * A, E) :- number(A), var_number(X, _), !, find_number_coef(A, E). find_expression_coef(A, E) :- number(A), !, find_number_coef(A, E). find_expression_coef(X, E) :- var_number(X, _), !, E = 1. find_expression_coef(_, _) :- throw(invalid_constraint). find_number_coef(X, E) :- R is rationalize(X), ( R = _ rdiv E -> true ; E = 1 ). % atomic_polyhedric_union(C, P) % Returns the polyhedric union P satisfying the constraint C % % C Atomic linear constraint % P Polyhedric union atomic_polyhedric_union(C, P) :- integerize(C, D), create_singleton_polyhedric_union(ppl_Polyhedron_add_constraint(D), P). % atomic_list_polyhedric_union(L, P) % Returns the polyhedric union P satisfying the list of constraints L % % C List of atomic linear constraints % P Polyhedric union atomic_list_polyhedric_union(L, P) :- integerize_list(L, M), create_singleton_polyhedric_union(ppl_Polyhedron_add_constraints(M), P). % create_singleton_polyhedric_union(Init, U) % Returns U the polyhedric union with a single polyhedron initialized by Init. % % Init Predicate p(P) where P is the polyhedron to initialize % U Polyhedric union create_singleton_polyhedric_union(Init, union(H, L)) :- ( hull_reasoning_flag -> universe_polyhedron(H), call_predicate(Init, [H]) ; true ), universe_polyhedron(P), call_predicate(Init, [P]), ( ppl_Polyhedron_is_empty(P) -> ppl_delete_Polyhedron(P), L = [] ; L = [P] ). % polyhedron_to_polyhedric_union(P, Q) % Returns the polyhedric union Q equaling the polyhedron P % % P Polyhedron % P Polyhedric union polyhedron_to_polyhedric_union(P, union(H, L)) :- ( hull_reasoning_flag -> polyhedron_copy(P, H) ; true ), ( ppl_Polyhedron_is_empty(P) -> L = [] ; L = [Q], polyhedron_copy(P, Q) ). % polyhedric_union_union(U, V, W) % Computes W the union between U and V % Memory management note: polyhedra of U and V are reused in W or deleted % % U Polyhedric union % V Polyhedric union polyhedric_union_union(union(HU, U), union(HV, V), union(HU, W)) :- ( hull_reasoning_flag, ppl_Polyhedron_is_disjoint_from_Polyhedron(HU, HV) -> append(U, V, W) ; index_two_polyhedric_unions(U, V, LU, LV), findall( P, ( enumerate_values(PU, PV, LU, LV), filter_included(PU, union(HV, PV), U_), filter_included(PV, union(HU, U_), V__), ( member(P, U_) ; member(P, V__) ) ), W ) ), ( hull_reasoning_flag -> ppl_Polyhedron_poly_hull_assign(HU, HV) ; true ). % filter_included(L, V, L_) % Keep in L_ only the polyhedra from L that are not included in V % % L List of polyhedra % V Polyhedric union filter_included([], _V, []). filter_included([H | T], V, L) :- ( polyhedron_in_polyhedric_union_local(H, V) -> ppl_delete_Polyhedron(H), filter_included(T, V, L) ; L = [H | U], filter_included(T, V, U) ). % polyhedric_union_inter(U, V, W) % Compute W the intersection between U and V % Memory management note: polyhedra in U and V are copied % % U Polyhedric union % V Polyhedric union % W Polyhedric union polyhedric_union_inter(union(HU, U), union(HV, V), union(HW, W)) :- ( hull_reasoning_flag, ppl_Polyhedron_is_disjoint_from_Polyhedron(HU, HV) -> empty_polyhedric_union(union(HW, W)) ; ( hull_reasoning_flag -> empty_polyhedron(HW) ; true ), index_two_polyhedric_unions(U, V, LU, LV), findall( Z, ( enumerate_common_values(PU, PV, LU, LV), findall( R, ( member(P, PU), member(Q, PV), universe_polyhedron(R), ppl_Polyhedron_intersection_assign(R, P), ppl_Polyhedron_intersection_assign(R, Q), check_satisfiable(R), ( hull_reasoning_flag -> ppl_Polyhedron_poly_hull_assign(HW, R) ; true ) ), X ), simplify_(X, Y), member(Z, Y) ), W ) ). % enumerate_values(PU, PV, ClassesU, ClassesV) % Enumerate the lists of polyhedra PU and PV which share the same values for % discrete variables in ClassesU and ClassesV. Lists of polyhedra whose values % are only in one side are returned together with the empty list for the other % side. % % PU List of polyhedra % PV List of polyhedra % ClassesU List of pairs [Values-Class] % ClassesV List of pairs [Values-Class] enumerate_values(PU, PV, [_ValuesU - PU_ | TU], []) :- !, ( PU = PU_, PV = [] ; enumerate_values(PU, PV, TU, []) ). enumerate_values(PU, PV, [], [_ValuesV - PV_ | TV]) :- !, ( PU = [], PV = PV_ ; enumerate_values(PU, PV, [], TV) ). enumerate_values(PU, PV, LU, LV) :- LU = [ValuesU - PU_ | TU], LV = [ValuesV - PV_ | TV], ( ValuesU @< ValuesV -> ( PU = PU_, PV = [] ; enumerate_values(PU, PV, TU, LV) ) ; ValuesU @> ValuesV -> ( PU = [], PV = PV_ ; enumerate_values(PU, PV, LU, TV) ) ; ( PU = PU_, PV = PV_ ; enumerate_values(PU, PV, TU, TV) ) ). % enumerate_common_values(PU, PV, ClassesU, ClassesV) % Enumerate the lists of polyhedra PU and PV which share the same values for % discrete variables in ClassesU and ClassesV. Lists of polyhedra whose values % are only in one side are discarded. % % PU List of polyhedra % PV List of polyhedra % ClassesU List of pairs [Values-Class] % ClassesV List of pairs [Values-Class] enumerate_common_values(PU, PV, [Values - PU_ | LU], [Values - PV_ | LV]) :- !, ( PU = PU_, PV = PV_ ; enumerate_common_values(PU, PV, LU, LV) ). enumerate_common_values(PU, PV, [ValuesU - PU_ | LU], [ValuesV - PV_ | LV]) :- ( ValuesU @< ValuesV -> enumerate_common_values(PU, PV, LU, [ValuesV - PV_ | LV]) ; enumerate_common_values(PU, PV, [ValuesU - PU_ | LU], LV) ). % polyhedron_discrete_vars(P, Vars) % Enumerates the discrete variables of P (variables of the form X = Const) % % P Polyhedron % Vars Sorted list of variables polyhedron_discrete_vars(P, Vars) :- ppl_Polyhedron_get_constraints(P, C), findall(X, member(1 * X = _, C), Vars_), sort(Vars_, Vars). % polyhedron_discrete_var_values(P, Vars, Values) % Enumerate the values of the discrete variables Vars in P % % P Polyhedron % Vars List of variables % Values List of values polyhedron_discrete_var_values(P, Vars, Values) :- ppl_Polyhedron_get_constraints(P, C), findall(V, (member(X, Vars), member(1 * X = V, C)), Values). % polyhedra_union_discrete_vars(L, Vars) % Enumerate the discrete variables of the list of polyhedra L, % that is to say all the variables which appear on the form X = Const % in all polyhedra of L. polyhedra_union_discrete_vars([], []). polyhedra_union_discrete_vars([H], Vars) :- !, polyhedron_discrete_vars(H, Vars). polyhedra_union_discrete_vars([H | T], Vars) :- polyhedra_union_discrete_vars(T, Vars0), polyhedron_discrete_vars(H, Vars1), intersect_sorted_list(Vars0, Vars1, Vars). % intersect_sorted_list(L0, L1, L) % Compute the intersection L of the sorted lists L0 and L1 % % L0 Sorted list % L1 Sorted list % L Sorted list intersect_sorted_list([], _, []) :- !. intersect_sorted_list(_, [], []) :- !. intersect_sorted_list(L0, L1, L) :- L0 = [H0 | T0], L1 = [H1 | T1], ( H0 @< H1 -> intersect_sorted_list(T0, L1, L) ; H0 @> H1 -> intersect_sorted_list(L0, T1, L) ; L = [H0 | T], intersect_sorted_list(T0, T1, T) ). % index_polyhedra_union(L, Vars, Classes) % Partition the list of polyhedra L on classes with the same values for the % discrete variables Vars % % L List of polyhedra % Vars List of discrete variables % Classes List of pairs [Values-Class] index_polyhedra_union(L, Vars, Classes) :- findall( Values - Class, bagof( P, ( member(P, L), polyhedron_discrete_var_values(P, Vars, Values) ), Class ), Classes_ ), sort(Classes_, Classes). % index_two_polyhedric_unions(U, V, ClassesU, ClassesV) % Partition the lists of polyhedra U and V on their common discrete variables % % U List of polyhedra % V List of polyhedra % ClassesU List of pairs [Values-Class] % ClassesV List of pairs [Values-Class] index_two_polyhedric_unions(U, V, ClassesU, ClassesV) :- polyhedra_union_discrete_vars(U, VarsU), polyhedra_union_discrete_vars(V, VarsV), intersect_sorted_list(VarsU, VarsV, Vars), index_polyhedra_union(U, Vars, ClassesU), index_polyhedra_union(V, Vars, ClassesV). % polyhedric_union_projection_dimension(P, X) % Project (in place) the polyhedric union in dimensions other than X % % X variable polyhedric_union_projection_dimension(union(H, L), X) :- ( hull_reasoning_flag -> ppl_Polyhedron_unconstrain_space_dimension(H, X) ; true ), ( member(P, L), ppl_Polyhedron_unconstrain_space_dimension(P, X), fail ; true ). % polyhedric_union_projection_dimensions(P, X) % Project (in place) the polyhedric union in dimensions other than X % % X variable list polyhedric_union_projection_dimensions(union(H, L), X) :- ( hull_reasoning_flag -> ppl_Polyhedron_unconstrain_space_dimensions(H, X) ; true ), ( member(P, L), ppl_Polyhedron_unconstrain_space_dimensions(P, X), fail ; true ). % polyhedric_union_projection_dimension_s(P, X) % Project (in place) the polyhedric union in dimensions other than X % % X variable or variable list polyhedric_union_projection_dimension_s(R, X) :- ( list(X) -> polyhedric_union_projection_dimensions(R, X) ; polyhedric_union_projection_dimension(R, X) ). % polyhedron_copy(P, Q) % Duplicate the polyhedron P in Q polyhedron_copy(P, Q) :- universe_polyhedron(Q), ppl_Polyhedron_intersection_assign(Q, P). % polyhedric_union_copy(P, Q) % Duplicate the polyhedric union P in Q polyhedric_union_copy(union(H, P), union(I, Q)) :- ( hull_reasoning_flag -> polyhedron_copy(H, I) ; true ), polyhedric_union_copy_(P, Q). polyhedric_union_copy_([], []). polyhedric_union_copy_([P | T], [Q | U]) :- polyhedron_copy(P, Q), polyhedric_union_copy_(T, U). % list(L) % Succeeds if L is a list list([]). list([_H | T]) :- list(T). enumerate_union(C \/ D, L) :- !, enumerate_union(C, CL), enumerate_union(D, DL), append(CL, DL, L). enumerate_union(C, [C]). enumerate_inter(C /\ D, L) :- !, enumerate_inter(C, CL), enumerate_inter(D, DL), append(CL, DL, L). enumerate_inter(C, [C]). % constraint_to_polyhedric_union(Constraint, Polyhedric_union) % Note that there is the dual polyhedric_union_to_constraint/2. % % Constraint C ::= | true | false | C /\ C | C \/ C | not(C) | C => C | C <=> C % | exists(X, C) | forall(X, C) | subst(C, Y, X) % | E = E | E =< E | E >= E | E < E | E > E | E \= E % | integer_between(X, N, M) % | Polyhedron | Polyhedric union % % Polyhedric_union Polyhedric union constraint_to_polyhedric_union(true, R) :- !, universe_polyhedric_union(R). constraint_to_polyhedric_union(false, R) :- !, empty_polyhedric_union(R). constraint_to_polyhedric_union(C /\ not(D), R) :- !, constraint_to_polyhedric_union(C, P), constraint_to_polyhedric_union(D, Q), polyhedric_union_inter_complement(P, Q, R), polyhedric_union_delete(P), polyhedric_union_delete(Q). constraint_to_polyhedric_union(C /\ D, R) :- !, enumerate_inter(C /\ D, L), ( \+ (member(X, L), \+ relational(X)) -> atomic_list_polyhedric_union(L, R) ; constraint_to_polyhedric_union_list(L, PL), polyhedric_union_big_inter(PL, R), polyhedric_union_list_delete(PL) ). constraint_to_polyhedric_union(C \/ D, R) :- !, enumerate_union(C \/ D, L), constraint_to_polyhedric_union_list(L, PL), polyhedric_union_big_union(PL, R). constraint_to_polyhedric_union(not(C => D), R) :- !, constraint_to_polyhedric_union(C /\ not(D), R). constraint_to_polyhedric_union(not(C /\ D), R) :- !, constraint_to_polyhedric_union(not(C) \/ not(D), R). constraint_to_polyhedric_union(not(C \/ D), R) :- !, constraint_to_polyhedric_union(not(C) /\ not(D), R). constraint_to_polyhedric_union(not(C \= D), R) :- !, constraint_to_polyhedric_union(C = D, R). constraint_to_polyhedric_union(not(C = D), R) :- !, constraint_to_polyhedric_union(C \= D, R). constraint_to_polyhedric_union(not(C), R) :- relational(C), !, constraint_negation(C, D), atomic_polyhedric_union(D, R). constraint_to_polyhedric_union(not(C), R) :- !, constraint_to_polyhedric_union(C, P), polyhedric_union_complement(P, R), polyhedric_union_delete(P). constraint_to_polyhedric_union(C => D, R) :- !, constraint_to_polyhedric_union(not(C) \/ D, R). constraint_to_polyhedric_union(C <=> D, R) :- !, constraint_to_polyhedric_union(C => D /\ D => C, R). constraint_to_polyhedric_union(exists(X, C), R_) :- !, constraint_to_polyhedric_union(C, R), polyhedric_union_projection_dimension_s(R, X), simplify(R, R_). constraint_to_polyhedric_union(forall(X, C), R) :- !, constraint_to_polyhedric_union(not(exists(X, not(C))), R). constraint_to_polyhedric_union(subst(C, Y, X), P) :- !, ( list(X) -> eq_list(Y, X, D), constraint_to_polyhedric_union(exists(X, D /\ C), P) ; constraint_to_polyhedric_union(exists(X, Y = X /\ C), P) ). constraint_to_polyhedric_union(A \= B, P) :- !, constraint_to_polyhedric_union(A < B \/ A > B, P). constraint_to_polyhedric_union(integer_between(X, M, N), R) :- !, ( M > N -> empty_polyhedric_union(R) ; M_ is M + 1, constraint_to_polyhedric_union(X = M \/ integer_between(X, M_, N), R) ). constraint_to_polyhedric_union(C, P) :- relational(C), !, atomic_polyhedric_union(C, P). constraint_to_polyhedric_union(C, P) :- number(C), !, polyhedron_to_polyhedric_union(C, P). constraint_to_polyhedric_union(C, R) :- C = union(_, _), !, polyhedric_union_copy(C, R). constraint_to_polyhedric_union(C, _P) :- throw(error(invalid_constraint(C), constraint_to_polyhedric_union / 2)). constraint_to_polyhedric_union_list([], []). constraint_to_polyhedric_union_list([H | T], [P | U]) :- constraint_to_polyhedric_union(H, P), constraint_to_polyhedric_union_list(T, U). test_constraint_to_polyhedric_union(C, C_) :- copy_term(C, S), term_variables(C, Vars), term_variables(S, SVars), zip(SVars, Vars, Subst), initialize_variables(S), constraint_to_polyhedric_union(S, P), polyhedric_union_to_constraint(P, SC_), change_variables(SC_, Subst, C_). eq_list([], [], true). eq_list([X | T], [Y | U], X = Y /\ C) :- eq_list(T, U, C). constraint_big_conjunction([], true). constraint_big_conjunction([X], X) :- !. constraint_big_conjunction([X | T], X /\ C) :- constraint_big_conjunction(T, C). constraint_big_disjunction([], false). constraint_big_disjunction([X], X) :- !. constraint_big_disjunction([X | T], X \/ C) :- constraint_big_disjunction(T, C). % relational(C) % Succeeds if C is relational (sub-predicate for constraint_to_polyhedron / 2) relational(_ = _). relational(_ =< _). relational(_ >= _). relational(_ < _). relational(_ > _). % write_polyhedric_union(P) % Pretty-print the (constraint) of P % % P Polyhedric_union write_polyhedric_union(P) :- polyhedric_union_to_constraint(P, C), write(C). polyhedron_to_constraint(P, C) :- ppl_Polyhedron_get_constraints(P, D), constraint_pretty_list(D, E), constraint_big_conjunction(E, C). % The following predicates pretty-transform a list of atomic % constraints (returned by PPL from a polyhedron) into a readable % constraint. constraint_pretty(C, D) :- C =.. [Op, Left, Right], linear_form_to_list(Left, LLeft), linear_form_to_list(Right, LRight), split_linear_form(LLeft, LeftPos, LeftNeg), split_linear_form(LRight, RightPos, RightNeg), append(LeftPos, RightNeg, LLeftPretty), append(RightPos, LeftNeg, LRightPretty), list_to_linear_form(LLeftPretty, LeftPretty), list_to_linear_form(LRightPretty, RightPretty), D =.. [Op, LeftPretty, RightPretty]. list_to_linear_form([], 0) :- !. list_to_linear_form([P], E) :- !, pair_to_expr(P, E). list_to_linear_form([P | T], E + F) :- !, pair_to_expr(P, E), list_to_linear_form(T, F). pair_to_expr(X - 1, X) :- !. pair_to_expr(1 - X, X) :- !. pair_to_expr(X - Y, X * Y). linear_form_to_list(A + B, L) :- !, linear_form_to_list(A, LA), linear_form_to_list(B, LB), append(LA, LB, L). linear_form_to_list(A * B, L) :- number(A), var_number(B, _), !, L = [A - B]. linear_form_to_list(A, L) :- number(A), !, L = [A - 1]. linear_form_to_list(A, _L) :- throw(invalid_linear_form(A)). split_linear_form([], [], []). split_linear_form([C - X | T], Lpos, Lneg) :- ( C = 0 -> split_linear_form(T, Lpos, Lneg) ; C > 0 -> Lpos = [C - X | Tpos], split_linear_form(T, Tpos, Lneg) ; D is -C, Lneg = [D - X | Tneg], split_linear_form(T, Lpos, Tneg) ). constraint_pretty_list([], []). constraint_pretty_list([A | T], [B | U]) :- constraint_pretty(A, B), constraint_pretty_list(T, U). % polyhedric_union_to_constraint(P, C) % Transform the polyhedric union P to a constraint C % % P Polyhedric union % C Constraint polyhedric_union_to_constraint(union(_, P), C) :- polyhedric_union_to_constraints(P, Cs), constraint_big_disjunction(Cs, C). polyhedric_union_to_constraints([], []). polyhedric_union_to_constraints([P | Ps], [C | Cs]) :- polyhedron_to_constraint(P, C), polyhedric_union_to_constraints(Ps, Cs). % change_variables(F, Subst, G) % Replace the variables in F by the substitution Subst % Useful to get the right variable names at the end of the computation % % F Constraint % Subst Associative list [Var-Value] % G Resulting constraint change_variables(A /\ B, Subst, C /\ D) :- change_variables(A, Subst, C), change_variables(B, Subst, D). change_variables(A \/ B, Subst, C \/ D) :- change_variables(A, Subst, C), change_variables(B, Subst, D). change_variables(A = B, Subst, C = D) :- change_variables_expr(A, Subst, C), change_variables_expr(B, Subst, D). change_variables(A < B, Subst, C < D) :- change_variables_expr(A, Subst, C), change_variables_expr(B, Subst, D). change_variables(A > B, Subst, C > D) :- change_variables_expr(A, Subst, C), change_variables_expr(B, Subst, D). change_variables(A =< B, Subst, C =< D) :- change_variables_expr(A, Subst, C), change_variables_expr(B, Subst, D). change_variables(A >= B, Subst, C >= D) :- change_variables_expr(A, Subst, C), change_variables_expr(B, Subst, D). change_variables(true, _Subst, true). change_variables(false, _Subst, false). change_variables_expr(A + B, Subst, C + D) :- !, change_variables_expr(A, Subst, C), change_variables_expr(B, Subst, D). change_variables_expr(A * B, Subst, C * D) :- !, change_variables_expr(A, Subst, C), change_variables_expr(B, Subst, D). change_variables_expr(A, Subst, B) :- member(A - B, Subst), !. change_variables_expr(A, _Subst, A). % foctl_debug_flag is true if fixpoint searches should be verbose :- dynamic(foctl_debug_flag/0). % foctl_debug % Enable verbose fixpoint searches foctl_debug :- ( foctl_debug_flag -> true ; assertz(foctl_debug_flag) ). foctl_debug_stop :- retractall(foctl_debug_flag). :- dynamic(local_equality_flag/0). local_equality :- ( local_equality_flag -> true ; assertz(local_equality_flag) ). full_equality :- retractall(local_equality_flag). :- dynamic(widening_flag/1). % widening(N) % Enable N-step widening widening(N) :- widening_stop, assert(widening_flag(N)). % widening_stop % Disable widening widening_stop :- retractall(widening_flag(_)). :- dynamic(widening/4). :- dynamic(widening_constraints/1). cleanup_widening :- \+ ( retract(widening_constraints(P)), \+ ( polyhedric_union_delete(P) ) ). cleanup_fix_widening :- ( retract(widening(_, _, Common, _)) -> polyhedric_union_delete(Common) ; true ). intersection_list(A /\ B, L) :- !, intersection_list(A, L0), append(L0, L1, L), intersection_list(B, L1). intersection_list(A, [A]). union_intersection_list(A \/ B, L) :- !, union_intersection_list(A, L0), append(L0, L1, L), union_intersection_list(B, L1). union_intersection_list(A, [L]) :- intersection_list(A, L0), sort(L0, L). extract_common_diff([], LB, [], [], LB) :- !. extract_common_diff(LA, [], [], LA, []) :- !. extract_common_diff([A | LA], [B | LB], LCommon, LDiffA, LDiffB) :- ( A @< B -> LDiffA = [A | TDiffA], extract_common_diff(LA, [B | LB], LCommon, TDiffA, LDiffB) ; B @< A -> LDiffB = [B | TDiffB], extract_common_diff([A | LA], LB, LCommon, LDiffA, TDiffB) ; LCommon = [A | TCommon], extract_common_diff(LA, LB, TCommon, LDiffA, LDiffB) ). find_widening_factors([], [], []). find_widening_factors([H | T], UDiffB, Factors) :- select(H_, UDiffB, UDiffB_), extract_common_diff(H, H_, HCommon, Diff, Diff_), atomic_list_polyhedric_union(Diff, WA), atomic_list_polyhedric_union(Diff_, WB), ( polyhedric_union_include(WA, WB), \+ polyhedric_union_include(WB, WA) -> Way = true ; \+ polyhedric_union_include(WA, WB), polyhedric_union_include(WB, WA) -> Way = false ; polyhedric_union_delete(WA), polyhedric_union_delete(WB), fail ), polyhedric_union_delete(WA), polyhedric_union_delete(WB), Factors = [(HCommon, Diff, Diff_) | TFactors], find_widening_factors(T, UDiffB_, TFactors). widening_isolate(A, B, U, Factors) :- polyhedric_union_to_constraint(A, CA), polyhedric_union_to_constraint(B, CB), union_intersection_list(CA, UA0), sort(UA0, UA), union_intersection_list(CB, UB0), sort(UB0, UB), extract_common_diff(UA, UB, U, UDiffA, UDiffB), find_widening_factors(UDiffA, UDiffB, Factors), !. widening_isolate(A, B, U, C, WA, WB, Way) :- A = union(HA, LA), B = union(HB, LB), select(PA, LA, QA), select(PB, LB, QB), ppl_Polyhedron_get_constraints(PA, CA), ppl_Polyhedron_get_constraints(PB, CB), select(CWA, CA, LC), select(CWB, CB, LC_), atomic_polyhedric_union(CWA, WA), atomic_polyhedric_union(CWB, WB), ( polyhedric_union_include(WA, WB), \+ polyhedric_union_include(WB, WA) -> Way = true ; \+ polyhedric_union_include(WA, WB), polyhedric_union_include(WB, WA) -> Way = false ; polyhedric_union_delete(WA), polyhedric_union_delete(WB), fail ), atomic_list_polyhedric_union(LC, C), atomic_list_polyhedric_union(LC_, C_), ( polyhedric_union_equal(C, C_) -> polyhedric_union_delete(C_) ; polyhedric_union_delete(C), polyhedric_union_delete(C_), fail ), U_ = union(HA, QA), U = union(HB, QB), polyhedric_union_equal(U, U_), !. test_with_respect_to_constraint(U, C) :- constraint_to_polyhedric_union(C, T), ( polyhedric_union_equal(U, T) -> polyhedric_union_delete(T) ; polyhedric_union_delete(T), polyhedric_union_to_constraint(U, U_), format('Failure: ~p expected, ~p found.\n', [C, U_]) ). test_widening_isolate :- initialize_variables([X, Y, Z]), constraint_to_polyhedric_union(X >= 0 \/ Y >= 0 /\ Z =< 1, A), constraint_to_polyhedric_union(X >= 0 \/ Y >= 0 /\ Z =< 2, B), widening_isolate(A, B, U, C, WA, WB, true), test_with_respect_to_constraint(U, X >= 0), test_with_respect_to_constraint(C, Y >= 0), test_with_respect_to_constraint(WA, Z =< 1), test_with_respect_to_constraint(WB, Z =< 2). test_widening_isolate_ :- initialize_variables([X, Y, Z]), constraint_to_polyhedric_union(X >= 0 \/ Y >= 0 /\ Z =< 1, A), constraint_to_polyhedric_union(X >= 0 \/ Y >= 0 /\ Z =< 2, B), widening_isolate(A, B, U, List), print(U), nl, print(List), nl. % fix(A, F, B) % Compute B the Op-fixpoint of F from A % % A Initial value (polyhedric_union) % F Fixpoint predicate % B Solution polyhedric_union fix(A, F, B) :- retractall(widening(_, _, _, _)), ( fix_(A, F, B) -> cleanup_fix_widening ; cleanup_fix_widening, fail ). fix_(A, F, B) :- call_predicate(F, [A, C_]), ( foctl_debug_flag -> write_polyhedric_union(C_), nl ; true ), ( widening_flag(N), widening_isolate(A, C_, U, Common, WA, WB, Way), polyhedric_union_delete(WA), ( retract(widening(M, U_, Common_, Way_)), ( polyhedric_union_equal(Common, Common_) -> polyhedric_union_delete(Common_) ; polyhedric_union_delete(Common_), fail ), Way = Way_, polyhedric_union_equal(U, U_) -> ( M > 0 -> polyhedric_union_delete(WB), M_ is M - 1, assert(widening(M_, U, Common, Way)), fail ; true ) ; polyhedric_union_delete(WB), assert(widening(N, U, Common, Way)), fail ) -> assert(widening_constraints(WB)), ( Way = true -> polyhedric_union_copy(Common, Common__), polyhedric_union_union(U, Common__, C) ; C = U ) ; C = C_ ), ( ( local_equality_flag -> polyhedric_union_equal_local(A, C) ; polyhedric_union_equal(A, C) ) -> polyhedric_union_delete(A), B = C ; polyhedric_union_delete(A), fix_(C, F, B) ). %:- dynamic(predecessor_flag/0). % %predecessor :- % set_flag(predecessor_flag). % % %predecessor_stop :- % retractall(predecessor_flag). % % %compute_predecessor(S, X_, R, C_, P) :- % ( % predecessor_flag % -> % P = exists(X_, R /\ C_) % ; % P = S % ). % ex(C, D, X, X_, R, S) % Compute D = ex(C) % % C Polyhedric union (input) % D Polyhedric union (output) % X List of state variables % X_ List of prime variables % R Polyhedric union (transition relation) % S Polyhedric union (precomputed state constraint, pred(R)) ex(C, D, X, X_, R, _S) :- constraint_to_polyhedric_union(exists(X_, R /\ subst(C, X_, X)), D). ef(C, U, X, X_, R, S) :- polyhedric_union_copy(C, C_), fix(C, ef_predicate(C_, X, X_, R, S), U), polyhedric_union_delete(C_). ef_predicate(P, F, C, X, X_, R, S) :- ex(P, E, X, X_, R, S), polyhedric_union_copy(C, C_), polyhedric_union_union(C_, E, F). eg(C, U, X, X_, R, S) :- polyhedric_union_copy(C, C_), fix(C, eg_predicate(C_, X, X_, R, S), U), polyhedric_union_delete(C_). eg_predicate(P, F, C, X, X_, R, S) :- ex(P, E, X, X_, R, S), polyhedric_union_inter(C, E, F), polyhedric_union_delete(E). eu(C, D, U, X, X_, R, S) :- polyhedric_union_copy(D, D_), fix(D, eu_predicate(C, D_, X, X_, R, S), U). eu_predicate(P, F, C, D, X, X_, R, S) :- ex(P, E, X, X_, R, S), polyhedric_union_inter(C, E, CE), polyhedric_union_copy(D, D_), polyhedric_union_union(D_, CE, F), polyhedric_union_delete(E). ax(C, D, X, X_, R, _S) :- constraint_to_polyhedric_union(subst(C, X_, X), C_), % compute_predecessor(S, X_, R, C_, P), constraint_to_polyhedric_union(exists(X_, R /\ C_) /\ forall(X_, (R => C_)), D). af(C, U, X, X_, R, S) :- polyhedric_union_copy(C, C_), fix(C, af_predicate(C_, X, X_, R, S), U), polyhedric_union_delete(C_). af_predicate(P, F, C, X, X_, R, S) :- ax(P, E, X, X_, R, S), polyhedric_union_copy(C, C_), polyhedric_union_union(C_, E, F). ag(C, U, X, X_, R, S) :- polyhedric_union_copy(C, C_), fix(C, ag_predicate(C_, X, X_, R, S), U), polyhedric_union_delete(C_). ag_predicate(P, F, C, X, X_, R, S) :- axg(P, E, X, X_, R, S), polyhedric_union_inter(C, E, F), polyhedric_union_delete(E). au(C, D, U, X, X_, R, S) :- polyhedric_union_copy(D, D_), fix(D, au_predicate(C, D_, X, X_, R, S), U). au_predicate(P, F, C, D, X, X_, R, S) :- ax(P, E, X, X_, R, S), polyhedric_union_inter(C, E, CE), polyhedric_union_copy(D, D_), polyhedric_union_union(D_, CE, F), polyhedric_union_delete(E). % axg is a specialized version of ax for ag which intersects the relation with % the current state (since ag(c) => c). axg(C, D, X, X_, R, _S) :- constraint_to_polyhedric_union(subst(C, X_, X), C_), % compute_predecessor(S, X_, R, C_, P), constraint_to_polyhedric_union(exists(X_, R /\ C_) /\ not(exists(X_, (R /\ C) /\ not(C_))), D). :- dynamic(log_eval_flag/0). log_eval :- set_flag(log_eval_flag). log_eval_stop :- asserta(log_eval_flag). log_eval(A) :- ( log_eval_flag -> write(A), nl ; true ). log_eval_result(A) :- ( log_eval_flag -> polyhedric_union_to_constraint(A, C), write(C), nl ; true ). % eval(C, X, X_, R, S, Z) % Unifies Z with the solution of C in the CTS R % % C FOCTL formula % X Current state % X_ Next state % R Transition polyhedric_union % S Pred(R) polyhedric_union % Z Polyhedric_union eval(A /\ B, X, X_, R, S, Z) :- !, eval(A, X, X_, R, S, U), eval(B, X, X_, R, S, V), log_eval(A /\ B), polyhedric_union_inter(U, V, Z), log_eval_result(Z), polyhedric_union_delete(U), polyhedric_union_delete(V). eval(A \/ B, X, X_, R, S, Z) :- !, eval(A, X, X_, R, S, U), eval(B, X, X_, R, S, V), log_eval(A \/ B), polyhedric_union_union(U, V, Z), log_eval_result(Z). eval(not(A => B), X, X_, R, S, Z) :- !, eval(A /\ not(B), X, X_, R, S, Z). eval(not(A), X, X_, R, S, Z) :- !, eval(A, X, X_, R, S, U), log_eval(not(A)), polyhedric_union_complement(U, Z_), polyhedric_union_delete(U), polyhedric_union_inter(Z_, S, Z), log_eval_result(Z), polyhedric_union_delete(Z_). eval(A => B, X, X_, R, S, Z) :- !, eval(not(A) \/ B, X, X_, R, S, Z). eval(A <=> B, X, X_, R, S, Z) :- !, eval(A => B /\ B => A, X, X_, R, S, Z). eval(exists(Y, A), X, X_, R, S, Z) :- !, eval(A, X, X_, R, S, Z_), log_eval(exists(Y, A)), polyhedric_union_projection_dimension_s(Z_, Y), simplify(Z_, Z). eval(forall(Y, A), X, X_, R, S, Z) :- !, eval(not(exists(Y, not(A))), X, X_, R, S, Z). eval(ex(A), X, X_, R, S, Z) :- !, eval(A, X, X_, R, S, U), log_eval(ex(A)), ex(U, Z, X, X_, R, S), log_eval_result(Z). eval(ef(A), X, X_, R, S, Z) :- !, eval(A, X, X_, R, S, U), log_eval(ef(A)), ef(U, Z, X, X_, R, S), log_eval_result(Z). eval(eg(A), X, X_, R, S, Z) :- !, eval(A, X, X_, R, S, U), log_eval(eg(A)), eg(U, Z, X, X_, R, S), log_eval_result(Z). eval(eu(A, B), X, X_, R, S, Z) :- !, eval(A, X, X_, R, S, U), eval(B, X, X_, R, S, V), log_eval(eu(A, B)), eu(U, V, Z, X, X_, R, S), log_eval_result(Z). eval(ew(A, B), X, X_, R, S, Z) :- !, eval(not(au(A /\ not(B), not(A) /\ not(B))), X, X_, R, S, Z). eval(ax(A), X, X_, R, S, Z) :- !, eval(A, X, X_, R, S, U), log_eval(ax(A)), ax(U, Z, X, X_, R, S), log_eval_result(Z). eval(af(A), X, X_, R, S, Z) :- !, eval(A, X, X_, R, S, U), log_eval(af(A)), af(U, Z, X, X_, R, S), log_eval_result(Z). eval(ag(A), X, X_, R, S, Z) :- !, eval(A, X, X_, R, S, U), log_eval(ag(A)), ag(U, Z, X, X_, R, S), log_eval_result(Z). eval(au(A, B), X, X_, R, S, Z) :- !, eval(A, X, X_, R, S, U), eval(B, X, X_, R, S, V), log_eval(au(A, B)), au(U, V, Z, X, X_, R, S), log_eval_result(Z). eval(aw(A, B), X, X_, R, S, Z) :- !, eval(not(eu(A /\ not(B), not(A) /\ not(B))), X, X_, R, S, Z). eval(C, _X, _X_, _R, S, P) :- log_eval(C), constraint_to_polyhedric_union(C /\ S, P), log_eval_result(P). % foctl(G, X, A, C, O) % Unify O with the solution of C over G % % G Predicate that specifies the Constraint Transition System. % The first arguments are X, X_, A, R where X and X_ are the % current and next states respectively, A is the parameter % term (see below) and R should be unified with the polyhedron % of the transition system. % X State variable or list of state variables % A Parameter term (a term that carries the other variables, if any) % C FOCTL formula % O Constraint foctl(G, X, A, C, O) :- foctl(G, X, A, C, O, _Subst). foctl(G, X, A, C, O, Subst) :- ( \+ var(X) -> length(X, N), length(X_, N) ; true ), copy_term(f(X, X_, A, C), f(SX, SX_, SA, SC)), term_variables(f(X, X_, A, C), Vars), term_variables(f(SX, SX_, SA, SC), SVars), zip(SVars, Vars, Subst), initialize_variables([SX, SX_, SA, SC]), G =.. [F | Args], G0 =.. [F, SX, SX_, SA, R | Args], statistics(walltime, [_, _]), call(G0), print_walltime('G'), constraint_to_polyhedric_union(exists(SX_, R), Pred), print_walltime('constraint_to_polyhedric_union'), eval(SC, SX, SX_, R, Pred, U), print_walltime('eval'), polyhedric_union_to_constraint(U, SS), polyhedric_union_delete(U), change_variables(SS, Subst, O). :- dynamic(log_time_flag/0). log_time :- set_flag(log_time_flag). log_time_stop :- retractall(log_time_flag). print_walltime(Name) :- ( log_time_flag -> statistics(real_time, [_, Walltime]), format('~a: ~f\n', [Name, Walltime]) ; true ). zip([], [], []). zip([A | As], [B | Bs], [A - B | Cs]) :- zip(As, Bs, Cs). example1(X, X_, A, R) :- constraint_to_polyhedric_union( 1 =< X /\ X =< 4 /\ X_ = X + 1 \/ X = 4 /\ X_ = 3 /\ A < 1 \/ X = 5 /\ X_ = 2, R ). example1_imply(X, X_, A, R) :- constraint_to_polyhedric_union( (1 =< X /\ X =< 4) => X_ = X + 1 /\ (X = 4 /\ A < 1) => X_ = 3 /\ X = 5 => X_ = 2, R ). test_example1 :- foctl(example1, X, _A, eg(X =< _V), C), write(C), nl. example2([X1, X2], [X1_, X2_], A, R) :- constraint_to_polyhedric_union( X1 = 1 /\ X2 = 1 /\ X1_ = 1 /\ X2_ = 1 /\ A > 1 \/ X1 = 1 /\ X2 = 1 /\ X1_ = 2 /\ X2_ = 2 /\ A < 2 \/ X1 = 1 /\ X2 = 1 /\ X1_ = 2 /\ X2_ = 3 /\ A < 2, R ). example3(X, X_, _A, R) :- constraint_to_polyhedric_union(X = 1 => X_ = X + 1, R). example_zenon(X, X_, _A, R) :- constraint_to_polyhedric_union(X = 2 * X_ /\ X >= 0 /\ X < 1, R). example_zenon_forward(X, X_, _A, R) :- constraint_to_polyhedric_union(X_ = 2 * X /\ X >= 0 /\ X < 1, R). example_while([X, Y], [X_, Y_], A, R) :- constraint_to_polyhedric_union( X >= 0 /\ Y >= 0 /\ X_ = X + 1 /\ (X < A => Y_ = Y + 1) /\ (X >= A => Y_ = Y - 1), R ). test_foctl(G, X, A, C, D) :- \+ \+ ( foctl(G, X, A, C, E), numbervars([X, A], 0, _), constraint_to_polyhedric_union(E, P), constraint_to_polyhedric_union(D, Q), ( polyhedric_union_equal(P, Q) -> true ; format('Failed on ~p: ~p\n', [G, C]) ) ). test_foctl :- test_foctl(example1, X, A, ax(X = 5), A >= 1 /\ X = 4), test_foctl(example1, X, A, ex(X = 3), X = 2 \/ A < 1 /\ X = 4), test_foctl(example1_imply, X, A, ex(X = 3), X > 5 \/ X > 4 /\ X < 5 \/ X = 2 \/ X < 1). % Interface with Rovergene % check(E, C) % Check the Rovergene export in file E % % E File to consult % C Constraint to check check_export(Vars, E, C) :- [E], statistics(real_time, [StartTime, _]), self_loop(StateVars, Params, _), StateVars =.. [statevar | StateVarList], Params =.. [param | ParamList], ( StateVarList = Vars -> true ; numberlist(StateVarList, 'X', 1), throw(error(domain_error(StateVarList, Vars), context(check_export / 3))) ), foctl(export, StateVarList, Params, C, O), numberlist(StateVarList, 'X', 1), numberlist(ParamList, 'P', 1), statistics(real_time, [EndTime, _]), Time is EndTime - StartTime, format('~p on ~p in ~ds\n', [C, E, Time]), initialConstraints(Params, I), normalize(O, I, O_), format_solution(O_). numberlist([], _, _). numberlist([H | T], X, I) :- format(atom(H), '~a~d', [X, I]), J is I + 1, numberlist(T, X, J). export(X, X_, A, R) :- initialConstraints(A, LConstraints), constraint_big_conjunction(LConstraints, Constraints), constraint_to_polyhedric_union(Constraints, PI), S =.. [statevar | X], trans(S, A, LTrans), trans_to_constraint(LTrans, X, X_, PI, CT), constraint_to_polyhedric_union(CT, PT), self_loop(S, A, LLoop), loop_to_constraint(LLoop, X, X_, PI, CL), constraint_to_polyhedric_union(CL, PL), constraint_to_polyhedric_union(PT \/ PL, R). trans_to_constraint([], _X, _X_, _Constraints, false). trans_to_constraint([(Src, Trans) | T], X, X_, Constraints, L0 \/ L1) :- trans_to_constraint_(Trans, Src, X, X_, Constraints, L0_), constraint_to_polyhedric_union(L0_, L0), trans_to_constraint(T, X, X_, Constraints, L1). trans_to_constraint_([], _Src, _X, _X_, _Constraints, false). trans_to_constraint_([(Tgt, Cstr) | T], Src, X, X_, Constraints, C \/ U) :- constraint_big_conjunction(Cstr, CCstr), constraint_to_polyhedric_union(Src /\ subst(Tgt, X_, X) /\ CCstr /\ Constraints, C), trans_to_constraint_(T, Src, X, X_, Constraints, U). loop_to_constraint([], _X, _X_, _Constraints, false). loop_to_constraint([(Point, Loop) | T], X, X_, Constraints, C \/ D) :- C = (Point /\ subst(Point, X_, X) /\ Loop /\ Constraints), loop_to_constraint(T, X, X_, Constraints, D). normalize(P1, P2, P3, X1, X2, X3, X4, E, C) :- [E], initialConstraints(param(P1, P2, P3), I), X1 = 'X1', X2 = 'X2', X3 = 'X3', X4 = 'X4', P1 = 'P1', P2 = 'P2', P3 = 'P3', normalize(C, I, D), format_solution(D). normalize(X \/ Y, I, X_ \/ Y_) :- !, normalize(X, I, X_), normalize(Y, I, Y_). normalize(A * X > B /\ Y, I, Y_) :- A_ is -A, B_ is -B, member(A_ * X < B_, I), !, normalize(Y, I, Y_). normalize(A * X < B /\ Y, I, Y_) :- member(A * X < B, I), !, normalize(Y, I, Y_). normalize(X /\ Y, I, X_ /\ Y_) :- !, normalize(X, I, X_), normalize(Y, I, Y_). normalize(A*X > B, _, X > C) :- !, C is B / A. normalize(A*X < B, _, X < C) :- !, C is B / A. normalize(A*X >= B, _, X >= C) :- !, C is B / A. normalize(A*X =< B, _, X =< C) :- !, C is B / A. normalize(X, _, X). format_conj(A /\ B) :- !, format_value(A), write(' /\\ '), format_conj(B). format_conj(A) :- format_value(A). format_value(A) :- write(A). format_solution(A \/ B) :- !, format_conj(A), write(' \\/\n'), format_solution(B). format_solution(A) :- format_conj(A), nl. test_widening :- widening(2), \+ \+ ( foctl(test_widening, X, _A, ef(0 =< X /\ X =< Y), C), X = 'X', Y = 'Y', print(C), nl ). test_widening(X, X_, _A, C) :- constraint_to_polyhedric_union( ( X < X_ + 1 ), C ).