1 :- module(logging,[synthesis_log/1,disable_logging/0,enable_logging/0]).
2
3 :- use_module(probsrc(translate),[print_bexpr/1,print_bexpr_or_subst/1]).
4
5 :- use_module(library(lists)).
6
7 :- dynamic enabled/1.
8 :- volatile enabled/1.
9
10 enabled(false).
11
12 disable_logging :-
13 retractall(enabled(_)) ,
14 assertz(enabled(false)).
15
16 enable_logging :-
17 retractall(enabled(_)) ,
18 assertz(enabled(true)).
19
20 synthesis_log(LoggingPredicate) :-
21 (enabled(true) ; LoggingPredicate =.. [solution|_]) ,
22 synthesis_log_aux(LoggingPredicate) , !.
23 synthesis_log(_) :- !.
24
25 synthesis_log_aux(solution_tuple(ProgramAST1,ProgramAST2)) :-
26 format("~nFound two eventually equivalent solutions:~n~w~n",[ProgramAST1]) ,
27 nl , print_bexpr_or_subst(ProgramAST1) , nl ,
28 print_bexpr_or_subst(ProgramAST2) , nl.
29
30 synthesis_log_aux(solution(_,none)) :-
31 format("~nSynthesis failed.~n",[]).
32 synthesis_log_aux(solution(_,state(State))) :-
33 format("~nDistinguishing State: ~w~n",[State]).
34 synthesis_log_aux(solution(_,transition(InputState,OutputState))) :-
35 format("~nDistinguishing Transition: ~w --> ~w~n",[InputState,OutputState]).
36 synthesis_log_aux(solution(Type,Solution)) :-
37 synthesis_log_aux(solution_enter(Type)) ,
38 synthesis_log_aux(solution_aux1(Type,Solution)).
39 % Solution can be a list of actions.
40 synthesis_log_aux(solution_aux1(action,Action)) :-
41 \+is_list(Action) , ! ,
42 synthesis_log_aux(solution_aux2(action,[Action])).
43 synthesis_log_aux(solution_aux1(action,Actions)) :-
44 synthesis_log_aux(solution_aux2(action,Actions)).
45 synthesis_log_aux(solution_aux1(Type,Solution)) :-
46 Type \= action ,
47 print_bexpr_or_subst(Solution) , nl.
48 synthesis_log_aux(solution_aux2(action,[])).
49 synthesis_log_aux(solution_aux2(action,[Action|T])) :-
50 print_bexpr_or_subst(Action) , nl ,
51 synthesis_log_aux(solution_aux2(action,T)).
52
53 synthesis_log_aux(solution_enter(Type)) :-
54 (Type = action -> PrintType = operation ; PrintType = Type) ,
55 format("~nSynthesized ~w:~n",[PrintType]).
56
57 synthesis_log_aux(symmetry_reduction(SymmetryReduction)) :-
58 format("~nSymmetry reduction:~n",[]) ,
59 print_bexpr(SymmetryReduction) , nl.
60
61 synthesis_log_aux(relax_guard(OpName)) :-
62 format("~nStart synthesizing relaxed guard for operation ~w ~n",[OpName]).
63
64 synthesis_log_aux(invariant_violation_initialisation_state(Init)) :-
65 format("~nInvariant violation in initialisation state ~w",[Init]).
66
67 synthesis_log_aux(invariant_violation_found(State,Operation)) :-
68 format("~nInvariant violation in state ~w, caused by operation ~w ~n",[State,Operation]).
69
70 synthesis_log_aux(involved_variables(VarNames)) :-
71 format("~nVariables involved in invariant violation: ~w.~n",[VarNames]).
72
73 synthesis_log_aux(synthesize_new_guard_if_loop) :-
74 format("~nSynthesize new precondition for an operation that fits the current example.~n",[]).
75
76 synthesis_log_aux(distinguishing_constraint(Type,Constraint)) :-
77 format("~nDistinguishing constraint for type ~w:~n",[Type]) ,
78 print_bexpr(Constraint) , nl.
79
80 synthesis_log_aux(distinguishing_transition_cache_changed(DistTransitionCache,DistTransitionCache)).
81 synthesis_log_aux(distinguishing_transition_cache_changed(DistTransitionCache,NewDistTransitionCache)) :-
82 DistTransitionCache \= NewDistTransitionCache ,
83 format("~nCache has changed:~n",[]) ,
84 print_bexpr(DistTransitionCache) , nl.
85
86 synthesis_log_aux(expand_library) :-
87 format("~nExpand library.~n",[]).
88
89 synthesis_log_aux(two_non_equivalent_solutions(Type,Solution,FurtherSolution)) :-
90 format("~nFound two non equivalent ~w~nSolution: ~w~nFurther solution: ~w~n",[Type,Solution,FurtherSolution]).
91
92 synthesis_log_aux(distinguishing_error(error,ProgramAST,ProgramAST2)) :-
93 format("~nError when searching for a distinguishing input for programs ~w~n~w~n~n",[ProgramAST,ProgramAST2]).
94 synthesis_log_aux(distinguishing_error(_,_,_)).
95
96 synthesis_log_aux(start_synthesis_loop(DistTransitionCache,DistStateCache,Library,LibExpansion,CurrentVars,PreCondVars,
97 ValidInvariantsOrGuards,Type,PosInput,NegInput,LocationVars,M1,ParameterAmount,Solution)) :-
98 format("~nEnter synthesis loop for type ~w.~n",[Type]) ,
99 format("Distinguishing transition cache: ~w~nDistinguishing state cache: ~w~nLibrary: ~w~nLibrary expansion: ~w~n",
100 [DistTransitionCache,DistStateCache,Library,LibExpansion]) ,
101 format("Current variables: ~w~nVariables affected in simultaneous guard (only for operations): ~w~n",[CurrentVars,PreCondVars]) ,
102 (Type = action
103 -> format("Valid invariants or guards: ~w~nInput: ~w~nOutput: ~w~nLocation variables: ",[ValidInvariantsOrGuards,PosInput,NegInput])
104 ; format("Valid invariants or guards: ~w~nPositive: ~w~nNegative: ~w~nLocation variables: ",[ValidInvariantsOrGuards,PosInput,NegInput])) ,
105 print_location_variables(LocationVars) ,
106 pp_io(PosInput,NegInput) ,
107 format("Line amount (M1): ~w~nParameter amount: ~w~nSolution: ~w~n",[M1,ParameterAmount,Solution]).
108
109 synthesis_log_aux(location_vars_to_program_and_fail(Type,Library,LocationVarsIn,LocationVarsOut,Parameter,Solution)) :-
110 format("~nERROR: location_vars_to_program/9 failed, probably a wrong library configuration or the line amount does not fit the library size.~n",[]) ,
111 format("Type: ~w~nLibrary: ~w~nLocationVarsIn: ~w~nLocationVarsOut: ~w~nParameter: ~w~n,Solution: ~w~n.",
112 [Type,Library,LocationVarsIn,LocationVarsOut,Parameter,Solution]) , !.
113
114 % this should be fixed and will hopefully never happen again, just to make sure
115 synthesis_log_aux(defective_further_solution_and_fail(Type,NewBehavioralConstraint,FurtherSolution,PosInput,NegInput,LocationVars,ProgramAST)) :-
116 Type \= action ,
117 FurtherSolution = solution(_) ,
118 ProgramAST = b(_,integer,_) , ! ,
119 format("~nError found in further solution.~n",[]) ,
120 format("Positive States: ~w~nNegative States: ~w~nFurther solution: ~w~nLocation variables: ~w~nBehavioral constraint:",
121 [PosInput,NegInput,FurtherSolution,LocationVars]) ,
122 print_bexpr(NewBehavioralConstraint) , nl , !.
123 synthesis_log_aux(defective_further_solution_and_fail(_,_,_,_,_,_,_)).
124
125 synthesis_log_aux(solve_distinguishing_constraint(DistConstraint,Solver)) :-
126 format("Try to find a distinguishing example:~nSolver: ~w~nDistinguishing constraint:~n",[Solver]) ,
127 translate:print_bexpr(DistConstraint) , nl ,
128 print(DistConstraint) , nl , nl.
129
130 pp_io(PosInput,NegInput) :-
131 format("Positive Examples:~n",[]) ,
132 pp_io_aux(0,PosInput) ,
133 format("Negative Examples:~n",[]) ,
134 pp_io_aux(0,NegInput).
135
136 pp_io_aux(_,[]).
137 pp_io_aux(C,[Example|T]) :-
138 format("Example #~w:~n",[C]) ,
139 pp_state(Example) ,
140 C1 is C + 1 ,
141 pp_io_aux(C1,T).
142
143 pp_state([]).
144 pp_state([IdValueAst|T]) :-
145 IdValueAst = b(_,_,Info) ,
146 member(synthesis(machinevar,VarName),Info) ,
147 format(" ~w:",[VarName]) ,
148 print_bexpr(IdValueAst) , nl ,
149 pp_state(T).
150
151 print_location_variables([]).
152 print_location_variables([LocationVar|T]) :-
153 print(LocationVar) , nl ,
154 print_location_variables(T).