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(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 LTL3BA tool for LTL ---> NBA.').
13
14		/* the C interface */
15		foreign_resource(ltl2ba, [cltl2ba]).
16		foreign(cltl2ba,c,cltl2ba(+term,+term,+term,+term,+term,-term)).
17
18		:- dynamic loaded_ltl2ba/0.
19		:- meta_predicate cltl2ba(+,+,+,+,+,+).
20
21		ltl2ba_init :-
22		print('Initialise LTL2BA...'), nl,
23		loadfr.
24
25		loadfr :- (loaded_ltl2ba -> true
26		; (assert(loaded_ltl2ba),
27		load_foreign_resource(library(ltl2ba)))
28		).
29
30		c_call_ltl2ba(LtlFormulaAsAtom,InitStateCallback,FiniteStateCallback,TransitionCallback,Verbose,Result) :-
31		cltl2ba(LtlFormulaAsAtom,InitStateCallback,FiniteStateCallback,TransitionCallback,Verbose,Result).