1		% (c) 2014-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		% A model checker for safety properties.
6
7		% At this point the property intended to be checked has been recognized as a safety property.
8		% As a consequence the negation of the property is represented by a finite automaton which
9		% accepts all bad prefixes violating the safety property. The algorithm implemented in this module
10		% traverses on-the-fly the state space and simulates at the same time movement through the automaton
11		% in regard to the evaluation of the atomic propositions. The algorithm halts when either a final
12		% state of the automaton is visited (bad prefix for the property has been found and will be reported as a counter-example)
13		% or when all nodes of the state space has been visited.
14
15		% TODO: we currently ignore ltllimit in the safety model checker
16		% TODO/Warning: the atom/3 terms contain a list of formulas; this seems relevant only for ProB for Rodin
17		% and do_ltl_modelcheck in eclipse_interface; we set the list to [1] on the assumption there is only one safety
18		% formula; but this is probably wrong for more complex safety properties and will break Rodin LTL visualization
19
20		:- module(safety_mc,[start_mc_safety_property/3]).
21
22		:- use_module(probsrc(error_manager), [add_error_fail/3, add_error/3, add_warning/2, add_error_and_fail/2, add_error/2, add_warning/3]).
23		%:- use_module(probsrc(preferences),[set_preference/2, get_preference/2]).
24		:- use_module(probsrc(specfile),[animation_mode/1]).
25		:- use_module(probsrc(debug),[debug_println/2, formatsilent/2, debug_format/3]).
26		:- use_module(probsrc(tools),[cputime/1]).
27		:- use_module(probsrc(bsyntaxtree),[is_truth/1]).
28
29		%%% state space exploration modules
30		:- use_module(probsrc(state_space),[visited_expression_id/1,
31		transition/4, visited_expression/2,
32		not_all_transitions_added/1, retract_open_node/1,
33		set_context_state/1, clear_context_state/0]).
34		%% :- use_module(probsrc(state_space_open_nodes), [retract_open_node_direct/1]).
35
36		%%% ltl modules
37		%:- use_module(probsrc(state_space),[find_initialised_states/1]).
38		:- use_module(probltlsrc(ltl_safety),[aut_transition/3, aut_final_state/1, aut_initial_state/1]).
39		:- use_module(probltlsrc(state_space_explorer),[compute_transitions_opt/3,get_b_optimisation_options/2]).
40
41		%%% library modules
42		:- use_module(library(file_systems)).
43		:- use_module(library(ordsets)).
44		:- use_module(library(random)).
45		:- use_module(library(lists)).
46
47		:- use_module(probsrc(module_information),[module_info/2]).
48		:- module_info(group,ltl).
49		:- module_info(description,'This module provides predicates for automata-based model checking of safety properties.').
50
51		:- dynamic visited_pair/3, visited_pair_origin/6, visited_pair_df/2, accepting_state/3.
52
53		%% profiler modules
54		%% :- use_module('../../extensions/profiler/profiler.pl').
55		%% :- use_module('../../extensions/profiler/profiler_te.pl').
56
57		%% :- enable_profiling(add_state_at_end/3).
58		%% :- enable_profiling(pop_state_from_end/1).
59		%% :- enable_profiling(check_for_aut_transition/4).
60		%% :- enable_profiling(compute_all_product_transitions/4).
61
62		% the automata-based safety model checker
63		start_mc_safety_property(SearchMode,StartNodes,Result) :-
64		prepare_mc_safety_property,
65		animation_mode(MODE),
66		get_b_optimisation_options(MODE,Optimizations),
67		%% perform_static_analyses(MODE,Optimizations),
68	?	initial_states_mc_safety_property(StartNodes,Optimizations,ProductInitStates),
69		(ProductInitStates == [], non_empty_automaton
70		-> %add_warning(run_mc_safety_property,'No initial states of the product transition system have been generated.'),
71		Result = none,
72		print('All relevant states visited (no initial LTL states feasible)! Product states analysed: '), print(0), nl
73		;
74		(\+ aut_final_state_reached(_)
75		-> add_warning(run_mc_safety_property,'No accept_all state has been found. The property is possibly not a safety property.')
76		; true),
77	?	(select((State,AutState,AId),ProductInitStates,Rest), aut_final_state_reached(AutState)
78		-> Initial = [(State,AutState,AId) | Rest]
79		; Initial = ProductInitStates
80		),
81		%format('Running LTL Safety MC in mode ~w : ~w~n',[SearchMode,Initial]),
82	?	run_mc_safety_property(SearchMode,Initial,Optimizations,Result)
83		).
84
85		run_mc_safety_property(breadth_first,ProductInitStates,Optimizations,Result) :- !,
86		cputime(T1),
87	?	run_mc_safety_property_bf(ProductInitStates,Optimizations,IntermediateResult),
88		cputime(T2), D is T2-T1,
89		format('% Overall Checking Time: ~w ms~n',[D]),
90		cputime(T1_CE),
91		get_bf_search_result(IntermediateResult,Result,Length),
92		cputime(T2_CE),
93		D_CE is T2_CE-T1_CE,
94		write(result(Result)),nl,
95		format('% Time to get result (~w) of length ~w from breadth-first safety model checking: ~w ms~n',[IntermediateResult,Length,D_CE]).
96		run_mc_safety_property(random,ProductInitStates,Optimizations,Result) :- !,
97		cputime(T1),
98		(run_mc_safety_property_df(ProductInitStates,Optimizations,Result) ->
99		cputime(T2),
100		print('Counter-example has been found'),nl,
101		print(counter_example(Result)),nl
102		;
103		cputime(T2),
104		get_state_space_statistics(TS,Product),
105		print('All nodes visited. No counter-example has been found.'), nl,
106		print('Number of states checked: '), print(Product), print(', where '),
107		print('number of states of the transition system is: '), print(TS), nl,
108		Result = none
109		),
110		print('% Overall Checking Time: '), D is T2-T1, print(D), print(' ms'),nl.
111		run_mc_safety_property(Otherwise,_ProductInitStates,_,_Result) :-
112		add_error_fail(run_mc_safety_property,'Unknown search mode: ', Otherwise).
113
114		/* The algorithm for performing breadth-first search LTL safety model checking */
115		run_mc_safety_property_bf(ProductInitStates,Optimizations,Result) :-
116		maplist(create_and_add_init_state,ProductInitStates),
117		Nr = 0,
118		statistics(walltime,[W1,_]),
119	?	open_search(Nr,W1,Optimizations,Result).
120
121		:- use_module(probsrc(model_checker),[get_model_check_stats/6]).
122		open_search(Nr,RefWallTime,Optimizations,Result) :-
123		get_next_node(CurId,AutState,ActionId),!,
124		debug_format(5,'~nProcessing B state ~w, BA state:~w, next action:~w~n',[CurId,AutState,ActionId]),
125		(aut_final_state_reached(AutState) -> % bad prefix has been found
126		Result = counter_example_found,
127		format('Found counter example (bad prefix) leading to state [~w: BA ~w]~n',[CurId,AutState])
128		; % continue the search
129		Nr1 is Nr +1,
130	?	(print_progress(Nr1,RefWallTime,NewRefTime)
131		-> DeltaW is (NewRefTime-RefWallTime)/1000,
132		get_model_check_stats(SS,TT,_,Perc,_,_),
133		formatsilent('Safety model checker progress: ~w product states processed (delta = ~1f sec)~nState space statistics: ~w states checked (~1f%), ~w transitions~n',[Nr1,DeltaW,SS,Perc,TT])
134		; NewRefTime=RefWallTime),
135		compute_state_space_transitions_if_necessary(CurId,Optimizations,ActionsAndIDs),
136		% format(' Transitions for ~w: ~w~n',[CurId,ActionsAndIDs]),
137	?	compute_all_product_transitions(CurId,AutState,ActionId,ActionsAndIDs,Optimizations),
138	?	open_search(Nr1,NewRefTime,Optimizations,Result)
139		).
140		open_search(Nr,_,_Optimizations,Res) :-
141		Res = none,
142		format('All relevant states visited!~nProduct states analysed: ~w~n',[Nr]). % these are product states
143
144
145		print_progress(Nr1,_,NewRefTime) :- Nr1 mod 10000 =:= 0, statistics(walltime,[NewRefTime,_]).
146		print_progress(Nr1,RefWallTime,NewRefTime) :- Nr1 mod 100 =:= 0, statistics(walltime,[NewRefTime,_]),
147		NewRefTime-RefWallTime > 10000. % more than 10 secs passed
148
149		compute_state_space_transitions_if_necessary(CurId,Optimizations,ActionsAndIDs) :-
150		compute_state_space_transitions_if_necessary2(CurId,Optimizations),
151		findall((ActId,ActionAsTerm,DestId),
152		transition(CurId,ActionAsTerm,ActId,DestId),
153		ActionsAndIDs).
154
155		compute_state_space_transitions_if_necessary2(CurId,Optimizations) :-
156		(not_all_transitions_added(CurId),
157		%format('Computing transitions for ~w (~w)~n',[CurId,Optimizations]),
158		(retract_open_node(CurId) -> true ; add_warning(safety_mc,'Not open node: ',CurId))
159		-> % if node is still not retracted from queue
160		% TODO: keep track of ltllimit maximum number of new nodes to explore
161		set_context_state(CurId),
162		visited_expression(CurId,CurState),
163		compute_transitions_opt(Optimizations,CurId,CurState),
164		clear_context_state
165		; true % nothing to do
166		).
167
168		% compute new AutomataState
169		% The formal model reaches a new state (DestId), we execute a Büchi Automaton transition
170		% based on the atomic properties of DstId
171		% ActionID is either a variable, or a transition number ensuring that AutState is mapped to CurID (for [X] properties)
172		compute_all_product_transitions(CurId,AutState,ActionId,ActionsAndIDs,Optimizations) :-
173		copy_term(ActionId,OrigActionId),
174	?	member((ActionId,_Term,DestId),ActionsAndIDs),
175		% format(' Processing state transition: (B:~w,BuechiAut:~w) --~w--> B:~w~n',[CurId,AutState,ActionId,DestId]),
176		compute_state_space_transitions_if_necessary2(DestId,Optimizations),
177	?	get_aut_successor(AutState,NextAutState),
178		% backtrack over candidate successor automata states first to perform visited_pair check,
179		% before finding all matching B transitions (NextActionId, if any)
180
181		% format(' Attempting to find compatible transitions to BA state ~w~n',[NextAutState]),
182		% if NextActionId is a variable, then any transition is ok
183		% now add all next actions to the queue which lead to NextAutState
184	?	check_for_aut_transition(AutState,DestId,NextAutState,NextActionId), % NextActionId is variable if no constraint on it
185		% format(' reaching: ~w * ~w (automata state via forced next action ~w)~n',[DestId,NextAutState,NextActionId]),
186
187	?	\+ already_visited(DestId,NextAutState,NextActionId), % pair not yet processed;
188		% format(' Asserting ~w~n',[visited_pair(DestId,NextAutState,NextActionId)]),
189		assertz(visited_pair(DestId,NextAutState,NextActionId)), % mark as processed / to-be-processed in queue
190		(aut_final_state_reached(NextAutState) ->
191		add_state_to_queue(DestId,NextAutState,NextActionId,coming_from(CurId,AutState,OrigActionId))
192		;
193		add_state_at_queue_end(DestId,NextAutState,NextActionId,coming_from(CurId,AutState,OrigActionId)),
194		fail
195		).
196		compute_all_product_transitions(_CurId,_AutState,_ActionId,_ActionsAndIDs,_).
197
198		already_visited(DestId,NextAutState,NextActionId) :-
199	?	visited_pair(DestId,NextAutState,OtherActionId),
200		(var(OtherActionId) -> true % we have already processed this product state without a constraint on the next action
201		; var(NextActionId) -> false % we now process the product state with unrestricted next action id: could be more behaviour
202		; NextActionId = OtherActionId).
203
204		%%% getting the initial states with respect to the the safety property
205		initial_states_mc_safety_property(StartNodes,Optimizations,ProductInitStatesSet) :-
206		findall(Init,aut_initial_state(Init),InitStates),
207	?	get_product_init_states(StartNodes,InitStates,Optimizations,ProductInitStates),
208		list_to_ord_set(ProductInitStates,ProductInitStatesSet),
209		debug_println(9,init_states(ProductInitStatesSet)).
210
211		get_product_init_states([],_InitStates,_Optimizations,[]).
212		get_product_init_states([StartNode|Nodes],InitStates,Optimizations,Res) :-
213	?	(ltl_safety:tps_occurring % for transition properties we need to have outgoing transitions
214		-> compute_state_space_transitions_if_necessary2(StartNode,Optimizations)
215		; true),
216	?	get_init_product(StartNode,InitStates,IStates),
217		append(IStates,Res1,Res),
218	?	get_product_init_states(Nodes,InitStates,Optimizations,Res1).
219
220		get_init_product(_StartNode,[],[]).
221		get_init_product(StartNode,[Init|Inits],Res) :-
222		findall(Succ,get_ba_successor_state(StartNode,Init,Succ),L),
223		append(L,Res1,Res),
224	?	get_init_product(StartNode,Inits,Res1).
225
226		% after reaching an initial state we execute one transition in the Büchi Automata
227		get_ba_successor_state(StartNode,Init,(StartNode,Next,ActionId)) :-
228	?	aut_transition(Init,Label,Next), % Büchi Automata transition via Label
229	?	check_transition(Label,StartNode,ActionId). % ActionId: id required to satisfy Label (if it has a transition property)
230
231		%---------------------------------------------------------------------
232
233		%%% utility predicates
234		prepare_mc_safety_property :-
235		retractall(product(_,_,_)),
236		retractall(visited_pair(_,_,_)),
237		retractall(visited_pair_origin(_,_,_, _,_,_)),
238		retractall(visited_pair_df(_,_)),
239		retractall(accepting_state(_,_,_)).
240
241		% automata relevant functions
242	?	aut_final_state_reached(AutState) :- aut_final_state(AutState),
243		(AutState = 'accept_all' -> true ; aut_transition(AutState,true,AutState)).
244
245		% Checking whether the automaton expresses the trivial property 'true'.
246		% If so, a counter-example [inital_state] is returned
247		trivial_automaton :-
248		aut_transition(P,L,Q),
249		(P=='accept_init',(L = ap(bpred(Pred))->is_truth(Pred);fail),Q =='accept_init').
250
251		non_empty_automaton :-
252		aut_transition(_P,_L,_Q).
253
254		% state space statistics
255		get_state_space_statistics(TS,Product) :-
256		findall((X,Y),visited_pair_df(X,Y),L),
257		debug_println(9,product_states(L)),
258		length(L,Product),
259		findall(ID,visited_expression_id(ID),IDL),
260		length(IDL,TS).
261		%-------------------------------------------
262
263		%%% Queue operations
264		:- dynamic product/3.
265
266		create_and_add_init_state((CurId,AutState,ActionId)) :-
267		debug_format(5,'Creating initial state [~w:BA ~w] -- ~w -->~n',[CurId,AutState,ActionId]),
268		(already_visited(CurId,AutState,ActionId) -> fail ; assertz(visited_pair(CurId,AutState,ActionId)) ),
269		add_state_to_queue(CurId,AutState,ActionId,coming_from(root,root,none)).
270
271		get_next_node(CurId,AutState,ActionId) :-
272		pop_state_from_end(product(CurId,AutState,ActionId)).
273
274		add_state_to_queue(State,AutState,ActionId,From) :-
275		(aut_final_state_reached(AutState) ->
276		add_state_at_queue_front(State,AutState,ActionId,From),
277		debug_format(19,'** Found Accepting state ~w~n',[(State,AutState,ActionId)]),
278		assertz(accepting_state(State,AutState,ActionId)) % save accepting state (for building later the counter-example)
279		; add_state_at_queue_end(State,AutState,ActionId,From)
280		).
281		add_state_at_queue_end(State,AutState,ActionId,coming_from(PrevState,PrevAutState,PrevActionId)) :-
282		% format('QUEUING: (~w,~w) --~w--> ~n',[State,AutState,ActionId]),
283		assertz(product(State,AutState,ActionId)),
284		assertz(visited_pair_origin(State,AutState,ActionId,PrevState,PrevAutState,PrevActionId)).
285		add_state_at_queue_front(State,AutState,ActionId,coming_from(PrevState,PrevAutState,PrevActionId)) :-
286		% format('QUEUING at FRONT: (~w,~w) --~w--> ~n',[State,AutState,ActionId]),
287		asserta(product(State,AutState,ActionId)),
288		assertz(visited_pair_origin(State,AutState,ActionId,PrevState,PrevAutState,PrevActionId)).
289
290		%add_state_at_front(State,AutState,ActionId) :-
291		% asserta(product(State,AutState,ActionId)).
292		pop_state_from_end(Node) :-
293	?	retract(product(State,AutState,ActionId)),!,
294		Node = product(State,AutState,ActionId).
295		%-------------------
296
297		/* An algorithm for checking safety LTL properties in depth-first manner.
298		First tryouts showed that the depth-first search is much more effective than the breadth-first mode. */
299
300		run_mc_safety_property_df(InitStates,Optimizations,Result) :-
301		member((CurId,AutState,ActionId),InitStates),
302		(trivial_automaton -> % the automaton is trivial , i.e. we have checked the formula 'false' and need to return one of the initial states as a counter-example
303		%% CEPath = [atom(CurId,CurId,none)],
304		Result=model([atom(CurId,[1],none)],no_loop)
305		;
306		mc_safety_property_init((CurId,AutState,ActionId),Optimizations,CEPath,CEPath,Result)
307		).
308
309		% at the init state we already checked for next automaton transitions
310		mc_safety_property_init((CurId,AutState,ActionId),Optimizations,History,HTail,Result) :-
311		(transition(CurId,_Op,ActionId,CurId) -> true ; assertz(visited_pair_df(CurId,AutState))),
312		mc_safety_property_next_state((CurId,AutState,ActionId),Optimizations,History,HTail,Result).
313
314		% model_checker: get_open_node_to_check(DFMODE,NodeID)
315		mc_safety_property((CurId,AutState,ActionId),Optimizations,History,HTail,Result) :-
316		assertz(visited_pair_df(CurId,AutState)),
317		debug_println(19,current_history(CurId,History)),
318		check_for_aut_transition(AutState,CurId,NextAutState,ActionId),
319		mc_safety_property_next_state((CurId,NextAutState,ActionId),Optimizations,History,HTail,Result).
320
321		mc_safety_property_next_state((CurId,AutState,ActionId),_Optimizations,History,[atom(CurId,[1],ActionId1)],Result) :-
322		aut_final_state_reached(AutState),!,
323		( nonvar(ActionId) -> ActionId1=ActionId; ActionId1 = none),
324		print(found_error(counter_example_found,CurId,History)),nl,
325		Result = model(History,no_loop).
326		mc_safety_property_next_state((CurId,AutState,ActionId),Optimizations,History,HTail,Result) :-
327		compute_state_space_transitions_if_necessary(CurId,Optimizations,ActionsAndIDs),
328		random_permutation(ActionsAndIDs,ActionsAndIDs1),
329		HTail = [atom(CurId,[1],ActionId)|HTail2],
330		get_next_state(ActionsAndIDs1,ActionId,DestId),
331		\+ visited_pair_df(DestId,AutState),
332		(ltl_safety:tps_occurring % if there is a transition property, we need outgoing transitions
333		-> compute_state_space_transitions_if_necessary2(DestId,Optimizations)
334		; true),
335		mc_safety_property((DestId,AutState,_NewActionId),Optimizations,History,HTail2,Result).
336
337		% try and get accepting state first
338		get_aut_successor(AutState,accept_all) :- (aut_transition(AutState,_,accept_all) -> true).
339		get_aut_successor(AutState,NextAutState) :- % TODO: randomise and succeed only once if multiple transitions lead
340	?	aut_transition(AutState,true,NextAutState),
341		%(the idea is to execute as soon as possible transitions that do not have the label 'true')
342		NextAutState \= accept_all.
343		get_aut_successor(AutState,NextAutState) :- % TODO: randomise and succeed only once if multiple transitions lead
344	?	aut_transition(AutState,Label,NextAutState), Label \= true, NextAutState \= accept_all.
345
346		check_for_aut_transition(AutState,CurId,NextAutState,ActionId) :-
347		aut_transition(AutState,Label,NextAutState),
348	?	check_transition(Label,CurId,ActionId). % check if label matches transition ActionId from B State CurId
349
350		/*
351		check_for_aut_transition_random(AutState,CurId,NextAutState,ActionId) :-
352		get_randomised_next_aut_states(AutState,Trans),
353		member((Label,NextAutState),Trans),
354		%format('Checking transition ~w from state ~w with label ~w (~w->~w)~n',[ActionId,CurId,Label,AutState,NextAutState]),
355		check_transition(Label,CurId,ActionId).
356
357		get_randomised_next_aut_states(AutState,Res) :-
358		% here we want to test first the non-truth automata transitions in order to terminate earlier in case of a counter-example
359		% this is a type of selective randomising (the idea is to execute as soon as possible transitions that do not have the label 'true')
360		findall((Labl,Next),(aut_transition(AutState,Labl,Next),\+is_truth_label(Labl)),L),
361		random_permutation(L,L1),
362		findall((Labl,Next),(aut_transition(AutState,Labl,Next),is_truth_label(Labl)),LTruth),
363		append(L1,LTruth,Res).
364		% TODO: optimize this; not very efficient
365
366		is_truth_label(true).
367		*/
368
369		get_next_state(ActionsAndIDs,ActionId,DstId) :-
370		member((ActionId,_Term,DstId),ActionsAndIDs).
371
372		%%% for getting the result from LTL Safety Model Check
373		get_bf_search_result(none,Result,Len) :- !, Result = none, Len=0.
374		get_bf_search_result(counter_example_found,Result,Length) :- !,
375		get_counter_example_from_product(Result,Length),
376		debug_println(9,counter_example(Length,Result)).
377		get_bf_search_result(Arg,_Result,_Len) :-
378		add_error_fail(run_mc_safety_property_bf, 'Unknow result: ', Arg).
379
380		get_counter_example_from_product(Result,Length) :-
381		accepting_state(State,AutState,ActionId),!,
382		(nonvar(ActionId) -> Trans = ActionId; Trans = none),
383		debug_format(19,'Start constructing counter-example backwards from ~w:~w~n',[State,AutState]),
384		%listing(accepting_state/3),nl, listing(visited_pair/3),nl, listing(visited_pair_origin/6),nl,
385		get_counter_example_list(State,AutState,ActionId,[atom(State,[1],Trans)],ResList),
386		Result = model(ResList,no_loop),
387		length(ResList,Length).
388		get_counter_example_from_product(Result,0) :-
389		add_error(safety_mc,'No accepting state was found (this is an internal error in the model checker).'),
390		Result=[].
391
392		get_counter_example_list(State,AutState,ActionId,CurRes,Result) :-
393		visited_pair_origin(State,AutState,StoredActionId,root,root,none),
394		(ActionId==StoredActionId -> true ; var(StoredActionId), var(ActionId)),
395		!, % we found our way back to an initial state
396		Result = CurRes.
397		get_counter_example_list(State,AutState,ActionId,CurRes,Result) :-
398		(%visited_pair(State,AutState,PrevState,PrevAutState,StoredActionId), % Note there could be several entries
399	?	visited_pair_origin(State,AutState,StoredActionId,PrevState,PrevAutState,PrevActionId),
400		(ActionId==StoredActionId -> true ; var(StoredActionId), var(ActionId)),
401		debug_format(5,' [~w:BA ~w] ---counter_ex_trans:~w---> previous:[~w:BA ~w ~w]~n',[State,AutState,ActionId,PrevState,PrevAutState,PrevActionId]),
402		copy_term(PrevActionId,GroundPrevActionId),
403		transition(PrevState,_ActionAsTerm,GroundPrevActionId,State), % has only one solution if ActionId ground
404		aut_transition(PrevAutState,_,AutState)
405		-> get_counter_example_list(PrevState,PrevAutState,PrevActionId,
406		[atom(PrevState,[1],GroundPrevActionId)|CurRes], Result)
407		; add_error(get_counter_example_list,'Could not find visited predecessor for: ',(State:AutState)),
408		Result=CurRes
409		).
410		%get_counter_example_list(State,AutState,CurRes,Result) :-
411		% add_error(get_counter_example_list,'No visited_pair found for: ',(State:AutState)),
412		% listing(safety_mc:visited_pair/4),
413		% Result=CurRes.
414
415
416		%------------------------------------------------------------------------------------------------------------------
417
418
419		%:- use_module(ltl_propositions,[check_enabled/2]).
420		:- use_module(probltlsrc(ltl_propositions), [check_transition_pred/5, check_ap/2]).
421		%%% synchronising the automaton transitions with the successor states of the model
422		%%% for transition predicates (like [Event]) the ActionId will be instantiated, and the BA property relies on the Action to be taken next
423		%%% if the ActionId remains a variable, then the property only depends on the state (like, {Pred} )
424		check_transition(true,_StateId,_ActionId) :- !.
425		check_transition(false,_StateId,_ActionId) :- !, fail.
426		check_transition(ap(AP),StateId,_ActionId) :- !,
427	?	check_ap_at_state(AP,StateId).
428		check_transition(tp(TP),StateId,ActionId) :- !,
429		%check_enabled(TP,StateId), % not sure why this is required: it checks there is one solution; the code below will do that as well
430	?	transition(StateId,Op,ActionId,DestId),
431	?	check_transition_pred(TP,Op,StateId,ActionId,DestId). % ltl_propositions
432		check_transition(not(AF),StateId,ActionId) :- !,
433	?	check_transition_fail(AF,StateId,ActionId).
434		check_transition(and(AF,AG),StateId,ActionId) :- !,
435	?	check_transition(AF,StateId,ActionId),
436	?	check_transition(AG,StateId,ActionId).
437		check_transition(or(AF,AG),StateId,ActionId) :- !,
438		(check_transition(AF,StateId,ActionId) ;
439		check_transition(AG,StateId,ActionId)).
440		check_transition(Label,_StateId,_ActionId) :-
441		add_error_fail(check_transition,'Unknown Buchi automaton transition label: ', Label).
442
443		check_transition_fail(true,_StateId,_ActionId) :- !, fail.
444		check_transition_fail(false,_StateId,_ActionId) :- !.
445		check_transition_fail(ap(AP),StateId,_ActionId) :- !,
446		(check_ap_at_state(AP,StateId)-> fail; true).
447		check_transition_fail(tp(TP),StateId,ActionId) :- !,
448	?	transition(StateId,Op,ActionId,DestId), % we require DestId to be known
449	?	\+ ltl_propositions:check_transition_pred(TP,Op,StateId,ActionId,DestId).
450		check_transition_fail(not(AF),StateId,ActionId) :- !,
451		check_transition(AF,StateId,ActionId).
452		check_transition_fail(and(AF,AG),StateId,ActionId) :- !,
453		(check_transition_fail(AF,StateId,ActionId) ;
454		check_transition_fail(AG,StateId,ActionId) ).
455		check_transition_fail(or(AF,AG),StateId,ActionId) :- !,
456		check_transition_fail(AF,StateId,ActionId),
457		check_transition_fail(AG,StateId,ActionId).
458		check_transition_fail(Label,_StateId,_ActionId) :-
459		add_error_fail(check_transition,'Unknown Buchi automaton transition label: ', Label).
460
461		check_ap_at_state(deadlock,StateId) :- !,
462		animation_mode(MODE),
463		get_b_optimisation_options(MODE,Optimizations),
464		compute_state_space_transitions_if_necessary2(StateId,Optimizations),
465	?	\+ transition(StateId,_ActionId,_ActionAsTerm,_DestId).
466		check_ap_at_state(AP,StateId) :-
467	?	check_ap(AP,StateId).
468