1		% (c) 2016-2022 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(state_space_explorer,[explore_state_space/5, compute_transitions_opt/3,
6		get_b_optimisation_options/2]).
7
8		/* ProB Libraries */
9		:- use_module(probsrc(error_manager)).
10		:- use_module(probsrc(tools),[print_message/1,print_mb/1,statistics_memory_used/1]).
11		:- use_module(probsrc(state_space),[clear_context_state/0,visited_expression/2,state_error/3,
12		set_context_state/1, update_context_state/1]).
13		:- use_module(probsrc(state_space_exploration_modes),[get_open_node_to_check/2,depth_breadth_first_mode/1]).
14		:- use_module(probsrc(specfile),[animation_mode/1]).
15		:- use_module(probsrc(preferences),[get_preference/2]).
16
17		:- use_module(probsrc(model_checker),[compute_transitions_opt/3, perform_static_analyses/3]).
18
19		:- use_module(probsrc(module_information),[module_info/2]).
20		:- module_info(group,ltl).
21		:- module_info(description,'This module provides predicates for state space exploration without performing any checks.').
22
23		explore_state_space(Nr,LimitNr,NodesAnalysed,LimitTime,Res) :-
24		animation_mode(MODE),
25		get_b_optimisation_options(MODE,Optimisations),
26		% 0 for not including the invariant into the respective analyses
27		perform_static_analyses(MODE,0,Optimisations),
28		depth_breadth_first_mode(DFMODE),
29		statistics(walltime,[ReferenceTime,_]),
30		get_model_check_stats(States,_Transitions,_ProcessedTotal,Percentage,_,_),
31		RefStatus=refstatus(ReferenceTime,Percentage,States,ReferenceTime),
32		set_context_state(root),
33		call_cleanup(explore_one_state_stats(Nr,LimitNr,RefStatus,NodesAnalysed,LimitTime,Optimisations,DFMODE,Res),
34		clear_context_state).
35
36		explore_one_state_stats(Nr,LimitNr,RefStatus,NodesAnalysed,LimitTime,Optimisations,DFMODE,Res) :-
37		(Nr < LimitNr ; LimitNr=:= -1),!, % -1 for infinite
38		statistics(walltime,[NewTime,_]),
39		print_stats_and_update_refstatus(Nr,RefStatus,NewTime,RefStatus1),
40		(number(LimitTime), NewTime>LimitTime, Nr>0
41		-> Res = [timeout,Nr],
42		NodesAnalysed=Nr
43		; explore_one_state(Nr,LimitNr,RefStatus1,NodesAnalysed,LimitTime,Optimisations,DFMODE,Res)
44		).
45		explore_one_state_stats(N,_LimitNr,_RefStatus,N,_,_,_,no).
46
47		explore_one_state(Nr,LimitNr,RefStatus,NodesAnalysed,LimitTime,Optimisations,DFMODE,Res) :-
48		get_open_node_to_check(DFMODE,ID),!,
49		visited_expression(ID,CurState),!,
50		update_context_state(ID),
51		compute_transitions_opt(Optimisations,ID,CurState),
52		(state_exploration_found_error(ID,Error)
53		-> model_checker:print_found_error(Error,ID),
54		clear_context_state,
55		NodesAnalysed=Nr
56		; N1 is Nr + 1,
57		explore_one_state_stats(N1,LimitNr,RefStatus,NodesAnalysed,LimitTime,Optimisations,DFMODE,Res)
58		).
59		explore_one_state(N,_LimitNr,_RefStatus,N,_,_,_,all) :-
60		% in case get_open_node_to_check/2 at the previous clause fails we do not have any other states to explore
61		print_message('All open states visited').
62
63		:- use_module(probsrc(model_checker),[get_model_check_stats/6]).
64		:- use_module(probsrc(debug),[formatsilent/2]).
65		print_stats_and_update_refstatus(Nr,RefStatus,NewTime,RefStatus1) :-
66		( (Nr mod 1000 =:= 0, Nr\=0)
67		-> RefStatus = refstatus(RefTime,_RefPerc,PrevStates,StartTime),
68		Delta is NewTime-RefTime,
69		(Delta>20000 % more than 20 seconds since last message
70		-> get_model_check_stats(States,Transitions,ProcessedTotal,Perc,_,_),
71		formatsilent('~n* ~w states explored (~1f% of total ~w), ~w transitions,',[ProcessedTotal,Perc,States,Transitions]),
72		statistics_memory_used(M),
73		print_mb(M),
74		DeltaStates is (States-PrevStates),
75		NodesPerSec is DeltaStates*1000 / (NewTime-RefTime),
76		formatsilent(', current ~2f states/sec~n',[NodesPerSec]),
77		RefStatus1 = refstatus(NewTime,Perc,States,StartTime)
78		; RefStatus1 = RefStatus)
79		; RefStatus1 = RefStatus).
80
81		state_exploration_found_error(ID,Error) :-
82		state_error(ID,_,Err),
83		Error = state_error(Err).
84		state_exploration_found_error(_ID,Error) :-
85		real_error_occurred,
86		Error = general_error_occurred.
87
88		get_b_optimisation_options(MODE,Optimisations) :-
89		(MODE == b),!,
90		Optimisations = opt(PORPrefs,PGEPref),
91		PORPrefs = por(POR,UseEnableGraph,Depth,PGEPref),
92		get_preference(por,POR),
93		get_preference(enable_graph,UseEnableGraph),
94		get_preference(enable_graph_depth,Depth),
95		get_preference(pge,PGEPref).
96		get_b_optimisation_options(_,Optimisations) :-
97		Optimisations = opt(off,off).