| 1 | % (c) 2021-2026 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(simb_simulator,[run_simb_simulation/1, run_simb_simulation/2, | |
| 6 | simb_initial_state/1, | |
| 7 | simb_perform_step/5, simb_perform_visible_step/5, | |
| 8 | simb_update_current_state_id/3, get_simb_current_state_id/2, | |
| 9 | get_simb_delay_until_next_step/2, get_simb_time/2, | |
| 10 | get_simb_next_activation_term/3, | |
| 11 | get_simb_scheduling_entry/5, | |
| 12 | portray_simb_state/1, get_simb_scheduling_table_info/2, | |
| 13 | print_simb_profile/0]). | |
| 14 | ||
| 15 | ||
| 16 | :- use_module(probsrc(error_manager)). | |
| 17 | :- use_module(probsrc(debug)). | |
| 18 | :- use_module(probsrc(tools_json)). | |
| 19 | :- use_module(probsrc(tools), [ajoin/2]). | |
| 20 | :- use_module(extrasrc(json_parser),[json_parse_file/3]). | |
| 21 | :- use_module(library(lists)). | |
| 22 | :- use_module(probsrc(tools),[safe_number_codes/2]). | |
| 23 | :- use_module(library(avl)). | |
| 24 | :- use_module(library(heaps)). | |
| 25 | :- use_module(simb_parser,[simb_activation_id/1, simb_activation_kind/2, | |
| 26 | simb_activation_priority/2, simb_activation_effect/6, simb_activation_options/2]). | |
| 27 | ||
| 28 | ||
| 29 | :- use_module(probsrc(tools),[start_ms_timer/1, stop_ms_timer_with_msg/2, get_elapsed_walltime/2]). | |
| 30 | :- use_module(extension('counter/counter')). | |
| 31 | :- use_module(probsrc(eventhandling),[register_event_listener/3]). | |
| 32 | ||
| 33 | simb_counters([simb_nr_simulations,simb_nr_steps,simb_skip_steps,simb_simulation_time, | |
| 34 | simb_deadlock_reached, simb_max_nr_steps_reached, | |
| 35 | simb_max_simulation_time_reached,simb_ltl_stop_condition_reached]). | |
| 36 | ||
| 37 | simb_startup :- % call once at startup to ensure all counters exist | |
| 38 | counter_init, | |
| 39 | simb_counters(Cs), | |
| 40 | maplist(new_counter,Cs). | |
| 41 | ||
| 42 | simb_reset :- simb_counters(Cs), maplist(reset_counter,Cs), | |
| 43 | retractall(time_stats(_,_)), | |
| 44 | retractall(hit_stats(_,_,_)). | |
| 45 | ||
| 46 | print_simb_profile :- | |
| 47 | get_counter(simb_nr_simulations,Total), | |
| 48 | format('SimB Simulation Statistics~n',[]), | |
| 49 | simb_counters(Cs), | |
| 50 | maplist(print_counter(Total),Cs), | |
| 51 | portray_hits. | |
| 52 | ||
| 53 | average_counter(simb_simulation_time). | |
| 54 | average_counter(simb_nr_steps). | |
| 55 | average_counter(simb_skip_steps). | |
| 56 | percentage_counter(simb_max_nr_steps_reached). | |
| 57 | percentage_counter(simb_max_simulation_time_reached). | |
| 58 | percentage_counter(simb_ltl_stop_condition_reached). | |
| 59 | percentage_counter(simb_deadlock_reached). | |
| 60 | ||
| 61 | print_counter(Total,C) :- Total>0, | |
| 62 | average_counter(C),!, | |
| 63 | get_counter(C,Nr), | |
| 64 | Avg is Nr / Total, | |
| 65 | format(' ~w : ~w (average: ~1f)~n',[C,Nr,Avg]). | |
| 66 | print_counter(Total,C) :- Total>0, | |
| 67 | percentage_counter(C),!, | |
| 68 | get_counter(C,Nr), | |
| 69 | Perc is 100*Nr / Total, | |
| 70 | format(' ~w : ~w (~1f %)~n',[C,Nr,Perc]). | |
| 71 | print_counter(_,C) :- get_counter(C,Nr), | |
| 72 | (time_stats(C,Time) | |
| 73 | -> (Nr>0 -> Avg is Time / Nr ; Avg = '?'), | |
| 74 | format(' ~w : ~w (total walltime ~w ms, average: ~1f ms)~n',[C,Nr,Time,Avg]) | |
| 75 | ; format(' ~w : ~w~n',[C,Nr]) | |
| 76 | ). | |
| 77 | ||
| 78 | :- dynamic time_stats/2. | |
| 79 | register_time(Counter,Time) :- retract(time_stats(Counter,OldTime)),!, | |
| 80 | NewTime is OldTime+Time, assert(time_stats(Counter,NewTime)). | |
| 81 | register_time(Counter,Time) :- assert(time_stats(Counter,Time)). | |
| 82 | ||
| 83 | :- dynamic hit_stats/3. | |
| 84 | register_hit(OpName,Kind) :- retract(hit_stats(OpName,Kind,OldCount)),!, | |
| 85 | NewCount is OldCount+1, assert(hit_stats(OpName,Kind,NewCount)). | |
| 86 | register_hit(OpName,Kind) :- assert(hit_stats(OpName,Kind,1)). | |
| 87 | ||
| 88 | portray_hit(h(Kind,Op,C)) :- format('~w ~w : ~w~n',[Op,Kind,C]). | |
| 89 | portray_hits :- findall(h(Kind,Op,C),hit_stats(Op,Kind,C),List), | |
| 90 | sort(List,SList), maplist(portray_hit,SList). | |
| 91 | ||
| 92 | :- register_event_listener(startup_prob,simb_startup, | |
| 93 | 'Initialise SimB Counters and Statistics.'). | |
| 94 | :- register_event_listener(reset_specification,simb_reset, | |
| 95 | 'Reset SimB Statistics.'). | |
| 96 | ||
| 97 | ||
| 98 | % running a SimB simulation for a number of steps | |
| 99 | % at the moment ignores after attribute; TODO: also provide maximum time and options (real_time, update_history,...) | |
| 100 | run_simb_simulation(MaxSteps) :- | |
| 101 | Options = [simulation_speed/1], | |
| 102 | run_simb_simulation(MaxSteps,Options). | |
| 103 | run_simb_simulation(MaxSteps,Options) :- | |
| 104 | get_initial_scheduling_table(InitialTable), | |
| 105 | inc_counter(simb_nr_simulations,_NrSim), | |
| 106 | start_ms_timer(Start), | |
| 107 | CurrentTime = 0, % TODO: we could use current walltime | |
| 108 | %(_NrSim>1 -> set_prolog_flag(profiling,on) ; true), | |
| 109 | run_simb(root,InitialTable,CurrentTime,0,MaxSteps,Options), | |
| 110 | %(_NrSim>1 -> print_profile,trace ; true), | |
| 111 | %ajoin(['SimB simulation ',_NrSim,': '],Msg), | |
| 112 | %stop_ms_timer_with_msg(Start,Msg), | |
| 113 | get_elapsed_walltime(Start,Delta), | |
| 114 | register_time(simb_nr_simulations,Delta). | |
| 115 | ||
| 116 | get_initial_scheduling_table(InitialTable) :- | |
| 117 | empty_scheduling_table(E), | |
| 118 | InitialList = ['$setup_constants','$initialise_machine'], | |
| 119 | schedule_activations(InitialList,E,InitialTable), | |
| 120 | (InitialTable=E -> add_message(simb,'No activations defined for : ',InitialList) ; true). | |
| 121 | ||
| 122 | schedule_activations([]) --> []. | |
| 123 | schedule_activations([ID|T]) --> {simb_activation_id(ID)},!, | |
| 124 | schedule_activation(ID,[],0,root,no_activation), schedule_activations(T). | |
| 125 | schedule_activations([_|T]) --> schedule_activations(T). | |
| 126 | ||
| 127 | ||
| 128 | % --------------------- | |
| 129 | ||
| 130 | % API for incremental step-by-step simulation | |
| 131 | ||
| 132 | simb_initial_state(simb_state(root,InitialTable,Time)) :- | |
| 133 | Time=0, get_initial_scheduling_table(InitialTable). | |
| 134 | ||
| 135 | simb_perform_step(simb_state(FromID,SchedulingTable,Time), TransID, Delta, Probability, | |
| 136 | simb_state(DestID,NewSchedulingTable,NewTime)) :- Options=[], | |
| 137 | simb_one_simulation_step(FromID,SchedulingTable,Time, _, TransID, Delta, Probability, | |
| 138 | DestID,NewSchedulingTable,NewTime, Options). | |
| 139 | ||
| 140 | % skip over none transitions (where only activations are triggered and nothing happens) | |
| 141 | simb_perform_visible_step(State,TransID,Delta,Prob,NewState) :- | |
| 142 | simb_perform_step(State,TID,D1,Prob1,S1), | |
| 143 | (TID=none | |
| 144 | -> simb_perform_visible_step(S1,TransID,D2,Prob2,NewState), | |
| 145 | Delta is D1+D2, multiply_prob(Prob1,Prob2,Prob) | |
| 146 | ; TransID = TID, Delta=D1, NewState=S1, Prob=Prob1). | |
| 147 | ||
| 148 | simb_update_current_state_id(simb_state(FromID,Table,Time),StateID,simb_state(StateID,Table,Time)) :- | |
| 149 | (FromID=StateID -> true | |
| 150 | ; format('Animator has changed state from ~w to ~w!~n',[FromID,StateID]) | |
| 151 | ). | |
| 152 | get_simb_current_state_id(simb_state(FromID,_,_),FromID). | |
| 153 | % TODO: simb_react_to_user_action(...) % inform simulator about user executed events in animator | |
| 154 | ||
| 155 | get_simb_time(simb_state(_,_,Time),Time). | |
| 156 | ||
| 157 | get_simb_scheduling_entry(simb_state(_,Table,_),Time,Prio,ActivationID,Params) :- | |
| 158 | get_scheduling_entry(Table,Time,Prio,ActIDTerm), | |
| 159 | get_activation_id(ActIDTerm,ActivationID), | |
| 160 | get_activation_params(ActIDTerm,Params). | |
| 161 | ||
| 162 | get_scheduling_entry(simb_st(SchedulingTable,_),Time,Prio,ActivationID) :- | |
| 163 | avl_member(Time,SchedulingTable,PrioQueue), | |
| 164 | heap_to_list(PrioQueue,List), | |
| 165 | member(Prio-ActivationID,List). | |
| 166 | ||
| 167 | % useful to probe when the next step will occur: | |
| 168 | get_simb_delay_until_next_step(simb_state(_,simb_st(SchedulingTable,_),Time),Delta) :- !, | |
| 169 | (empty_avl(SchedulingTable) -> Delta = -1 | |
| 170 | ; avl_min(SchedulingTable,NewTime,_) -> Delta is NewTime-Time | |
| 171 | ; add_internal_error('Illegal scheduling table:',SchedulingTable), Delta=0 | |
| 172 | ). | |
| 173 | get_simb_delay_until_next_step(State,Delta) :- | |
| 174 | add_internal_error('Illegal SimB state:',get_simb_delay_until_next_step(State,Delta)), Delta=0. | |
| 175 | ||
| 176 | get_simb_next_activation_term(simb_state(_,SimBST,_),ActivationID,Params) :- !, | |
| 177 | select_next_activation(SimBST,ActivationID,ActIDTerm,_Time,_), | |
| 178 | get_activation_params(ActIDTerm,Params). | |
| 179 | get_simb_next_activation_term(State,_,_) :- | |
| 180 | add_internal_error('Illegal SimB state:',get_simb_next_activation_term(State,_,_)), fail. | |
| 181 | ||
| 182 | ||
| 183 | portray_simb_state(simb_state(StateID,Table,Time)) :- | |
| 184 | format('SimB state for state ~w at time ~w ms:~n',[StateID,Time]), | |
| 185 | portray_scheduling_table(Table). | |
| 186 | ||
| 187 | get_simb_scheduling_table_info(simb_state(_StateID,Table,_Time),Info) :- | |
| 188 | Table = simb_st(T,Single), | |
| 189 | avl_size(T,TimePoints), | |
| 190 | avl_size(Single,SingleActivations), | |
| 191 | ajoin(['Scheduled time points: ',TimePoints,', single activations: ',SingleActivations],Info). | |
| 192 | ||
| 193 | % --------------------- | |
| 194 | ||
| 195 | % scheduling table tools: | |
| 196 | % scheduling_table simb_st(AVL_TimeToPrioQueue, AVL_SingleActivationsToTime) | |
| 197 | empty_scheduling_table(simb_st(E,E)) :- empty_avl(E). | |
| 198 | ||
| 199 | % schedule an activation at time-point Time | |
| 200 | schedule_activation(ID,Params,Time,FromID,FromActIDTerm,SchedulingTable,NewTable) :- | |
| 201 | simb_activation_kind(ID,Kind),!, | |
| 202 | eval_activation_params(Params,ID,FromID,FromActIDTerm,ActivationIDTerm), | |
| 203 | schedule_activation_term(Kind,ID,ActivationIDTerm,Time,FromID,SchedulingTable,NewTable). | |
| 204 | schedule_activation(ID,_Params,_Time,_FromID,_FromActIDTerm,SchedulingTable,NewTable) :- | |
| 205 | add_error(simb,'Cannot schedule unknown activation id:',ID), | |
| 206 | NewTable=SchedulingTable. | |
| 207 | ||
| 208 | schedule_activation_term(multi,ID,ActivationIDTerm,Time,FromID,simb_st(SchedulingTable,SingleTable), | |
| 209 | simb_st(NewTable,SingleTable)) :- | |
| 210 | eval_activation_priority(ID,ActivationIDTerm,FromID,Prio), | |
| 211 | multi_schedule_activation(ActivationIDTerm,Time,Prio,SchedulingTable,NewTable). | |
| 212 | schedule_activation_term(Single,ID,ActIDTerm,Time,FromID,simb_st(SchedulingTable,SingleTable), | |
| 213 | simb_st(NewSchedTable,NewSingleTable)) :- | |
| 214 | avl_fetch(ID,SingleTable,OldTime),!, % TODO: question is whether single applies to ID or ActIDTerm with params? | |
| 215 | (schedule_time_needs_updating(Single,Time,OldTime) | |
| 216 | -> avl_fetch(OldTime,SchedulingTable,OldHeap,SchedTable1), | |
| 217 | eval_activation_priority(ID,ActIDTerm,FromID,Prio), | |
| 218 | delete_from_heap(OldHeap,Prio,ID,NewHeap), | |
| 219 | avl_store(OldTime,SchedTable1,NewHeap,SchedTable2), % remove ID from priority queue of OldTime | |
| 220 | multi_schedule_activation(ActIDTerm,Time,Prio,SchedTable2,NewSchedTable), | |
| 221 | avl_store(ID,SingleTable,Time,NewSingleTable) | |
| 222 | ; % we keep the old time already scheduled for the activation | |
| 223 | NewSchedTable=SchedulingTable, NewSingleTable=SingleTable | |
| 224 | ). | |
| 225 | schedule_activation_term(_Single,ID,ActIDTerm,Time,FromID,simb_st(SchedulingTable,SingleTable), | |
| 226 | simb_st(NewTable,NewSingleTable)) :- | |
| 227 | avl_store(ID,SingleTable,Time,NewSingleTable), % store that we now have a time for this single activation kind | |
| 228 | eval_activation_priority(ID,ActIDTerm,FromID,Prio), | |
| 229 | multi_schedule_activation(ActIDTerm,Time,Prio,SchedulingTable,NewTable). | |
| 230 | ||
| 231 | eval_activation_priority(ID,ActIDTerm,FromID,Prio) :- | |
| 232 | simb_activation_priority(ID,TPrio),!, | |
| 233 | eval_simb_number_expr(FromID,ActIDTerm,priority,TPrio,Prio). | |
| 234 | eval_activation_priority(ID,A,FromID,Prio) :- | |
| 235 | add_internal_error('Unknown activation id:',eval_activation_priority(ID,A,FromID,Prio)), Prio=1. | |
| 236 | ||
| 237 | eval_activation_params([],ID,_FromID,_FromActIDTerm,Res) :- !, Res=ID. | |
| 238 | eval_activation_params(Params,ID,FromID,FromActIDTerm,Res) :- | |
| 239 | eval_simb_params(FromID,FromActIDTerm,Params,ParamValues), | |
| 240 | Res = activation(ID,ParamValues). | |
| 241 | ||
| 242 | % get an activation id from an activation entry in the scheduling table (possible with params) | |
| 243 | get_activation_id(activation(ID,_Params),Res) :- atomic(ID), !, Res=ID. | |
| 244 | get_activation_id(ID,Res) :- atomic(ID),!, Res=ID. | |
| 245 | get_activation_id(ID,ID) :- add_internal_error('Illegal activation term:',ID). | |
| 246 | ||
| 247 | get_activation_params(activation(_,Params),Res) :- !, Res=Params. | |
| 248 | get_activation_params(_,[]). | |
| 249 | ||
| 250 | schedule_time_needs_updating('single:max',NewTime,OldTime) :- NewTime > OldTime. | |
| 251 | schedule_time_needs_updating('single:min',NewTime,OldTime) :- NewTime < OldTime. | |
| 252 | ||
| 253 | % schedule an activation at given time-point in the Time -> ID scheduling table: | |
| 254 | multi_schedule_activation(ActIDTerm,Time,Prio,SchedulingTable,NewTable) :- | |
| 255 | avl_fetch(Time,SchedulingTable,OldAtTime),!, % there are already activations for this time-point | |
| 256 | insert_activation(ActIDTerm,Prio,OldAtTime,NewAtTime), | |
| 257 | avl_store(Time,SchedulingTable,NewAtTime,NewTable). | |
| 258 | multi_schedule_activation(ActIDTerm,Time,Prio,SchedulingTable,NewTable) :- | |
| 259 | init_with_activation(ActIDTerm,Prio,NewAtTime), | |
| 260 | avl_store(Time,SchedulingTable,NewAtTime,NewTable). | |
| 261 | ||
| 262 | ||
| 263 | init_with_activation(ActIDTerm,Prio,NewHeap) :- | |
| 264 | empty_heap(Heap), | |
| 265 | insert_activation(ActIDTerm,Prio,Heap,NewHeap). | |
| 266 | ||
| 267 | % insert activation ID into a heap of activations for a certain time point | |
| 268 | insert_activation(ActIDTerm,Priority,Heap,NewHeap) :- | |
| 269 | add_to_heap(Heap,Priority,ActIDTerm,NewHeap). | |
| 270 | ||
| 271 | % select the top-priority activation among a list of activations for a time point | |
| 272 | select_activation(ID,ActIDTerm,Heap,NewHeap) :- | |
| 273 | get_from_heap(Heap,_Prio,ActIDTerm,NewHeap), | |
| 274 | get_activation_id(ActIDTerm,ID). | |
| 275 | ||
| 276 | select_next_activation(simb_st(SchedulingTable,Single),ActivationID,ActIDTerm,Time, | |
| 277 | simb_st(NewSchedulingTable,NewSingle)) :- | |
| 278 | avl_min(SchedulingTable,Time,ActivationHeap), | |
| 279 | select_activation(ActivationID,ActIDTerm,ActivationHeap,Rest), | |
| 280 | (empty_heap(Rest) | |
| 281 | -> avl_delete(Time,SchedulingTable,_,NewSchedulingTable) | |
| 282 | ; avl_store(Time,SchedulingTable,Rest,NewSchedulingTable) | |
| 283 | ), | |
| 284 | (simb_activation_kind(ActivationID,multi) -> NewSingle=Single | |
| 285 | ; avl_delete(ActivationID,Single,_,NewSingle)). | |
| 286 | ||
| 287 | ||
| 288 | portray_schedule_point(TimePoint-ActivationsHeap) :- | |
| 289 | format(' - ~w ms : ',[TimePoint]), | |
| 290 | portray_heap(ActivationsHeap),nl. | |
| 291 | portray_scheduling_table(simb_st(T,Single)) :- !, | |
| 292 | avl_to_list(T,LT), | |
| 293 | length(LT,Len), | |
| 294 | avl_domain(Single,Dom), | |
| 295 | format('Scheduling table with ~w time point(s) and single activations ~w:~n',[Len,Dom]), | |
| 296 | maplist(portray_schedule_point,LT). | |
| 297 | portray_scheduling_table(T) :- | |
| 298 | format(user_error,'Unknown SimB scheduling table: ~w~n',[T]). | |
| 299 | ||
| 300 | % --------------------- | |
| 301 | ||
| 302 | :- use_module(probsrc(state_space),[transition/4]). | |
| 303 | :- use_module(probsrc(specfile),[get_operation_internal_name/2]). | |
| 304 | :- use_module(probsrc(tcltk_interface),[compute_all_transitions_if_necessary/2]). | |
| 305 | ||
| 306 | run_simb(FromID,SchedulingTable,Time,StepNr,Max,Options) :- | |
| 307 | finish_simulation(FromID,Time,StepNr,Max,Options),!, | |
| 308 | register_finised_simulation(FromID,Time,StepNr,Options), | |
| 309 | (silent_mode(on) -> true | |
| 310 | ; format('SimB Simulation finished at step ~w and time ~w ms in state ~w~n',[StepNr,Time,FromID]), | |
| 311 | portray_scheduling_table(SchedulingTable),nl | |
| 312 | ). | |
| 313 | run_simb(FromID,SchedulingTable,Time,StepNr,Max,Options) :- | |
| 314 | %write(step(StepNr,Time,FromID)),nl,portray_scheduling_table(SchedulingTable),nl, | |
| 315 | simb_one_simulation_step(FromID,SchedulingTable,Time, OpName, _TransID, _Delta, _Probability, | |
| 316 | DestID,NewSchedulingTable,NewTime, Options), | |
| 317 | !, | |
| 318 | N1 is StepNr+1, | |
| 319 | formatsilent('SimB Step ~w from state ~w executed ~w~n',[N1,FromID,OpName]), | |
| 320 | run_simb(DestID,NewSchedulingTable,NewTime,N1,Max,Options). | |
| 321 | run_simb(FromID,SchedulingTable,Time,StepNr,_,Options) :- | |
| 322 | inc_counter(simb_deadlock_reached), | |
| 323 | register_finised_simulation(FromID,Time,StepNr,Options), | |
| 324 | format('SimB Simulation cannot proceed at step ~w and time ~w ms in state ~w~n',[StepNr,Time,FromID]), | |
| 325 | portray_scheduling_table(SchedulingTable),nl. | |
| 326 | ||
| 327 | :- use_module(probltlsrc(ltl_propositions), [is_atomic_ltl_property/1, check_atomic_property_formula/2]). | |
| 328 | finish_simulation(_FromID,_Time,StepNr,Max,_) :- StepNr >= Max, | |
| 329 | inc_counter(simb_max_nr_steps_reached). | |
| 330 | finish_simulation(_FromID,Time,_StepNr,_Max,Options) :- | |
| 331 | member(max_simulation_time(MaxTime),Options), | |
| 332 | Time >= MaxTime, | |
| 333 | inc_counter(simb_max_simulation_time_reached). | |
| 334 | finish_simulation(FromID,_Time,_StepNr,_Max,Options) :- | |
| 335 | member(ltl_stop_condition(AtomicLTL_StopCond),Options), | |
| 336 | check_atomic_property_formula(AtomicLTL_StopCond,FromID), | |
| 337 | inc_counter(simb_ltl_stop_condition_reached). | |
| 338 | ||
| 339 | register_finised_simulation(_FromID,Time,StepNr,_Options) :- | |
| 340 | inc_counter_by(simb_nr_steps,StepNr), | |
| 341 | inc_counter_by(simb_simulation_time,Time). | |
| 342 | ||
| 343 | :- use_module(probsrc(translate),[translate_bexpression_with_limit/3]). | |
| 344 | simb_one_simulation_step(FromID,SchedulingTable,Time, OpName,TransID, Delta, Probability, | |
| 345 | DestID,NewSchedulingTable,NewTime, Options) :- | |
| 346 | select_next_activation(SchedulingTable,ActivationID,ActIDTerm,NewTime,SchedulingTable1), | |
| 347 | debug_format(19,'Activating: ~w~n',[ActIDTerm]), | |
| 348 | (NewTime > Time | |
| 349 | -> Delta is NewTime - Time, | |
| 350 | formatsilent('SimB TIME elapsing ~w ms, new time ~w ms~n',[Delta,NewTime]), | |
| 351 | advance_time(Delta,Options) | |
| 352 | ; Delta=0), | |
| 353 | (simb_activation_effect(ActivationID,OpNames,AddGuard,TransSelection,After,ActivationList) -> true | |
| 354 | ; add_error(simb,'Unknown activation id: ',ActivationID),fail | |
| 355 | ), | |
| 356 | %compile_params(ActIDTerm,AddGuard,AddGuardInlined), | |
| 357 | (execute_operation(OpNames,AddGuard,TransSelection,FromID,ActIDTerm,OpName,TransID,DestID,Probability1) | |
| 358 | -> ActivationList2=ActivationList % TODO: also return probability this TransID was chosen | |
| 359 | ; register_hit(ActivationID,execute_failed), | |
| 360 | simb_activation_options(ActivationID,ActOptions), | |
| 361 | (AddGuard=b(truth,_,_) -> GMsg='', GMsg2='' | |
| 362 | ; GMsg = ' with additional guard ', | |
| 363 | translate_bexpression_with_limit(AddGuard,15,GMsg2) % maybe only show in debug_mode | |
| 364 | ), | |
| 365 | (member(errorWhenNotExecuted,ActOptions) | |
| 366 | -> ajoin(['Could not execute operation(s)',GMsg,GMsg2, | |
| 367 | ' in state ',FromID,' for activation ', ActivationID,':'],Msg), | |
| 368 | add_error(simb,Msg,OpNames) | |
| 369 | ; true), | |
| 370 | (member(activatingOnlyWhenExecuted,ActOptions) | |
| 371 | -> formatsilent('Cannot execute ~w ~wfor activation ~w, discarding activation~n',[OpNames,GMsg,ActivationID]), | |
| 372 | DestID=FromID,ActivationList2 = [], OpName = skip | |
| 373 | ; formatsilent('Cannot execute ~w ~wfor activation ~w, performing activations~n',[OpNames,GMsg,ActivationID]), | |
| 374 | DestID=FromID,ActivationList2 = ActivationList, OpName = skip | |
| 375 | ) | |
| 376 | ), | |
| 377 | !, | |
| 378 | eval_simb_number_expr(FromID,ActIDTerm,after,After,AfterValue), | |
| 379 | SchedulingTime is NewTime+AfterValue, | |
| 380 | In = pst(Probability1,SchedulingTable1), Out = pst(Probability,NewSchedulingTable), | |
| 381 | scheduleNextActivations(ActivationList2,SchedulingTime,FromID,ActIDTerm,In,Out). | |
| 382 | ||
| 383 | :- use_module(library(system),[sleep/1]). | |
| 384 | advance_time(Delta,Options) :- member(simulation_speed/Factor,Options),!, | |
| 385 | D is (Delta*Factor)/1000, % TODO: we could keep track of how many ms the ProB steps required and deduct those | |
| 386 | sleep(D). | |
| 387 | advance_time(_,_). | |
| 388 | ||
| 389 | :- use_module(library(random),[random_member/2]). | |
| 390 | execute_operation([],AddGuard,_,FromID,ActIDTerm,skip,none,DestID,none) :- !, | |
| 391 | check_predicate(FromID,ActIDTerm,AddGuard), | |
| 392 | DestID=FromID, | |
| 393 | inc_counter(simb_skip_steps). | |
| 394 | execute_operation(OpNames,AddGuard,first,FromID,ActIDTerm,OpName,TransID,DestID,Prob) :- !, | |
| 395 | % this corresponds to transitionSelection first | |
| 396 | Prob=none, % there is no randomness here: we always chose the same first transition | |
| 397 | CheckInvariant = false, % TODO: pass as option | |
| 398 | compute_all_transitions_if_necessary(FromID,CheckInvariant), | |
| 399 | member(OpName,OpNames), | |
| 400 | find_transition(FromID,ActIDTerm,OpName,AddGuard,TransID,DestID), | |
| 401 | register_hit(OpName,executed). | |
| 402 | execute_operation(OpNames,AddGuard,uniform,FromID,ActIDTerm,OpName,TransID,DestID,Prob) :- | |
| 403 | compute_all_transitions_if_necessary(FromID,false), | |
| 404 | member(OpName,OpNames), | |
| 405 | findall(cand(OpName,TransID,DestID),find_transition(FromID,ActIDTerm,OpName,AddGuard,TransID,DestID),Candidates), | |
| 406 | random_member(cand(OpName,TransID,DestID),Candidates), | |
| 407 | length(Candidates,Len), Prob is 1/Len, | |
| 408 | register_hit(OpName,executed). | |
| 409 | ||
| 410 | ||
| 411 | :- use_module(probsrc(specfile),[state_corresponds_to_initialised_b_machine/1]). | |
| 412 | :- use_module(probsrc(state_space),[visited_expression/2]). | |
| 413 | :- use_module(probsrc(b_state_model_check),[execute_operation_by_predicate_in_state_with_pos/7]). | |
| 414 | % TODO: merge logic with b_intelligent_trace_replay:perform_single_replay_step_statespace and/or VisB ? | |
| 415 | find_transition(FromID,ActIDTerm,OpName,AddGuard,TransID,DestID) :- | |
| 416 | OpName == skip,!, | |
| 417 | TransID=none, DestID = FromID, | |
| 418 | check_predicate(FromID,ActIDTerm,AddGuard). | |
| 419 | find_transition(FromID,_ActIDTerm,OpName,AddGuard,TransID,DestID) :- is_truth(AddGuard),!, % TO DO: check MAX_OP = 0 | |
| 420 | transition(FromID,OpTerm,TransID,DestID), | |
| 421 | get_operation_internal_name(OpTerm,OpName). | |
| 422 | find_transition(FromID,ActIDTerm,OpName,AddGuard,TransID,DestID) :- | |
| 423 | visited_expression(FromID,BState), Pos=AddGuard, | |
| 424 | state_corresponds_to_initialised_b_machine(BState), | |
| 425 | compile_params_into_pred(ActIDTerm,AddGuard,AddGuardInlined), | |
| 426 | execute_operation_by_predicate_in_state_with_pos(BState,OpName,AddGuardInlined,OpTerm,NewState,Pos,TransInfo), | |
| 427 | tcltk_interface:add_trans_id_infos(FromID,OpTerm,NewState,DestID,TransID,TransInfo). | |
| 428 | ||
| 429 | ||
| 430 | ||
| 431 | :- use_module(probsrc(specfile),[get_state_for_b_formula/3]). | |
| 432 | :- use_module(probsrc(b_interpreter),[b_test_boolean_expression_for_ground_state/5]). | |
| 433 | :- use_module(probsrc(b_global_sets),[add_prob_deferred_set_elements_to_store/3]). | |
| 434 | ||
| 435 | check_predicate(_,_,b(truth,_,_)) :- !. | |
| 436 | check_predicate(StateID,ActIDTerm,Pred) :- | |
| 437 | get_state_for_b_formula(StateID,Pred,State1), | |
| 438 | add_prob_deferred_set_elements_to_store(State1, State2, visible), | |
| 439 | get_local_state(ActIDTerm,ParamValues), | |
| 440 | b_test_boolean_expression_for_ground_state(Pred,ParamValues,State2,'SimB predicate check',0). | |
| 441 | ||
| 442 | :- use_module(library(random),[random/3, random/1]). | |
| 443 | % process a list of triggerActivation/3 terms or atomic activation ids | |
| 444 | scheduleNextActivations(List,SchedulingTime,FromID,FromActIDTerm) --> | |
| 445 | scheduleNextActivations(List,SchedulingTime,FromID,FromActIDTerm,1.0). | |
| 446 | scheduleNextActivations([],_,_,_,_) --> []. | |
| 447 | scheduleNextActivations([H],SchedulingTime,FromID,FromActIDTerm,RemainingProbability) --> | |
| 448 | {number(RemainingProbability), RemainingProbability > 0},!, | |
| 449 | processSingleActivation(H,SchedulingTime,FromID,FromActIDTerm,0,_). % will force a choice; assumes we move all activations with probabilities to the end | |
| 450 | scheduleNextActivations([H|T],SchedulingTime,FromID,FromActIDTerm,RemainingProbability) --> | |
| 451 | processSingleActivation(H,SchedulingTime,FromID,FromActIDTerm,RemainingProbability,NewRemProb), | |
| 452 | scheduleNextActivations(T,SchedulingTime,FromID,FromActIDTerm,NewRemProb). | |
| 453 | ||
| 454 | % we either have an atom for an ActivationID or a list of choices with probabilities | |
| 455 | % amongst the activations with probabilities a single one will be chosen | |
| 456 | processSingleActivation(ID,SchedulingTime,FromID,FromActIDTerm,RemProb,R) --> | |
| 457 | {atomic(ID)},!, % atomic activation id; unconditionally triggered | |
| 458 | {R=RemProb}, schedule_activation_with_prob(ID,[],SchedulingTime,FromID,FromActIDTerm,none). | |
| 459 | processSingleActivation(triggerActivation(ID,Params,Probability),SchedulingTime,FromID,FromActIDTerm,RemProb,NewRemProb) --> !, | |
| 460 | {check_probability(Probability,FromID,FromActIDTerm,RemProb,NewRemProb,Res)}, | |
| 461 | ({Res=trigger(Prob)} -> schedule_activation_with_prob(ID,Params,SchedulingTime,FromID,FromActIDTerm,Prob) ; []). | |
| 462 | processSingleActivation(ID,_,_,_,RemProb,RemProb) --> {add_internal_error('Illegal activation:',ID)},!. | |
| 463 | ||
| 464 | schedule_activation_with_prob(ID,Params,SchedulingTime,FromID,FromActIDTerm,Prob,pst(InProb,InST),pst(OutProb,OutST)) :- | |
| 465 | multiply_prob(InProb,Prob,OutProb), % compute/update the probability that this particular path is chosen | |
| 466 | schedule_activation(ID,Params,SchedulingTime,FromID,FromActIDTerm,InST,OutST). | |
| 467 | ||
| 468 | multiply_prob(none,X,R) :- !, R=X. | |
| 469 | multiply_prob(X,none,R) :- !, R=X. | |
| 470 | multiply_prob(X,Y,R) :- R is X*Y. | |
| 471 | ||
| 472 | % evaluate probability formula and check whether the probability is satisfied (Res=trigger) or not. | |
| 473 | check_probability(none,_FromID,_FromActIDTerm,RemProb,NewRemProb,Res) :- !, | |
| 474 | % probability = none means unconditional trigger | |
| 475 | NewRemProb=RemProb, Res=trigger(none). | |
| 476 | check_probability(_Prob,_FromID,_,inf,NewRemProb,Res) :- !, NewRemProb=inf, Res=no_trigger. | |
| 477 | check_probability(Prob,FromID,FromActIDTerm,RemainingProbability,NewRemProb,Res) :- | |
| 478 | eval_simb_number_expr(FromID,FromActIDTerm,probability,Prob,ProbValue), | |
| 479 | (random(Nr), | |
| 480 | debug_format(19,'Remaining probability: ~w, limit: ~w, random number: ~w~n',[RemainingProbability,ProbValue,Nr]), | |
| 481 | Nr*RemainingProbability =< ProbValue | |
| 482 | -> Res=trigger(ProbValue), NewRemProb = inf % we have executed one event discard rest | |
| 483 | ; Res=no_trigger, NewRemProb is RemainingProbability - ProbValue | |
| 484 | ). | |
| 485 | ||
| 486 | :- use_module(probsrc(b_interpreter),[b_compute_expression_nowf/7]). | |
| 487 | % evaluate an expression which is either a number or a typed formula: | |
| 488 | eval_simb_number_expr(_StateID,_,_,Nr,Res) :- number(Nr),!, Res=Nr. | |
| 489 | eval_simb_number_expr(StateID,FromActIDTerm,Attr,TypedExpr,Res) :- | |
| 490 | get_state_for_b_formula(StateID,TypedExpr,State1), | |
| 491 | add_prob_deferred_set_elements_to_store(State1, State2, visible), | |
| 492 | get_local_state(FromActIDTerm,ParamValues), | |
| 493 | b_compute_expression_nowf(TypedExpr,ParamValues,State2,ResValue,'SimB expression',Attr,TypedExpr),!, | |
| 494 | debug_println(4,eval_simb_number_expr(Attr,ResValue)), | |
| 495 | (extract_number_val(ResValue,NrVal) -> Res=NrVal | |
| 496 | ; ajoin(['Evaluation of SimB expression for ',Attr,' in state ',StateID,' produced a non-number value:'],Msg), | |
| 497 | add_error(sim,Msg,ResValue),fail | |
| 498 | ). | |
| 499 | eval_simb_number_expr(StateID,FromActIDTerm,Attr,TypedExpr,_Res) :- | |
| 500 | get_activation_id(FromActIDTerm,ActID), | |
| 501 | ajoin(['Evaluation of SimB number expression for ',Attr,' for activation ',ActID, | |
| 502 | ' in state ',StateID,' failed:'],Msg), | |
| 503 | add_error(sim,Msg,TypedExpr), fail. | |
| 504 | ||
| 505 | extract_number_val(int(Nr),Nr). | |
| 506 | extract_number_val(term(floating(Nr)),Nr). | |
| 507 | ||
| 508 | ||
| 509 | eval_simb_expr(_StateID,_,_,Nr,Res) :- integer(Nr),!, Res=int(Nr). | |
| 510 | eval_simb_expr(_StateID,_,_,Nr,Res) :- float(Nr),!, Res=term(floating(Nr)). | |
| 511 | eval_simb_expr(StateID,FromActIDTerm,Attr,TypedExpr,ResValue) :- | |
| 512 | get_state_for_b_formula(StateID,TypedExpr,State1), | |
| 513 | add_prob_deferred_set_elements_to_store(State1, State2, visible), | |
| 514 | get_local_state(FromActIDTerm,ParamValues), | |
| 515 | b_compute_expression_nowf(TypedExpr,ParamValues,State2,ResValue,'SimB expression',Attr,TypedExpr),!, | |
| 516 | debug_println(4,eval_simb_expr(Attr,ResValue)). | |
| 517 | eval_simb_expr(StateID,FromActIDTerm,Attr,TypedExpr,_Res) :- | |
| 518 | get_activation_id(FromActIDTerm,ActID), | |
| 519 | ajoin(['Evaluation of SimB expression for ',Attr,' for activation ',ActID, | |
| 520 | ' in state ',StateID,' failed:'],Msg), | |
| 521 | add_error(sim,Msg,TypedExpr), fail. | |
| 522 | ||
| 523 | get_local_state(activation(_,ParamVals),LS) :- nonvar(ParamVals), !, LS=ParamVals. | |
| 524 | get_local_state(ID,R) :- atomic(ID),!, R=[]. | |
| 525 | get_local_state(ID,[]) :- add_internal_error('Illegal activation term:',ID). | |
| 526 | ||
| 527 | ||
| 528 | eval_simb_params(_StateID,_,[],Res) :- !, Res=[]. | |
| 529 | eval_simb_params(StateID,FromActIDTerm,[param(Name,Expr)|T],[bind(Name,HR)|TR]) :- | |
| 530 | eval_simb_expr(StateID,FromActIDTerm,Name,Expr,HR), | |
| 531 | eval_simb_params(StateID,FromActIDTerm,T,TR). | |
| 532 | ||
| 533 | ||
| 534 | :- use_module(probsrc(bsyntaxtree),[is_truth/1,safe_create_texpr/3]). | |
| 535 | :- use_module(probsrc(b_compiler),[b_optimize/6]). | |
| 536 | % compile parameter values into predicate by creating a LET | |
| 537 | % used when we cannot pass the ParamBindings as local store | |
| 538 | compile_params_into_pred(activation(_ID,ParamBindings),Pred,NewPred) :- | |
| 539 | \+ no_need_to_compile(Pred),!, | |
| 540 | split_param_bindings(ParamBindings,TIDs,Exprs), | |
| 541 | safe_create_texpr(let_predicate(TIDs,Exprs,Pred),pred,NewPred), | |
| 542 | (debug_mode(on) -> translate:print_bexpr(NewPred),nl ; true). | |
| 543 | compile_params_into_pred(_,Pred,Pred). % no params available | |
| 544 | ||
| 545 | split_param_bindings([],RI,RV) :- !, RI=[], RV=[]. | |
| 546 | split_param_bindings([bind(ID,VAL)|T],[TID|TI],[TVAL|TV]) :- !, | |
| 547 | TID = b(identifier(ID),any,[]), TVAL = b(value(VAL),any,[]), % TODO: get types from activation_params(ID,_) | |
| 548 | split_param_bindings(T,TI,TV). | |
| 549 | split_param_bindings(L,[],[]) :- add_internal_error('Illegal param bindings:',L). | |
| 550 | ||
| 551 | no_need_to_compile(Pred) :- is_truth(Pred). | |
| 552 | %no_need_to_comple(Nr) :- number(Nr). % not a typed AST; a number from the JSON file |