:- module( foltl, [ % Grammar foltl/1, foltl_predicate/1, foltl_expression/1, parameter_between_interval/1, variable_objective/1, time_value/1, time_value_list/1, % Biocham commands validity_domain/1, satisfaction_degree/2, (ltl_pattern)/1, list_ltl_patterns/0, delete_ltl_pattern/1, expand_ltl/1, % Public API expand_formula/2, validity_domain/2, satisfaction_degree/3, generate_domain_cpp/1, generate_domain_cpp/2, generate_objective/1, free_variable_index/2, column/2, op(700, xfy, '<>'), op(700, xfy, '<<'), op(700, xfy, '>>'), op(800, yfx, '/\\'), % left parentheses for the reversed order used below op(900, yfx, '\\/'), % idem op(1010, fx, ltl_pattern) ] ). % linting :- use_module(doc). :- use_module(biocham). :- use_module(objects). :- use_module(reaction_rules). :- doc('Firt-Order Linear Time Logic with linear constraints over the reals, FO-LTL(Rlin), can be used to specify semi-qualitative semi-quantitative constraints on the dynamical behavior of the system, in a much more flexible manner than by curves to fit \\cite{RBFS11tcs}. The syntax of FO-LTL(Rlin) formulas is given below together with some useful abbreviations \\cite{FT14book}:'). :- doc('The \\texttt{foltl_magnitude} option (default 5) is the multiplicative factor used for the strong comparison operators \\texttt{<<} and \\texttt{>>} over positive numbers, \\texttt{A<} over real numbers.'). :- initial('option(foltl_magnitude: 5)'). :- devdoc('TODO: split this file into two and create ppl.pl (structure similar to ctl.pl/nusmv.pl) I failed because of unextricable errors with grammar_map as always... \\begin{itemize} \\item add_ltl for creating FO-LTL(Rlin) specifications \\item generate_ltl for interesting patterns with objective values \\item in ppl.pl: move from here the cpp program generation for ppl and compute robustness as penetration depth in addition to satisfaction degree \\item in tables.pl or perhaps numerical_simulation.pl about traces: move from here the little time:value list grammar, and add trace simplification keeping only the time points that are extremal for some variable \\end{itemize}'). :- devdoc('\\section{Grammar}'). :- grammar(foltl). foltl('X'(F)) :- foltl(F). foltl('F'(F)) :- foltl(F). foltl('G'(F)) :- foltl(F). foltl(not(F)) :- foltl(F). foltl('U'(F, G)) :- foltl(F), foltl(G). foltl('R'(F, G)) :- foltl(F), foltl(G). foltl('W'(F, G)) :- foltl(F), foltl(G). foltl(F /\ G) :- foltl(F), foltl(G). foltl(F \/ G) :- foltl(F), foltl(G). foltl(exists(X, F)) :- name(X), foltl(F). foltl(F => G) :- foltl(F), foltl(G). % :- doc(' \\emphright{\\texttt{f => g} is equivalent to \\texttt{not f \\\\/ g}}'). foltl(G <=> F) :- foltl(F), foltl(G). % :- doc(' \\emphright{\\texttt{f <=> g} is equivalent to \\texttt{f => g /\\\\ g => f}}'). foltl(false). foltl(true). foltl(FunctionApplication) :- function_application(untyped, FunctionApplication). foltl(F) :- foltl_predicate(F). :- grammar(foltl_predicate). foltl_predicate(E = F) :- foltl_expression(E), foltl_expression(F). foltl_predicate(E <> F) :- foltl_expression(E), foltl_expression(F). foltl_predicate(E << F) :- foltl_expression(E), foltl_expression(F). foltl_predicate(E >> F) :- foltl_expression(E), foltl_expression(F). foltl_predicate(E < F) :- foltl_expression(E), foltl_expression(F). foltl_predicate(E <= F) :- foltl_expression(E), foltl_expression(F). foltl_predicate(E > F) :- foltl_expression(E), foltl_expression(F). foltl_predicate(E >= F) :- foltl_expression(E), foltl_expression(F). :- grammar(foltl_expression). foltl_expression(E + F) :- foltl_expression(E), foltl_expression(F). foltl_expression(E - F) :- foltl_expression(E), foltl_expression(F). foltl_expression(E * F) :- foltl_expression(E), foltl_expression(F). foltl_expression(E ^ F) :- foltl_expression(E), foltl_expression(F). foltl_expression(E / F) :- foltl_expression(E), foltl_expression(F). foltl_expression(E) :- number(E). foltl_expression(FunctionApplication) :- function_application(foltl_expression, FunctionApplication). foltl_expression(E) :- name(E). foltl_expression([E]) :- name(E). :- grammar(time_value). time_value(Time:Value) :- time(Time), number(Value). :- grammar(time_value_list). time_value_list(L):- list(time_value, L). :- grammar(parameter_between_interval). parameter_between_interval(Min <= Parameter <= Max) :- number(Min), parameter_name(Parameter), number(Max). :- grammar(variable_objective). variable_objective(Variable -> Value) :- name(Variable), number(Value). :- doc('Furthermore, some useful abbreviations have been predefined with the following FO-LTL(Rlin) formula patterns:'). :- initial('ltl_pattern forall(X, Formula) = not(exists(X, not(Formula)))'). :- initial('ltl_pattern reachable(Formula) = F(Formula)'). :- initial('ltl_pattern steady(Formula) = G(Formula)'). :- doc('\\emph{Curves.}'). :- initial('ltl_pattern curve(Molecule, Time_Value_List) = curve(Molecule, Time_Value_list)'). :- doc('\\emph{Sequence of events} \\doi{MRMFJ08bi}.'). :- initial('ltl_pattern occurs(Formula) = F(Formula)'). :- initial('ltl_pattern excludes(Formula) = G(not(Formula))'). :- initial('ltl_pattern invariates(Formula) = G(Formula)'). :- initial('ltl_pattern weak_sequence(Formula1, Formula2) = F(Formula1 /\\ F(Formula2))'). :- initial('ltl_pattern exact_sequence(Formula1, Formula2) = F(Formula1 /\\ X(Formula2))'). :- initial('ltl_pattern sequence(Formula1, Formula2) = G(U(Formula1,Formula2))'). :- initial('ltl_pattern consequence(Formula1, Formula2) = G(Formula1 => F(Formula2))'). :- initial('ltl_pattern implication(Formula1, Formula2) = G(Formula1 => Formula2)'). :- doc('\\emph{Thresholds, global extrema, amplitudes} \\cite{FT14book}.'). :- initial('ltl_pattern reached(Molecule, Concentration) = F(Molecule >= Concentration)'). :- initial('ltl_pattern unreached(Molecule, Concentration) = F(Molecule <= Concentration)'). :- initial('ltl_pattern inf_amplitude(Molecule, Amplitude) = exists(Concentration, F(Molecule <= Concentration /\\ F(Molecule >= Concentration+Amplitude)))'). :- initial('ltl_pattern sup_amplitude(Molecule, Amplitude) = exists(Concentration, G(Molecule >= Concentration /\\ Molecule <= Concentration+Amplitude))'). :- initial('ltl_pattern first_value(Molecule, Concentration) = (Molecule=Concentration)'). :- initial('ltl_pattern last_value(Molecule, Concentration) = F(G(Molecule=Concentration))'). % non linear constraints %:- initial('ltl_pattern value(Molecule, T, Concentration) = F(exists(c, exists(t1, exists(t2, Molecule=c /\\ Time=t1 /\\ t1<=T /\\ X(Time=t2 /\\ t2>T /\\ Concentration=c+(T-t1)*(Molecule-c)/(t2-t1))))))'). %:- initial('ltl_pattern differential(Molecule, T, Diff) = F(exists(Concentration, exists(t1, exists(t2, Molecule=Concentration /\\ Time=t1 /\\ t1<=T /\\ X(Time=t2 /\\ t2>T /\\ Diff=(Molecule-Concentration)/(t2-t1))))))'). %:- initial('ltl_pattern differential(Molecule, Diff) = exists(Concentration, exists(t1, exists(t2, Molecule=Concentration /\\ Time=t1 /\\ X(Time=t2 /\\ Diff=(Molecule-Concentration)/(t2-t1)))))'). %:- initial('ltl_pattern maximum(Molecule, Concentration) = (G(Molecule <= Concentration) /\\ F(Molecule=Concentration))'). :- initial('ltl_pattern maximum(Molecule, Concentration) = (G(Molecule <= Concentration) /\\ F(Molecule>=Concentration))'). :- initial('ltl_pattern minimum(Molecule, Concentration) = (G(Molecule >= Concentration) /\\ F(Molecule<=Concentration))'). :- initial('ltl_pattern maximum(Molecule, Concentration, T) = (G(Molecule <= Concentration) /\\ F(Molecule>=Concentration /\\ Time=T))'). :- initial('ltl_pattern minimum(Molecule, Concentration, T) = (G(Molecule >= Concentration) /\\ F(Molecule<=Concentration /\\ Time=T))'). :- initial('ltl_pattern amplitude(Molecule, Amplitude) = exists(Minimum, exists(Maximum, maximum(Molecule,Maximum) /\\ minimum(Molecule, Minimum) /\\ Amplitude=Maximum-Minimum))'). %:- initial('ltl_pattern amplitude2(Molecule, Amplitude) = exists(Minimum, minimum(Molecule,Minimum) /\\ maximum(Molecule, Minimum+Amplitude))'). % infinite loop in PPL ? why ? %:- initial('ltl_pattern amplitude3(Molecule, Amplitude) = exists(Minimum, (G(Minimum <= Molecule /\\ Molecule <= Minimum+Amplitude) /\\ F(Molecule=Minimum) /\\ F(Molecule=Minimum+Amplitude)))'). :- doc('\\emph{Local extrema}'). %:- initial('ltl_pattern increase(Molecule, Concentration) = ((Molecule=Concentration) /\\ X(Molecule>=Concentration))'). :- initial('ltl_pattern increase(Molecule, Concentration) = ((Molecule<=Concentration) /\\ X(Molecule>=Concentration))'). :- initial('ltl_pattern decrease(Molecule, Concentration) = ((Molecule>=Concentration) /\\ X(Molecule<=Concentration))'). :- initial('ltl_pattern increase(Molecule) = exists(Concentration, increase(Molecule, Concentration))'). :- initial('ltl_pattern decrease(Molecule) = exists(Concentration, decrease(Molecule, Concentration))'). :- initial('ltl_pattern local_maximum(Molecule, Concentration) = F(peak(Molecule,Concentration))'). :- initial('ltl_pattern local_maximum(Molecule, Concentration, T) = F(peak(Molecule,Concentration,T))'). :- initial('ltl_pattern peak(Molecule, Concentration) = (MoleculeConcentration /\\ X(increase(Molecule, Concentration)))'). :- initial('ltl_pattern base(Molecule, Concentration, T) = (Molecule>Concentration /\\ X(increase(Molecule, Concentration) /\\ Time=T))'). :- initial('ltl_pattern first_base(Molecule, Concentration, T) = U(increase(Molecule), U(decrease(Molecule), base(Molecule, Concentration, T)))'). :- initial('ltl_pattern first_base(Molecule, Concentration) = U(increase(Molecule), U(decrease(Molecule), base(Molecule, Concentration)))'). :- initial('ltl_pattern last_base(Molecule, Concentration, T) = F(base(Molecule, Concentration, T) /\\ X(U(increase(Molecule), U(decrease(Molecule), exists(c, G(Molecule=c))))))'). :- initial('ltl_pattern last_base(Molecule, Concentration) = F(base(Molecule, Concentration /\\ X(U(increase(Molecule), U(decrease(Molecule), exists(c, G(Molecule=c)))))))'). :- initial('ltl_pattern successive_bases(Molecule, C1, T1, C2, T2) = F(U(increase(Molecule), U(decrease(Molecule), base(Molecule,C1, T1) /\\ X(first_base(Molecule, C2, T2)))))'). :- initial('ltl_pattern successive_bases(Molecule, C1, C2) = F(U(increase(Molecule), U(decrease(Molecule), base(Molecule,C1) /\\ X(first_base(Molecule, C2)))))'). :- initial('ltl_pattern first_successive_bases(Molecule, C1, T1, C2, T2) = U(increase(Molecule), U(decrease(Molecule), base(Molecule,C1, T1) /\\ X(first_base(Molecule, C2, T2))))'). :- initial('ltl_pattern last_successive_bases(Molecule, C1, T1, C2, T2) = F(base(Molecule,C1, T1) /\\ X(U(increase(Molecule), U(decrease(Molecule), base(Molecule,C2, T2) /\\ X(U(increase(Molecule), U(decrease(Molecule), exists(c, G(Molecule=c)))))))))'). :- doc('\\emph{Periods and delays.}'). :- initial('ltl_pattern period(Molecule, Period) = exists(T1, exists(T2, exists(C1, exists(C2, successive_peaks(Molecule, C1, T1, C2, T2) /\\ Period=T2-T1))))'). :- initial('ltl_pattern first_period(Molecule, Period) = exists(T1, exists(T2, exists(C1, exists(C2, first_successive_peaks(Molecule, C1, T1, C2, T2) /\\ Period=T2-T1))))'). :- initial('ltl_pattern last_period(Molecule, Period) = exists(T1, exists(T2, exists(C1, exists(C2, last_successive_peaks(Molecule, C1, T1, C2, T2) /\\ Period=T2-T1))))'). :- initial('ltl_pattern delay(Molecule1, Molecule2, Delay) = exists(T1, exists(T2, exists(C1, exists(C2, F(peak(Molecule1,C1,T1) /\\ first_peak(Molecule2,C2,T2) /\\ Delay=T2-T1)))))'). :- initial('ltl_pattern first_delay(Molecule1, Molecule2, Delay) = exists(T1, exists(T2, exists(C1, exists(C2, U(decrease(Molecule1), U(increase(Molecule1), peak(Molecule1, C1, T1) /\\ first_peak(Molecule2,C2,T2) /\\ Delay=T2-T1))))))'). % first_peak(Molecule1,C1,T1) /\\ first_peak(Molecule2,C2,T2) /\\ Delay=T2-T1))))'). :- initial('ltl_pattern last_delay(Molecule1, Molecule2, Delay) = exists(T1, exists(T2, exists(C1, exists(C2, last_peak(Molecule1,C1,T1) /\\ last_peak(Molecule2,C2,T2) /\\ Delay=T2-T1))))'). :- initial('ltl_pattern base_period(Molecule, Period) = exists(T1, exists(T2, exists(C1, exists(C2, successive_bases(Molecule, C1, T1, C2, T2) /\\ Period=T2-T1))))'). :- initial('ltl_pattern first_base_period(Molecule, Period) = exists(T1, exists(T2, exists(C1, exists(C2, first_successive_bases(Molecule, C1, T1, C2, T2) /\\ Period=T2-T1))))'). :- initial('ltl_pattern last_base_period(Molecule, Period) = exists(T1, exists(T2, exists(C1, exists(C2, last_successive_bases(Molecule, C1, T1, C2, T2) /\\ Period=T2-T1))))'). :- initial('ltl_pattern base_delay(Molecule1, Molecule2, Delay) = exists(T1, exists(T2, exists(C1, exists(C2, F(base(Molecule1,C1,T1) /\\ first_base(Molecule2,C2,T2) /\\ Delay=T2-T1)))))'). :- initial('ltl_pattern first_base_delay(Molecule1, Molecule2, Delay) = exists(T1, exists(T2, exists(C1, exists(C2, U(increase(Molecule1), U(decrease(Molecule1), base(Molecule1, C1, T1) /\\ first_base(Molecule2,C2,T2) /\\ Delay=T2-T1))))))'). % first_base(Molecule1,C1,T1) /\\ first_base(Molecule2,C2,T2) /\\ Delay=T2-T1))))'). :- initial('ltl_pattern last_base_delay(Molecule1, Molecule2, Delay) = exists(T1, exists(T2, exists(C1, exists(C2, last_base(Molecule1,C1,T1) /\\ last_base(Molecule2,C2,T2) /\\ Delay=T2-T1))))'). :- devdoc('\\section{Commands}'). :- doc('FO-LTL(Rlin) formulas are evaluated on traces, i.e. numerical data time series either generated by simulation or loaded from biological experiments. FO-LTL(Rlin) formulas may contain free variables, in which case they are called constraints. While a closed formula (i.e. without free variable) is either true or false on a trace, a formula with free variable is either satisfiable (i.e. true for some valuations of the variables) or unsatisfiable (i.e. false for any valuation).'). validity_domain(Formula) :- biocham_command, type(Formula, foltl), doc(' solves a FOLTL(Rlin) constraint on the current trace, i.e. computes the validity domain for the free variables that make the formula true on the numerical trace. The formula is false if the validity domain of one of its free variables is empty, and satisfiable otherwise. \\clearmodel \\begin{example} \\trace{ biocham: a => b. biocham: present(a,10). biocham: numerical_simulation. plot. biocham: validity_domain(G(Time < T => a > b)). } \\end{example} '), option(foltl_magnitude, number, _Magnitude, 'order of magnitude for << and >> operators'), validity_domain(Formula, Domain), format('~w\n', [Domain]). satisfaction_degree(Formula, Objective) :- biocham_command, type(Formula, foltl), type(Objective, [variable_objective]), option(foltl_magnitude, number, _Magnitude, 'order of magnitude for << and >> operators'), doc(' computes a continuous satisfaction degree in the interval [0,+∞) for an FOLTL(Rlin) property on the current trace with respect to some objective values for the free variables of the formula. The degree is greater or equal than 1 if the formula is satisfied. The greater the degree the greater the margin in the satisfaction of the formula (i.e. formula satisfaction robustness). This satisfaction degree is computed by (an approximation of) the distance of the objective point to the validity domain of the formula (if less than 1), or by its penetration depth (if greater than 1). '), satisfaction_degree(Formula, Objective, Degree), format('~f\n', [Degree]). ltl_pattern(PatternList) :- biocham_command(*), type(PatternList, '*'(function_prototype = foltl)), doc('sets the definition of patterns.'), \+ ( member(Pattern = Value, PatternList), \+ ( set_macro(ltl_pattern, Pattern, Value) ) ). list_ltl_patterns :- biocham_command, doc('lists all known LTL patterns.'), list_items([kind: ltl_pattern]). expand_ltl(Formula) :- biocham_command, type(Formula, foltl), doc('shows the expansion in LTL of a formula with patterns.'), expand_formula(Formula,ExpandedFormula), format('~w\n', [ExpandedFormula]). delete_ltl_pattern(FunctorSet) :- biocham_command(*), type(FunctorSet, '*'(functor)), doc('deletes some LTL patterns. Either arity is given, or all LTL patterns with the given functor are deleted.'), \+ ( member(Functor, FunctorSet), \+ ( delete_macro(ltl_pattern, Functor) ) ). :- devdoc('\\section{Public API}'). validity_domain(Formula, Domain) :- compute_domain('ppl_validity_domain.cc', Formula, none, DomainRaw), reformat_domain(DomainRaw, Domain). satisfaction_degree(Formula, Objective, SatisfactionDegree) :- compute_domain( 'satisfaction_degree.cc', Formula, some(Objective), SatisfactionDegree ). :- devdoc('\\section{Private predicates}'). compute_domain(CppProgram, Formula, Objective, Result) :- CFilename = 'check.inc', TableFilename = 'check.csv', ExecutableFilename = 'check', expand_formula(Formula, ExpandedFormula), with_clean( [foltl:column/2], ( populate_table_columns, with_output_to_file( CFilename, ( generate_domain_cpp(ExpandedFormula), ( Objective = some(Objective0) -> generate_objective([Objective0]) ; true ) ) ) ) ), compile_domain_cpp_program(CppProgram, ExecutableFilename), export_table(TableFilename), call_subprocess( ExecutableFilename, [TableFilename], [stdout(pipe(ResultStream))] ), read_term( ResultStream, Result, [variables(Variables), variable_names(VariableNames)]), name_variables_and_anonymous(Variables, VariableNames), !, ( have_to_delete_temporary_files -> delete_file(CFilename), delete_file(ExecutableFilename), delete_file(TableFilename) ; true ). populate_table_columns :- get_current_table(Table), \+ ( columns(Table, Index, X), \+ ( assertz(column(X, Index)) ) ). expand_formula(curve(Molecule, Time_Value_List), ExpandedFormula):- !, expand_curve(Time_Value_List, Molecule, ExpandedFormula). expand_formula(F => G, ExpandedFormula) :- !, expand_formula(not(F) \/ G, ExpandedFormula). expand_formula(not(Formula), ExpandedNegatedFormula) :- !, expand_formula(Formula, ExpandedFormula), ( negate_formula(ExpandedFormula, NegatedFormula) -> expand_formula(NegatedFormula, ExpandedNegatedFormula) ; ExpandedNegatedFormula = not(ExpandedFormula) ). expand_formula(Formula, ExpandedFormula) :- macro_apply(ltl_pattern, Formula, NewBody), !, expand_formula(NewBody, ExpandedFormula). %expand_formula((A < B), (A+P <= B)):- % let us believe in the precision option % !, % get_option(precision, FOLTLPrecision), % P is 10 ** (-FOLTLPrecision). % %expand_formula((A > B), (A >= B+P)):- % !, % get_option(precision, FOLTLPrecision), % P is 10 ** (-FOLTLPrecision). expand_formula((A << B), R):- !, get_option(foltl_magnitude, M), expand_formula((M*A < B), R). expand_formula((A >> B), R):- !, get_option(foltl_magnitude, M), expand_formula((A > M*B), R). expand_formula(true, ExpandedFormula):- % ... !, expand_formula(1<1000, ExpandedFormula). expand_formula(false, ExpandedFormula):- !, expand_formula(1>1000, ExpandedFormula). expand_formula(Formula, ExpandedFormula) :- grammar_map( foltl, [foltl:foltl:expand_formula, foltl_expression:foltl:expand_expression], Formula, ExpandedFormula ). expand_curve([Time:Value], Molecule, 'F'('Time'=Time /\ Molecule=Value)) :- !. expand_curve([(Time:Value)|Tail], Molecule, 'Time'=Time /\ Molecule=Value /\ 'X'('F'(TailFormula))) :- expand_curve(Tail, Molecule, TailFormula). expand_expression(Expression, ExpandedExpression) :- function_apply(Expression, NewBody), !, expand_expression(NewBody, ExpandedExpression). expand_expression(Expression, ExpandedExpression) :- grammar_map( foltl_expression, [foltl_expression:foltl:expand_expression], Expression, ExpandedExpression ). negate_formula(false, true). negate_formula(true, false). negate_formula(not(A), A). negate_formula(A \/ B, NotA /\ NotB) :- negate_formula(A, NotA), negate_formula(B, NotB). negate_formula(A /\ B, NotA \/ NotB) :- negate_formula(A, NotA), negate_formula(B, NotB). negate_formula('X'(A), 'X'(NotA)) :- negate_formula(A, NotA). negate_formula('F'(A), 'G'(NotA)) :- negate_formula(A, NotA). negate_formula('G'(A), 'F'(NotA)) :- negate_formula(A, NotA). negate_formula('U'(A, B), 'W'(NotB, NotA)) :- negate_formula(A, NotA), negate_formula(B, NotB). negate_formula('W'(A, B), 'U'(NotB, NotA)) :- negate_formula(A, NotA), negate_formula(B, NotB). negate_formula('R'(A, B), 'U'(NotA, NotB)) :- negate_formula(A, NotA), negate_formula(B, NotB). negate_formula(A <= B, A > B). negate_formula(A > B, A <= B). negate_formula(A >= B, A < B). negate_formula(A < B, A >= B). negate_formula(A = B, A <> B). % A < B \/ A > B). negate_formula(A << B, M*A >= B):- get_option(foltl_magnitude, M). negate_formula(A >> B, A <= M*B):- get_option(foltl_magnitude, M). prolog:message(error(unknown_free_variable(Variable))) --> ['Unknown free variable: ~p'-[Variable]]. :- dynamic(free_variable_index/2). :- dynamic(sub_formula/2). :- dynamic(column/2). generate_objective(Objectives) :- get_option(precision, FOLTLPrecision), Precision is 10 ** FOLTLPrecision, format('#define FOLTL_PRECISION ~d\n', [Precision]), maplist(length, Objectives, Counts), write('static const int objective_count[] = {\n'), forall( member(Count, Counts), format(' ~d,~n', [Count]) ), write('};\n'), forall( nth0(Index, Objectives, Objective), generate_objective(Index, Objective) ), length(Objectives, NObjectives), MaxObj is NObjectives - 1, write('static const struct variable_objective *var_obj[] = {\n'), forall( between(0, MaxObj, I), format(' variable_objectives~d,~n', [I]) ), write('};\n'). generate_objective(Index, Objective) :- length(Objective, ObjectiveCount), write('static const struct variable_objective\n'), format('variable_objectives~d[~d] = {~n', [Index, ObjectiveCount]), \+ ( member((Variable -> Value), Objective), \+ ( ( foltl:free_variable_index(Variable, VariableIndex) -> true ; search:free_variable_index(Index, Variable, VariableIndex) -> true ; throw(error(unknown_free_variable(Variable))) ), format(' {~d, ~f},\n', [VariableIndex, Value]) ) ), write('};\n'). generate_domain_cpp(Formula) :- generate_domain_cpp(Formula, ''). generate_domain_cpp(Formula, FuncSuffix) :- expand_formula(Formula, ExpandedFormula), set_counter(free_variables, 0), retractall(free_variable_index(_, _)), set_counter(sub_formulae, 0), retractall(sub_formula(_, _)), format( '\c static Domain compute_domain~w(const Table &table) { ', [FuncSuffix]), declare_free_variables(ExpandedFormula), check_linearity(ExpandedFormula), declare_formula(ExpandedFormula, RootIndex), write( ' \c for (Table::const_reverse_iterator i = table.rbegin(); i != table.rend(); ++i) { '), \+ ( sub_formula(SubFormula, Index), \+ ( generate_sub_formula(SubFormula, Index) ) ), \+ ( sub_formula(_SubFormula, Index), \+ ( format(' domain~d = next_domain~d;\n', [Index, Index]) ) ), format( ' \c } domain~d.pairwise_reduce(); return domain~d; } ', [RootIndex, RootIndex]). generate_sub_formula(Predicate, Index) :- get_option(precision, FOLTLPrecision), Precision is 10 ** FOLTLPrecision, binary_predicate(Predicate, A, Op, B), !, with_output_to( atom(Left), generate_expression(A) ), with_output_to( atom(Right), generate_expression(B) ), peek_count(free_variables, FreeVariableCount), ( ( has_variable(A) ; has_variable(B) ) -> format( ' \c Domain next_domain~d(~d, PPL::EMPTY); { PPL::Constraint_System cs; cs.set_space_dimension(~d); cs.insert((~a) * ~d ~a (~a) * ~d); next_domain~d.add_disjunct(PPL::NNC_Polyhedron(cs)); } ', [Index, FreeVariableCount, FreeVariableCount, Left, Precision, Op, Right, Precision, Index] ) ; format( ' \c Domain next_domain~d(~d, ~a ~a ~a ? PPL::UNIVERSE : PPL::EMPTY); ', [Index, FreeVariableCount, Left, Op, Right] ) ). generate_sub_formula('X'(A), Index) :- sub_formula(A, AIndex), format( ' \c Domain next_domain~d(domain~d); ', [Index, AIndex] ). generate_sub_formula('F'(A), Index) :- sub_formula(A, AIndex), format( ' \c Domain next_domain~d(domain~d); for ( Domain::iterator j = next_domain~d.begin(); j != next_domain~d.end(); ++j ) { next_domain~d.add_disjunct(j->pointset()); } ', [Index, Index, AIndex, AIndex, Index] ). generate_sub_formula('G'(A), Index) :- sub_formula(A, AIndex), format( ' \c Domain next_domain~d(domain~d); next_domain~d.intersection_assign(next_domain~d); ', [Index, Index, Index, AIndex] ). generate_sub_formula('U'(A, B), Index) :- generate_sub_formula_u_or_w(A, B, Index). generate_sub_formula('W'(A, B), Index) :- generate_sub_formula_u_or_w(A, B, Index). generate_sub_formula('R'(A, B), Index) :- generate_sub_formula_u_or_w(A, B, Index). generate_sub_formula(A /\ B, Index) :- sub_formula(A, AIndex), sub_formula(B, BIndex), format( ' \c Domain next_domain~d(next_domain~d); next_domain~d.intersection_assign(next_domain~d); ', [Index, AIndex, Index, BIndex] ). generate_sub_formula(A \/ B, Index) :- sub_formula(A, AIndex), sub_formula(B, BIndex), format(' Domain next_domain~d(next_domain~d); for ( Domain::iterator j = next_domain~d.begin(); j != next_domain~d.end(); ++j ) { next_domain~d.add_disjunct(j->pointset()); } ', [Index, AIndex, BIndex, BIndex, Index] ). generate_sub_formula(exists(X, A), Index) :- sub_formula(A, AIndex), free_variable_index(X, XIndex), format(' Domain next_domain~d(next_domain~d); next_domain~d.unconstrain(x~d); ', [Index, AIndex, Index, XIndex] ). generate_sub_formula(not(_A), _Index) :- throw(error('LTL \'not\' is not implemented yet')). % ??? generate_sub_formula_u_or_w(A, B, Index) :- sub_formula(A, AIndex), sub_formula(B, BIndex), format(' Domain next_domain~d(domain~d); next_domain~d.intersection_assign(next_domain~d); for ( Domain::iterator j = next_domain~d.begin(); j != next_domain~d.end(); ++j ) { next_domain~d.add_disjunct(j->pointset()); } ', [Index, Index, Index, AIndex, BIndex, BIndex, Index] ). generate_expression(Number) :- number(Number), !, format('~w', [Number]). generate_expression(A) :- free_variable_index(A, Index), !, format('x~d', [Index]). generate_expression(A) :- ( column(A, Index) ; A = [Object], column(Object, Index) ), !, format('(*i)[~d]', [Index]). generate_expression(A^B) :- !, write('pow('), generate_expression(A), write(', '), generate_expression(B), write(')'). generate_expression(Expression) :- binary_operator(Expression, A, Op, B), !, generate_expression_with_parentheses(A), write(Op), generate_expression_with_parentheses(B). binary_predicate(A = B, A, '==', B). binary_predicate(A <> B, A, '!=', B). binary_predicate(A << B, A, '<<', B). binary_predicate(A >> B, A, '>>', B). binary_predicate(A < B, A, '<', B). binary_predicate(A <= B, A, '<=', B). binary_predicate(A > B, A, '>', B). binary_predicate(A >= B, A, '>=', B). binary_operator(A + B, A, '+', B). binary_operator(A - B, A, '-', B). binary_operator(A * B, A, '*', B). binary_operator(A / B, A, '/', B). check_linearity(Formula) :- grammar_iter( foltl, [foltl_expression: foltl:check_linearity_expression], Formula ). check_linearity_expression(Expression) :- ( Expression = A + B ; Expression = A - B ), !, check_linearity_expression(A), check_linearity_expression(B). check_linearity_expression(Expression) :- Expression = A * B, !, ( has_variable(A), has_variable(B) -> throw(error(not_linear(Expression))) ; true ). check_linearity_expression(Expression) :- Expression = A ^ B, !, ( ( has_variable(A) ; has_variable(B) ) -> throw(error(not_linear(Expression))) ; true ). check_linearity_expression(Expression) :- Expression = A / B, !, ( has_variable(B) -> throw(error(not_linear(Expression))) ; true ), check_linearity_expression(A). check_linearity_expression(_). prolog:message(error(not_linear(Expression))) --> ['Not linear: ~p'-[Expression]]. generate_expression_with_parentheses(A) :- write('('), generate_expression(A), write(')'). has_variable(A) :- binary_operator(A, Left, _Op, Right), !, ( has_variable(Left) ; has_variable(Right) ). has_variable(A) :- is_free_variable(A). is_free_variable(A) :- free_variable_index(A, _Index). declare_free_variables(Formula) :- grammar_iter( foltl, [name: foltl:declare_free_variable_name], Formula ). declare_free_variable_name(X) :- ( column(X, _) -> true ; free_variable_index(X, _Index) -> true ; count(free_variables, Index), asserta(free_variable_index(X, Index)), format(' PPL::Variable x~d(~d);\n', [Index, Index]) ). declare_formula(Formula) :- declare_formula(Formula, _Index). declare_formula(Formula, Index) :- ( ( Formula = 'G'(_) ; Formula = 'W'(_, _) ) -> Initial = 'PPL::UNIVERSE' ; Initial = 'PPL::EMPTY' ), declare_sub_formulae(Formula), index_formula(Formula, Initial, Index). declare_sub_formulae(Formula) :- grammar_iter( foltl, [foltl: foltl:declare_formula], Formula ). index_formula(Formula, Initial, Index) :- ( sub_formula(Formula, Index) -> true ; peek_count(free_variables, FreeVariableCount), count(sub_formulae, Index), assertz(sub_formula(Formula, Index)), format( ' Domain domain~d(~d, ~a);\n', [Index, FreeVariableCount, Initial] ) ). compile_domain_cpp_program(CppProgram, ExecutableFilename) :- ppl_compile_options(PplCompileOptions), compile_cpp_program( [CppProgram, 'csv_reader.o'], PplCompileOptions, ExecutableFilename ). reformat_domain({ Conjunction0 }, Conjunction1) :- reformat_domain_conjunction(Conjunction0, Conjunction1). reformat_domain((A0, B0), B1 \/ A1) :- % reversed order reformat_domain(A0, A1), reformat_domain(B0, B1). reformat_domain(false, false). reformat_domain(true, true). reformat_ppl(A, B, K, X) :- (number(B), (((A = -X), (K = -1)) ; (A=(K * X), number(K)))). % PPL variable domain normal form reformat_domain_conjunction(A0 = B0, R) :- reformat_expression(A0, A1), reformat_expression(B0, B1), ( reformat_ppl(A1, B1, K, X) -> Z is B1/K, R=(X = Z) ; R=(A1 = B1) ). reformat_domain_conjunction(A0 < B0, A1 < B1) :- reformat_expression(A0, A1), reformat_expression(B0, B1). reformat_domain_conjunction(A0 <= B0, A1 <= B1) :- reformat_expression(A0, A1), reformat_expression(B0, B1). reformat_domain_conjunction(A0 > B0, R) :- reformat_expression(A0, A1), reformat_expression(B0, B1), ( reformat_ppl(A1, B1, K, X) -> Z is B1/K, ( K<0 -> R=(X < Z) ; R=(X > Z) ) ; R=(A1 > B1) ). reformat_domain_conjunction(A0 >= B0, R) :- reformat_expression(A0, A1), reformat_expression(B0, B1), ( reformat_ppl(A1, B1, K, X) -> Z is B1/K, ( K<0 -> R=(X <= Z) ; R=(X >= Z) ) ; R=(A1 >= B1) ). reformat_domain_conjunction((A0, B0), B1 /\ A1) :- % reversed order reformat_domain_conjunction(A0, A1), reformat_domain_conjunction(B0, B1). reformat_expression(-E0, -E1) :- !, reformat_expression(E0, E1). reformat_expression(E0 + F0, E1 + F1) :- !, reformat_expression(E0, E1), reformat_expression(F0, F1). reformat_expression(E0 - F0, E1 - F1) :- !, reformat_expression(E0, E1), reformat_expression(F0, F1). reformat_expression(E0 * F0, E1 * F1) :- !, reformat_expression(E0, E1), reformat_expression(F0, F1). reformat_expression(E0 / F0, E1 / F1) :- !, reformat_expression(E0, E1), reformat_expression(F0, F1). reformat_expression(Number, Number) :- number(Number), !. reformat_expression(DimensionName, X) :- atom(DimensionName), !, atom_length(DimensionName, NameLength), ( NameLength > 1 -> sub_atom(DimensionName, 0, 1, _, Letter), sub_atom(DimensionName, 1, _, 0, Counter), letter_index(Letter, LetterIndex), Index is Counter * 26 + LetterIndex ; letter_index(DimensionName, Index) ), once(free_variable_index(X, Index)). letter_index(Letter, Index) :- once(sub_atom('ABCDEFGHIJKLMNOPQRSTUVWXYZ', Index, 1, _, Letter)).