1 % (c) 2009-2024 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,
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 :-
61 (loaded(_) -> true
62 ; assertz(loaded(failure)),
63 %assert_dir,
64 assertz(user:library_directory('.')),
65 (safe_load_foreign_resource(counter,counter) %load_foreign_resource(counter)
66 -> retractall(loaded(_)),
67 assertz(loaded(success))
68 ; format(user_output,"You can set the environment variable prob_c_counter to false to avoid using the counter C++ library~n",[])
69 )
70 ).
71
72 inc_counter_by(Counter,1) :- !,
73 inc_counter(Counter,_).
74 inc_counter_by(Counter,Incr) :-
75 get_counter(Counter,Old),
76 New is Old+Incr,
77 set_counter(Counter,New).
78
79 %-----------------------
80 :- else.
81 %-----------------------
82
83 :- write('Using Prolog counter instead of C++ extension'),nl.
84
85 % Pure Prolog implementation for compatibility.
86
87 % we now use the SICStus blackboard primitives; they are also available in SWI when using expects_dialect(sicstus4).
88 % we have to ensure there are no clashes with other uses of bb_put, bb_get, ...
89 % currently only memoization.pl uses it in profiling mode
90
91 % Previously we used assertz/retract
92 % 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
93 % blackboard primitives ensure atomic updates out-of-the-box
94
95
96 counter_init.
97
98 get_counter(Counter,Value) :- bb_get(Counter,Value).
99
100 set_counter(Counter, Value) :- bb_update(Counter,_,Value).
101
102 new_counter(Counter) :- bb_put(Counter,0).
103
104 reset_counter(Counter) :- bb_put(Counter,0).
105
106 inc_counter(Counter, New) :- bb_get(Counter,Old), New is Old+1, bb_update(Counter,_,New).
107
108 inc_counter_by(Counter, Incr) :- bb_get(Counter,Old), New is Old+Incr, bb_update(Counter,_,New).
109
110 % probably we should throw an exception:
111 next_float_twoards(Float,Float2,R) :-
112 format(user_error,'*** Not implemented: ~w~n',[next_float_twoards(Float,Float2,R)]), R=Float2.
113 next_smaller_abs_float(Float,R) :-
114 format(user_error,'*** Not implemented: ~w~n',[next_smaller_abs_float(Float,R)]), R=Float.
115 next_larger_float(Float,R) :-
116 format(user_error,'*** Not implemented: ~w~n',[next_larger_float(Float,R)]), R=Float.
117 next_smaller_float(Float,R) :-
118 format(user_error,'*** Not implemented: ~w~n',[next_smaller_float(Float,R)]), R=Float.
119
120 largest_float(R) :- R is 1.7976931348623157E+308.
121 smallest_float(R) :- R is -1.7976931348623157E+308.
122 smallest_abs_float(R) :- R is 5.0E-324.
123
124
125 :- endif.
126 %-----------------------
127
128 % code for both versions:
129
130 inc_counter(Counter) :-
131 inc_counter(Counter, _NewVal).
132
133
134 % :- statistics(walltime,_),counter:new_counter(bench), repeat, counter:inc_counter(bench,N), N>1000000, statistics(walltime,[_,W]), print(W),nl.
135 % C: 465 - 467 ms, Prolog: 721 - 728 ms, SWI Prolog 1955-1960 ms
136 % C dropped to 259 - 266 ms when dropping checking for inc_counter
137
138 % :- 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.
139 % around 590 ms -> faster than assertz; we should use this for the Prolog counter !
140 % around 396 in SWI!
141
142 % 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.
143 % C : 451 - 459 ms, Prolog: 1306 - 1342 ms
144
145
146 % a good probcli performance test is this one:
147 % probcli ../prob_examples/public_examples/B/PerformanceTests/ModelChecking/Lift_1Million.mch -mc 100000 -disable-time-out