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(counter, [
6 counter_init/0, counter_init/1,
7 new_counter/1,
8 get_counter/2,
9 set_counter/2,
10 inc_counter/1, inc_counter/2,
11 inc_counter_by/2,
12 reset_counter/1,
13
14 % utilities for counting up/down floats:
15 next_smaller_abs_float/2, % next smaller float towards 0
16 next_smaller_float/2, % towards -INFINITY
17 next_larger_float/2, % larger toward +INFINITY
18 next_float_twoards/3,
19 smallest_float/1,
20 largest_float/1,
21 smallest_abs_float/1
22 ]).
23
24 :- load_files(library(system), [when(compile_time), imports([environ/2])]).
25 :- (environ(prob_c_counter,X) -> format('environ(prob_c_counter,~w)~n',[X]) ; true).
26
27 :- if((predicate_property(load_foreign_resource(_), _), \+ environ(prob_c_counter,false))).
28
29 % C implementation of counter for better performance on SICStus.
30 % A good test is 1748, where this gains maybe 1 second for 22 second model checking time
31
32 foreign_resource('counter', [new_counter,get_counter,inc_counter,set_counter,reset_counter,
33 next_float_twoards,
34 next_smaller_abs_float, next_smaller_float, next_larger_float,
35 largest_float, smallest_float, smallest_abs_float]).
36 foreign(new_counter, c, new_counter(+atom)).
37 foreign(get_counter, c, get_counter(+atom, [-integer])).
38 foreign(inc_counter, c, inc_counter(+atom, [-integer])).
39 foreign(set_counter, c, set_counter(+atom, +integer)).
40 foreign(reset_counter, c, reset_counter(+atom)).
41
42 % not really counting: it is counting up/down floats:
43 foreign(next_float_twoards, c, next_float_twoards(+float,+float,[-float])).
44 foreign(next_smaller_abs_float, c, next_smaller_abs_float(+float,[-float])).
45 foreign(next_smaller_float, c, next_smaller_float(+float,[-float])).
46 foreign(next_larger_float, c, next_larger_float(+float,[-float])).
47 foreign(largest_float, c, largest_float([-float])).
48 foreign(smallest_float, c, smallest_float([-float])).
49 foreign(smallest_abs_float, c, smallest_abs_float([-float])).
50
51 % with this line below we need to adapt the Makefile to include the counter resource in the binary:
52 % (maybe this is a good idea)
53 % :- load_foreign_resource(counter).
54
55
56 :- use_module(probsrc(pathes_lib),[safe_load_foreign_resource/2]).
57
58 :- dynamic loaded/1.
59
60 counter_init :- counter_init(_).
61
62 counter_init(Result) :-
63 (loaded(R) -> Result=R
64 ; assertz(loaded(failure_to_load)),
65 %assert_dir,
66 assertz(user:library_directory('.')),
67 (safe_load_foreign_resource(counter,counter) %load_foreign_resource(counter)
68 -> retractall(loaded(_)),
69 assertz(loaded(success)),
70 Result = success
71 ; format(user_output,"Set environment variable prob_c_counter to false to avoid using counter C++ library.~n",[]),
72 format(user_output,"Using fallback Prolog implementation for counter.~n",[]),
73 format(user_output,"Float solver and external functions RNEXT, RPEV *not* available!~n",[]),
74 assert((get_counter(Counter,Value) :- bb_get(Counter,Value))),
75 assert((set_counter(Counter, Value) :- bb_update(Counter,_,Value))),
76 assert((new_counter(Counter) :- bb_put(Counter,0))),
77 assert((reset_counter(Counter) :- bb_put(Counter,0))),
78 assert((inc_counter(Counter, New) :- bb_get(Counter,Old), New is Old+1, bb_update(Counter,_,New))),
79 Result = failure_to_load
80 )
81 ).
82
83 inc_counter_by(Counter,1) :- !,
84 inc_counter(Counter,_).
85 inc_counter_by(Counter,Incr) :-
86 get_counter(Counter,Old),
87 New is Old+Incr,
88 set_counter(Counter,New).
89
90 %-----------------------
91 :- else.
92 %-----------------------
93
94 :- write('Using Prolog counter instead of C++ extension'),nl.
95
96 % Pure Prolog implementation for compatibility.
97
98 % we now use the SICStus blackboard primitives; they are also available in SWI when using expects_dialect(sicstus4).
99 % we have to ensure there are no clashes with other uses of bb_put, bb_get, ...
100 % currently only memoization.pl uses it in profiling mode
101
102 % Previously we used assertz/retract
103 % Note: we first set new value before we retract old value to ensure we have no problem if time-out/CTRL-C happens in th emiddle; maybe we can use clause references to make this efficient
104 % blackboard primitives ensure atomic updates out-of-the-box
105
106
107 counter_init.
108 counter_init(success).
109
110 get_counter(Counter,Value) :- bb_get(Counter,Value).
111
112 set_counter(Counter, Value) :- bb_update(Counter,_,Value).
113
114 new_counter(Counter) :- bb_put(Counter,0).
115
116 reset_counter(Counter) :- bb_put(Counter,0).
117
118 inc_counter(Counter, New) :- bb_get(Counter,Old), New is Old+1, bb_update(Counter,_,New).
119
120 inc_counter_by(Counter, Incr) :- bb_get(Counter,Old), New is Old+Incr, bb_update(Counter,_,New).
121
122 % probably we should throw an exception:
123 next_float_twoards(Float,Float2,R) :-
124 format(user_error,'*** Not implemented: ~w~n',[next_float_twoards(Float,Float2,R)]), R=Float2.
125 next_smaller_abs_float(Float,R) :-
126 format(user_error,'*** Not implemented: ~w~n',[next_smaller_abs_float(Float,R)]), R=Float.
127 next_larger_float(Float,R) :-
128 format(user_error,'*** Not implemented: ~w~n',[next_larger_float(Float,R)]), R=Float.
129 next_smaller_float(Float,R) :-
130 format(user_error,'*** Not implemented: ~w~n',[next_smaller_float(Float,R)]), R=Float.
131
132 largest_float(R) :- R is 1.7976931348623157E+308.
133 smallest_float(R) :- R is -1.7976931348623157E+308.
134 smallest_abs_float(R) :- R is 5.0E-324.
135
136
137 :- endif.
138 %-----------------------
139
140 % code for both versions:
141
142 inc_counter(Counter) :-
143 inc_counter(Counter, _NewVal).
144
145
146 % :- statistics(walltime,_),counter:new_counter(bench), repeat, counter:inc_counter(bench,N), N>1000000, statistics(walltime,[_,W]), print(W),nl.
147 % C: 465 - 467 ms, Prolog: 721 - 728 ms, SWI Prolog 1955-1960 ms
148 % C dropped to 259 - 266 ms when dropping checking for inc_counter
149
150 % :- statistics(walltime,_),bb_put(b,0), repeat, bb_get(b,C),C1 is C+1, bb_update(b,_,C1), C1>1000000, statistics(walltime,[_,W]), print(W),nl.
151 % around 590 ms -> faster than assertz; we should use this for the Prolog counter !
152 % around 396 in SWI!
153
154 % statistics(walltime,_),counter:new_counter(b), counter:new_counter(c), repeat,counter:set_counter(c,0), counter:inc_counter(b,N), N>1000000, statistics(walltime,[_,W]), print(W),nl.
155 % C : 451 - 459 ms, Prolog: 1306 - 1342 ms
156
157
158 % a good probcli performance test is this one:
159 % probcli ../prob_examples/public_examples/B/PerformanceTests/ModelChecking/Lift_1Million.mch -mc 100000 -disable-time-out