1		% (c) 2014-2021 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		:- module(master, [start_master/8
5		% , hash_matches/2 % no longer exported
6		]).
7
8		:- use_module(library(fastrw),[ fast_buf_read/2,fast_buf_write/3 ]).
9		:- use_module(probsrc(module_information)).
10		:- use_module(extension('zmq/zmq'), [init_zmq/0, master_main/10, alloc_term/3]).
11
12		:- module_info(group,zmq).
13		:- module_info(description,'This is the interface to C code for distributed model checking.').
14
15		%get_initialisation(Term) :-
16		% consult('/Users/bendisposto/Puzzle.eventb'),
17		% package(Term),
18		% (Term = load_event_b_project(_A,_B,_C,_D) -> true ; print(err(Term)),nl).
19
20		:- dynamic assertion_count/1.
21
22		get_first_workpackage(assertions(_,_,_),assertions) :-
23		assertion_count(N),
24		print(nr_of_assertions(N)),nl,flush_output,
25		set_assertion_mode(N).
26		get_first_workpackage(_,state(root)).
27
28		:- use_module(probsrc(error_manager)).
29		set_assertion_mode(N) :- add_error(zmq,'Note yet implemented:',set_assertion_mode(N)).
30
31		%hash_matches(State,Hash) :-
32		% init_zmq_master,
33		% fast_buf_write(State,_Len1,_Addr1),
34		% gen_hash(_Addr1,_Len1,Hash).
35
36		:- use_module(probsrc(debug)).
37
38		% TODO: Recovery is not yet implemented
39		start_master(Term,MaxStates,PortStart,Strict,MasterIP,Logfile,TmpDir,HashCycle) :-
40		init_zmq,
41		get_first_workpackage(Term,WP),
42		fast_buf_write(Term,Len1,Addr1),
43		print(size_model(Len1)),nl,flush_output,
44		alloc_term(Addr1, Len1, ModelChunk),
45		fast_buf_write(WP,Len2,Addr2),
46		alloc_term(Addr2, Len2, FWPChunk),
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).