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