1		:- module(master, [start_master/8
2		% , hash_matches/2 % no longer exported
3		]).
4
5		:- use_module(library(fastrw),[ fast_buf_read/2,fast_buf_write/3 ]).
6		:- use_module('../../../src/module_information.pl').
7		:- use_module('../zmq.pl', [init_zmq/0, master_main/10, alloc_term/3]).
8
9		:- module_info(group,experimental).
10		:- module_info(description,'This is the interface to C code for distributed model checking.').
11		:- module_info(revision,'$Rev: 9609 $').
12		:- module_info(lastchanged,'$LastChangedDate: 2011-11-18 10:43:02 +0100 (Fr, 18 Nov 2011) $').
13
14		%get_initialisation(Term) :-
15		% consult('/Users/bendisposto/Puzzle.eventb'),
16		% package(Term),
17		% (Term = load_event_b_project(_A,_B,_C,_D) -> true ; print(err(Term)),nl).
18
19		:- dynamic assertion_count/1.
20
21		get_first_workpackage(assertions(_,_,_),assertions) :-
22		assertion_count(N),
23		print(nr_of_assertions(N)),nl,flush_output,
24		set_assertion_mode(N).
25		get_first_workpackage(_,state(root)).
26
27		:- use_module(probsrc(error_manager)).
28		set_assertion_mode(N) :- add_error(zmq,'Note yet implemented:',set_assertion_mode(N)).
29
30		%hash_matches(State,Hash) :-
31		% init_zmq_master,
32		% fast_buf_write(State,_Len1,_Addr1),
33		% gen_hash(_Addr1,_Len1,Hash).
34
35		:- use_module(probsrc(debug)).
36
37		% TODO: Recovery is not yet implemented
38		start_master(Term,MaxStates,PortStart,Strict,MasterIP,Logfile,TmpDir,HashCycle) :-
39		init_zmq,
40		get_first_workpackage(Term,WP),
41		fast_buf_write(Term,Len1,Addr1),
42		print(size_model(Len1)),nl,flush_output,
43		alloc_term(Addr1, Len1, ModelChunk),
44		fast_buf_write(WP,Len2,Addr2),
45		alloc_term(Addr2, Len2, FWPChunk),
46		(debug_mode(off) -> Level = 20 ; debug_level(Level)),
47		%AssertionMode = 0,
48		master_main(PortStart, MaxStates, Strict, ModelChunk, FWPChunk, MasterIP, Logfile, TmpDir,HashCycle,RetVal), !,
49		print(retval(RetVal)),nl,flush_output,
50		RetVal == 0.
51
52		%find_hash(H,ID,B) :-
53		% state_space:visited_expression(ID,B),
54		% hash_matches(state(B),H).