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 |