1		% (c) 2014-2024 Lehrstuhl fuer Softwaretechnik und Programmiersprachen,
2		% Heinrich Heine Universitaet Duesseldorf
3		% This software is licenced under EPL 1.0 (http://www.eclipse.org/org/documents/epl-v10.html)
4
5		% 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]).
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/4, 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		format('% Time to get result (~w) of length ~w from breadth-first safety model checking: ~w ms~n',[IntermediateResult,Length,D_CE]).
95		run_mc_safety_property(random,ProductInitStates,Optimizations,Result) :- !,
96		cputime(T1),
97		(run_mc_safety_property_df(ProductInitStates,Optimizations,Result) ->
98		cputime(T2),
99		print('Counter-example has been found'),nl,
100		print(counter_example(Result)),nl
101		;
102		cputime(T2),
103		get_state_space_statistics(TS,Product),
104		print('All nodes visited. No counter-example has been found.'), nl,
105		print('Number of states checked: '), print(Product), print(', where '),
106		print('number of states of the transition system is: '), print(TS), nl,
107		Result = none
108		),
109		print('% Overall Checking Time: '), D is T2-T1, print(D), print(' ms'),nl.
110		run_mc_safety_property(Otherwise,_ProductInitStates,_,_Result) :-
111		add_error_fail(run_mc_safety_property,'Unknown search mode: ', Otherwise).
112
113		/* The algorithm for performing breadth-first search LTL safety model checking */
114		run_mc_safety_property_bf(ProductInitStates,Optimizations,Result) :-
115		maplist(create_and_add_init_state,ProductInitStates),
116		Nr = 0,
117		statistics(walltime,[W1,_]),
118	?	open_search(Nr,W1,Optimizations,Result).
119
120		:- use_module(probsrc(model_checker),[get_model_check_stats/6]).
121		open_search(Nr,RefWallTime,Optimizations,Result) :-
122		get_next_node(CurId,AutState,ActionId),!,
123		% format('Processing B state ~w, BA state:~w, next action:~w~n',[CurId,AutState,ActionId]),
124		(aut_final_state_reached(AutState) -> % bad prefix has been found
125		Result = counter_example_found,
126		print(found_error(counter_example_found,CurId,AutState)),nl
127		; % continue the search
128		Nr1 is Nr +1,
129	?	(print_progress(Nr1,RefWallTime,NewRefTime)
130		-> DeltaW is (NewRefTime-RefWallTime)/1000,
131		get_model_check_stats(SS,TT,_,Perc,_,_),
132		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])
133		; NewRefTime=RefWallTime),
134		compute_state_space_transitions_if_necessary(CurId,Optimizations,ActionsAndIDs),
135		%format(' Transitions for ~w: ~w~n',[CurId,ActionsAndIDs]),
136	?	compute_all_product_transitions(CurId,AutState,ActionId,ActionsAndIDs,Optimizations),
137	?	open_search(Nr1,NewRefTime,Optimizations,Result)
138		).
139		open_search(Nr,_,_Optimizations,Res) :-
140		Res = none,
141		print('All relevant states visited! Product states analysed: '), print(Nr), nl. % these are product states
142
143
144		print_progress(Nr1,_,NewRefTime) :- Nr1 mod 10000 =:= 0, statistics(walltime,[NewRefTime,_]).
145		print_progress(Nr1,RefWallTime,NewRefTime) :- Nr1 mod 100 =:= 0, statistics(walltime,[NewRefTime,_]),
146		NewRefTime-RefWallTime > 10000. % more than 10 secs passed
147
148		compute_state_space_transitions_if_necessary(CurId,Optimizations,ActionsAndIDs) :-
149		compute_state_space_transitions_if_necessary2(CurId,Optimizations),
150		findall((ActId,ActionAsTerm,DestId),
151		transition(CurId,ActionAsTerm,ActId,DestId),
152		ActionsAndIDs).
153
154		compute_state_space_transitions_if_necessary2(CurId,Optimizations) :-
155		(not_all_transitions_added(CurId),
156		%format('Computing transitions for ~w (~w)~n',[CurId,Optimizations]),
157		(retract_open_node(CurId) -> true ; add_warning(safety_mc,'Not open node: ',CurId))
158		-> % if node is still not retracted from queue
159		% TODO: keep track of ltllimit maximum number of new nodes to explore
160		set_context_state(CurId),
161		visited_expression(CurId,CurState),
162		compute_transitions_opt(Optimizations,CurId,CurState),
163		clear_context_state
164		; true % nothing to do
165		).
166
167		% compute new AutomataState
168		% The formal model reaches a new state (DestId), we execute a Büchi Automaton transition
169		% based on the atomic properties of DstId
170		% ActionID is either a variable, or a transition number ensuring that AutState is mapped to CurID (for [X] properties)
171		compute_all_product_transitions(CurId,AutState,ActionId,ActionsAndIDs,Optimizations) :-
172	?	member((ActionId,_Term,DestId),ActionsAndIDs),
173		% format('Processing state transition: (B:~w,BuechiAut:~w) --~w--> B:~w~n',[CurId,AutState,ActionId,DestId]),
174		compute_state_space_transitions_if_necessary2(DestId,Optimizations),
175	?	get_aut_successor(AutState,NextAutState),
176		% backtrack over candidate successor automata states first to perform visited_pair check,
177		% before finding all matching B transitions (NextActionId, if any)
178		(\+ visited_pair(DestId,NextAutState,_,_) % pair not yet processed; TODO: check if this is really correct
179		-> %format('Asserting ~w~n',[visited_pair(DestId,NextAutState,CurId,ActionId)]),
180		assertz(visited_pair(DestId,NextAutState,CurId,ActionId)) % mark as processed
181		; aut_final_state_reached(NextAutState) % TODO: do we need this ??
182		),
183		% format('Attempting to find compatible transitions to BA state ~w~n',[NextAutState]),
184		% now add all next actions to the queue which lead to NextAutState
185	?	check_for_aut_transition(AutState,DestId,NextAutState,NextActionId),
186		% if NextActionId is a variable, then any transition is ok
187		% format(' reaching: ~w * ~w (automata state via forced next action ~w)~n',[DestId,NextAutState,NextActionId]),
188		(aut_final_state_reached(NextAutState) ->
189		add_state_at_end(DestId,NextAutState,NextActionId),
190		assertz(accepting_state(DestId,NextAutState,NextActionId)) % save accepting state (for building later the counter-example)
191		;
192		%\+ visited_pair(DestId,NextAutState,_,_), % THE CHECK used to be here; but that was wrong
193		add_state_at_end(DestId,NextAutState,NextActionId),
194		fail
195		).
196		compute_all_product_transitions(_CurId,_AutState,_ActionId,_ActionsAndIDs,_).
197
198		%%% getting the initial states with respect to the the safety property
199		initial_states_mc_safety_property(StartNodes,Optimizations,ProductInitStatesSet) :-
200		findall(Init,aut_initial_state(Init),InitStates),
201	?	get_product_init_states(StartNodes,InitStates,Optimizations,ProductInitStates),
202		list_to_ord_set(ProductInitStates,ProductInitStatesSet),
203		debug_println(9,init_states(ProductInitStatesSet)).
204
205		get_product_init_states([],_InitStates,_Optimizations,[]).
206		get_product_init_states([StartNode|Nodes],InitStates,Optimizations,Res) :-
207	?	(ltl_safety:tps_occurring % for transition properties we need to have outgoing transitions
208		-> compute_state_space_transitions_if_necessary2(StartNode,Optimizations)
209		; true),
210	?	get_init_product(StartNode,InitStates,IStates),
211		append(IStates,Res1,Res),
212	?	get_product_init_states(Nodes,InitStates,Optimizations,Res1).
213
214		get_init_product(_StartNode,[],[]).
215		get_init_product(StartNode,[Init|Inits],Res) :-
216		findall(Succ,get_ba_successor_state(StartNode,Init,Succ),L),
217		append(L,Res1,Res),
218	?	get_init_product(StartNode,Inits,Res1).
219
220		% after reaching an initial state we execute one transition in the Büchi Automata
221		get_ba_successor_state(StartNode,Init,(StartNode,Next,ActionId)) :-
222	?	aut_transition(Init,Label,Next), % Büchi Automata transition via Label
223	?	check_transition(Label,StartNode,ActionId). % ActionId: id required to satisfy Label (if it has a transition property)
224
225		%---------------------------------------------------------------------
226
227		%%% utility predicates
228		prepare_mc_safety_property :-
229		retractall(product(_,_,_)),
230		retractall(visited_pair(_,_,_,_)),
231		retractall(visited_pair_df(_,_)),
232		retractall(accepting_state(_,_,_)).
233
234		% automata relevant functions
235	?	aut_final_state_reached(AutState) :- aut_final_state(AutState),
236		(AutState = 'accept_all' -> true ; aut_transition(AutState,true,AutState)).
237
238		% Checking whether the automaton expresses the trivial property 'true'.
239		% If so, a counter-example [inital_state] is returned
240		trivial_automaton :-
241		aut_transition(P,L,Q),
242		(P=='accept_init',(L = ap(bpred(Pred))->is_truth(Pred);fail),Q =='accept_init').
243
244		non_empty_automaton :-
245		aut_transition(_P,_L,_Q).
246
247		% state space statistics
248		get_state_space_statistics(TS,Product) :-
249		findall((X,Y),visited_pair_df(X,Y),L),
250		debug_println(9,product_states(L)),
251		length(L,Product),
252		findall(ID,visited_expression_id(ID),IDL),
253		length(IDL,TS).
254		%-------------------------------------------
255
256		%%% Queue operations
257		:- dynamic product/3.
258
259		create_and_add_init_state((CurId,AutState,ActionId)) :-
260		(visited_pair(CurId,AutState,_,_) -> true
261		; assertz(visited_pair(CurId,AutState,root,none))
262		%,format('Asserting init pair (~w,~w) coming from ~w via action ~w~n',[CurId,AutState,root,none])
263		),
264		add_state_at_end(CurId,AutState,ActionId),
265		(aut_final_state_reached(AutState) -> assertz(accepting_state(CurId,AutState,ActionId)); true),
266		debug_println(9,add_node_to_queue(product(CurId,AutState,ActionId))).
267
268		get_next_node(CurId,AutState,ActionId) :-
269		pop_state_from_end(product(CurId,AutState,ActionId)).
270
271		add_state_at_end(State,AutState,ActionId) :-
272		%format('QUEUING: (~w,~w) --~w--> ~n',[State,AutState,ActionId]),
273		assertz(product(State,AutState,ActionId)).
274		%add_state_at_front(State,AutState,ActionId) :-
275		% asserta(product(State,AutState,ActionId)).
276		pop_state_from_end(Node) :-
277	?	retract(product(State,AutState,ActionId)),!,
278		Node = product(State,AutState,ActionId).
279		%-------------------
280
281		/* An algorithm for checking safety LTL properties in depth-first manner.
282		First tryouts showed that the depth-first search is much more effective than the breadth-first mode. */
283
284		run_mc_safety_property_df(InitStates,Optimizations,Result) :-
285		member((CurId,AutState,ActionId),InitStates),
286		(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
287		%% CEPath = [atom(CurId,CurId,none)],
288		Result=model([atom(CurId,[1],none)],no_loop)
289		;
290		mc_safety_property_init((CurId,AutState,ActionId),Optimizations,CEPath,CEPath,Result)
291		).
292
293		% at the init state we already checked for next automaton transitions
294		mc_safety_property_init((CurId,AutState,ActionId),Optimizations,History,HTail,Result) :-
295		(transition(CurId,_Op,ActionId,CurId) -> true ; assertz(visited_pair_df(CurId,AutState))),
296		mc_safety_property_next_state((CurId,AutState,ActionId),Optimizations,History,HTail,Result).
297
298		% model_checker: get_open_node_to_check(DFMODE,NodeID)
299		mc_safety_property((CurId,AutState,ActionId),Optimizations,History,HTail,Result) :-
300		assertz(visited_pair_df(CurId,AutState)),
301		debug_println(19,current_history(CurId,History)),
302		check_for_aut_transition(AutState,CurId,NextAutState,ActionId),
303		mc_safety_property_next_state((CurId,NextAutState,ActionId),Optimizations,History,HTail,Result).
304
305		mc_safety_property_next_state((CurId,AutState,ActionId),_Optimizations,History,[atom(CurId,[1],ActionId1)],Result) :-
306		aut_final_state_reached(AutState),!,
307		( nonvar(ActionId) -> ActionId1=ActionId; ActionId1 = none),
308		print(found_error(counter_example_found,CurId,History)),nl,
309		Result = model(History,no_loop).
310		mc_safety_property_next_state((CurId,AutState,ActionId),Optimizations,History,HTail,Result) :-
311		compute_state_space_transitions_if_necessary(CurId,Optimizations,ActionsAndIDs),
312		random_permutation(ActionsAndIDs,ActionsAndIDs1),
313		HTail = [atom(CurId,[1],ActionId)|HTail2],
314		get_next_state(ActionsAndIDs1,ActionId,DestId),
315		\+ visited_pair_df(DestId,AutState),
316		(ltl_safety:tps_occurring % if there is a transition property, we need outgoing transitions
317		-> compute_state_space_transitions_if_necessary2(DestId,Optimizations)
318		; true),
319		mc_safety_property((DestId,AutState,_NewActionId),Optimizations,History,HTail2,Result).
320
321		% try and get accepting state first
322		get_aut_successor(AutState,accept_all) :- (aut_transition(AutState,_,accept_all) -> true).
323		get_aut_successor(AutState,NextAutState) :- % TODO: randomise and succeed only once if multiple transitions lead
324	?	aut_transition(AutState,true,NextAutState),
325		%(the idea is to execute as soon as possible transitions that do not have the label 'true')
326		NextAutState \= accept_all.
327		get_aut_successor(AutState,NextAutState) :- % TODO: randomise and succeed only once if multiple transitions lead
328	?	aut_transition(AutState,Label,NextAutState), Label \= true, NextAutState \= accept_all.
329
330		check_for_aut_transition(AutState,CurId,NextAutState,ActionId) :-
331		aut_transition(AutState,Label,NextAutState),
332	?	check_transition(Label,CurId,ActionId). % check if label matches transition ActionId from B State CurId
333
334		/*
335		check_for_aut_transition_random(AutState,CurId,NextAutState,ActionId) :-
336		get_randomised_next_aut_states(AutState,Trans),
337		member((Label,NextAutState),Trans),
338		%format('Checking transition ~w from state ~w with label ~w (~w->~w)~n',[ActionId,CurId,Label,AutState,NextAutState]),
339		check_transition(Label,CurId,ActionId).
340
341		get_randomised_next_aut_states(AutState,Res) :-
342		% here we want to test first the non-truth automata transitions in order to terminate earlier in case of a counter-example
343		% this is a type of selective randomising (the idea is to execute as soon as possible transitions that do not have the label 'true')
344		findall((Labl,Next),(aut_transition(AutState,Labl,Next),\+is_truth_label(Labl)),L),
345		random_permutation(L,L1),
346		findall((Labl,Next),(aut_transition(AutState,Labl,Next),is_truth_label(Labl)),LTruth),
347		append(L1,LTruth,Res).
348		% TODO: optimize this; not very efficient
349
350		is_truth_label(true).
351		*/
352
353		get_next_state(ActionsAndIDs,ActionId,DstId) :-
354		member((ActionId,_Term,DstId),ActionsAndIDs).
355
356		%%% for getting the result from LTL Safety Model Check
357		get_bf_search_result(none,Result,Len) :- !, Result = none, Len=0.
358		get_bf_search_result(counter_example_found,Result,Length) :- !,
359		get_counter_example_from_product(Result,Length),
360		debug_println(9,counter_example(Length,Result)).
361		get_bf_search_result(Arg,_Result,_Len) :-
362		add_error_fail(run_mc_safety_property_bf, 'Unknow result: ', Arg).
363
364		get_counter_example_from_product(Result,Length) :-
365	?	accepting_state(State,AutState,ActionId),!,
366		(nonvar(ActionId) -> Trans = ActionId; Trans = none),
367		get_counter_example_list(State,AutState,[atom(State,[1],Trans)],ResList),
368		Result = model(ResList,no_loop),
369		length(ResList,Length).
370		get_counter_example_from_product(Result,0) :-
371		add_error(safety_mc,'No accepting state was found (this is an internal error in the model checker).'),
372		Result=[].
373
374		get_counter_example_list(State,AutState,CurRes,Result) :-
375		visited_pair(State,AutState,root,none),!,
376		Result = CurRes.
377		get_counter_example_list(State,AutState,CurRes,Result) :-
378		visited_pair(State,AutState,PrevState,ActionId),!,
379		%format(' ~w:BA~w ---trans:~w---> previous:~w~n',[State,AutState,ActionId,PrevState]),
380		(transition(PrevState,_ActionAsTerm,ActionId,State), % has only one solution
381	?	aut_transition(PrevAutState,_,AutState),
382		visited_pair(PrevState,PrevAutState,_,_)
383		-> get_counter_example_list(PrevState,PrevAutState,[atom(PrevState,[1],ActionId)|CurRes], Result)
384		; add_error(get_counter_example_list,'Could not find visited predecessor for: ',(State:AutState)),
385		Result=CurRes
386		).
387		get_counter_example_list(State,AutState,CurRes,Result) :-
388		add_error(get_counter_example_list,'No visited_pair found for: ',(State:AutState)),
389		listing(safety_mc:visited_pair/4),
390		Result=CurRes.
391
392
393		%------------------------------------------------------------------------------------------------------------------
394
395
396		:- use_module(ltl_propositions,[check_enabled/2]).
397		:- use_module(probltlsrc(ltl_propositions), [check_transition/4, check_ap/2]).
398		%%% synchronising the automaton transitions with the successor states of the model
399		%%% for transition predicates (like [Event]) the ActionId will be instantiated, and the BA property relies on the Action to be taken next
400		%%% if the ActionId remains a variable, then the property only depends on the state (like, {Pred} )
401		check_transition(true,_StateId,_ActionId) :- !.
402		check_transition(false,_StateId,_ActionId) :- !, fail.
403		check_transition(ap(AP),StateId,_ActionId) :- !,
404	?	check_ap_at_state(AP,StateId).
405		check_transition(tp(TP),StateId,ActionId) :- !,
406		check_enabled(TP,StateId),
407	?	transition(StateId,Op,ActionId,DestId),
408	?	check_transition(TP,Op,StateId,DestId). % ltl_propositions
409		check_transition(not(AF),StateId,ActionId) :- !,
410	?	check_transition_fail(AF,StateId,ActionId).
411		check_transition(and(AF,AG),StateId,ActionId) :- !,
412	?	check_transition(AF,StateId,ActionId),
413	?	check_transition(AG,StateId,ActionId).
414		check_transition(or(AF,AG),StateId,ActionId) :- !,
415		(check_transition(AF,StateId,ActionId) ;
416		check_transition(AG,StateId,ActionId)).
417		check_transition(Label,_StateId,_ActionId) :-
418		add_error_fail(check_transition,'Unknown Buchi automaton transition label: ', Label).
419
420		check_transition_fail(true,_StateId,_ActionId) :- !, fail.
421		check_transition_fail(false,_StateId,_ActionId) :- !.
422		check_transition_fail(ap(AP),StateId,_ActionId) :- !,
423		(check_ap_at_state(AP,StateId)-> fail; true).
424		check_transition_fail(tp(TP),StateId,ActionId) :- !,
425	?	transition(StateId,Op,ActionId,DestId), % we require DestId to be known
426	?	\+ ltl_propositions:check_transition(TP,Op,StateId,DestId).
427		check_transition_fail(not(AF),StateId,ActionId) :- !,
428		check_transition(AF,StateId,ActionId).
429		check_transition_fail(and(AF,AG),StateId,ActionId) :- !,
430		(check_transition_fail(AF,StateId,ActionId) ;
431		check_transition_fail(AG,StateId,ActionId) ).
432		check_transition_fail(or(AF,AG),StateId,ActionId) :- !,
433		check_transition_fail(AF,StateId,ActionId),
434		check_transition_fail(AG,StateId,ActionId).
435		check_transition_fail(Label,_StateId,_ActionId) :-
436		add_error_fail(check_transition,'Unknown Buchi automaton transition label: ', Label).
437
438		check_ap_at_state(deadlock,StateId) :- !,
439		animation_mode(MODE),
440		get_b_optimisation_options(MODE,Optimizations),
441		compute_state_space_transitions_if_necessary2(StateId,Optimizations),
442	?	\+ transition(StateId,_ActionId,_ActionAsTerm,_DestId).
443		check_ap_at_state(AP,StateId) :-
444	?	check_ap(AP,StateId).
445