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