1		% (c) 2016-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
5		:- module(ltl2ba, [ltl2ba_init/0,c_call_ltl2ba/6]).
6
7		:- use_module(library(lists)).
8		:- use_module('../../src/module_information.pl').
9		:- use_module('../../src/debug.pl').
10
11		:- module_info(group,ltl).
12		:- module_info(description,'This is the interface to the LTL2BA tool for LTL to NBA conversion.').
13
14		% ProB Tcl/Tk has the command "Download and Install LTL2BA Tool" in the Help menu
15		% it will download from:
16		% https://stups.hhu-hosting.de/downloads/ltl2ba_pl/sicstus4.8/
17		% which in turn is built from
18		% https://gitlab.cs.uni-duesseldorf.de/stups/prob/ltl2ba_pl
19
20		/* the C interface */
21		foreign_resource(ltl2ba, [cltl2ba]).
22		foreign(cltl2ba,c,cltl2ba(+term,+term,+term,+term,+term,-term)).
23
24		:- dynamic loaded_ltl2ba/0.
25		:- meta_predicate c_call_ltl2ba(-,1,1,3,-,-).
26
27		ltl2ba_init :-
28		loadfr.
29
30		loadfr :- (loaded_ltl2ba -> true
31		; print('Initialise LTL2BA...'), nl,
32		load_foreign_resource(library(ltl2ba)),
33		assertz(loaded_ltl2ba)
34		).
35
36		c_call_ltl2ba(LtlFormulaAsAtom,InitStateCallback,FiniteStateCallback,TransitionCallback,Verbose,Result) :-
37		cltl2ba(LtlFormulaAsAtom,InitStateCallback,FiniteStateCallback,TransitionCallback,Verbose,Result).