| 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 |