1		% (c) 2009-2025 Lehrstuhl fuer Softwaretechnik und Programmiersprachen,
2		% Heinrich Heine Universitaet Duesseldorf
3		% This software is licenced under EPL 1.0 (http://www.eclipse.org/org/documents/epl-v10.html)
4
5		:- module(succeed_max,[reset_max_reached/0, reset_max_reached/1,
6		max_reached/0, max_reached/1,
7		succeed_max_call/2, succeed_max_call_id/3,
8		succeed_max_initialise/0,
9		assert_max_reached/1 % mainly for operation caching
10		]).
11
12		:- use_module(tools).
13
14		:- use_module(module_information).
15		:- module_info(group,infrastructure).
16		:- module_info(description,'This module provides a meta call to retrieve a specified maximum number of solutions.').
17
18		:- use_module(extension('counter/counter'),
19		[counter_init/0, new_counter/1, inc_counter/2, reset_counter/1]).
20
21		:- dynamic max_reached/1.
22
23		max_reached :- max_reached(_),!.
24
25		% assert that for Id a maximum number of solutions was reached,
26		% typically Id is an operation name; meaning that not all transitions were computed for it
27		assert_max_reached(Id) :-
28		(max_reached(Id) -> true ; assertz(max_reached(Id))).
29
30		reset_max_reached(Id) :- retractall(max_reached(Id)).
31		reset_max_reached :-
32		(retract(max_reached(_)) -> retractall(max_reached(_)) ; true). % retractall seems sometimes expensive in SICStus
33
34		:- meta_predicate succeed_max_call(0,-).
35		:- meta_predicate succeed_max_call_id(+,0,-).
36
37		succeed_max_call(Call,MaxNrOfSols) :-
38		succeed_max_call_id('$unknown',Call,MaxNrOfSols).
39
40
41		succeed_max_initialise :- counter_init,new_counter(inits_found),new_counter(constants_found),new_counter(ops_found).
42
43		:- use_module(eventhandling,[register_event_listener/3]).
44		:- register_event_listener(specification_initialised,succeed_max_initialise,
45		'Initialise sols_found counter.').
46
47		succeed_max_call_id(Id,Call,MaxNrOfSols) :-
48		get_counter_name(Id,Counter),
49		reset_counter(Counter),
50		succeed_max_call_id_aux(Id,Counter,Call,MaxNrOfSols).
51
52		succeed_max_call_id_aux(Id,_,_Call,MaxNrOfSols) :-
53		MaxNrOfSols==0,!,
54		assert_max_reached(Id),fail.
55		succeed_max_call_id_aux(Id,Counter,Call,MaxNrOfSols) :- %print_message(max_call(Call,MaxnrOfSols)),
56		call(Call),
57		inc_counter(Counter,X1),
58		% print_message(sol(X1)), %
59		(X1>=MaxNrOfSols
60		-> (!, %print_message(max_sol_found(Call,X1,MaxNrOfSols)),
61		assert_max_reached(Id)
62		)
63		; true).
64
65		% use different counters so that we can have at least one of each succeed_max_call pending without interaction
66		get_counter_name(V,Name) :- var(V),!, Name=ops_found.
67		get_counter_name('$initialise_machine',Name) :- !, Name=inits_found.
68		get_counter_name('$setup_constants',Name) :- !,Name=constants_found.
69		get_counter_name(_,ops_found).
70