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). |