1		% (c) 2009-2017 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		% This module is a version of the XTL interpreter as plugin
6
7		:- module(xtl, [plugin_info/1]).
8
9		:- use_module(library(codesio)).
10		:- use_module(xtl_program).
11
12		plugin_info([
13		% The name of the Plugin
14		name = 'ProB Plugin Demonstration'
15		% Author is not used yet
16		%,author = 'Mark Mustermann'
17		% marks the plugin as unstable or stable
18		,status = unstable
19		% A list of supported file extensions together with a file description
20		,file_extensions = [ ('Plugin demonstration spec', ['.xtl2', '.PPP']) ]
21		% The predicate that is used to load a file. The first argument is the
22		% filename, the second the file extension (like '.mch').
23		,load_file = load_spec/1
24		% The transition skeleton initialises a transition variable in such
25		% way that only a part of all transitions match it. It is used to
26		% separate time outs and maximum number of computations for several
27		% transition classes (like different operations).
28		%,transition_skeleton = trans_skel/1
29		% The predicate that computes a transition in the state-space, its
30		% arguments are SourceState,Operation,DestinationState,ListOfOperationInfos.
31		,transition = do_transition/4
32		% The predicate that computes an initial state, its arguments are
33		% Operation,DestinationState,ListOfOperationInfos.
34		,initialisation = do_initialisation/3
35		% A predicate that returns a property for a given state, its arguments
36		% are State,Property.
37		,state_property = find_state_property/2
38		% A predicate that receives a list of expressions,predicates and
39		% predicates on transitions as input (list of codes) and returns
40		% the parsed expressions.
41		% Its arguments are ListOfExpressionStrings,ListOfPredicateStrings,
42		% ListOfTransitionPredicateStrings,ListOfExpressions,ListOfPredicates,
43		% ListOfTransitionPredicates.
44		,parser = parse_spec/6
45		% A predicate that computes a value of an expression (returned by
46		% the parser above) in a state. Its arguments are Expression,State
47		%,compute_expression = compute/2
48		% A predicate that evaluates a predicate (returned by the parser above)
49		% in a state. Its arguments are Predicate,State
50		,evaluate_predicate = eval/2
51		% A predicate that evaluates a predicate (returned by the parser above)
52		% for a transition. Its arguments are Predicate,Transition
53		,evaluate_transition = evaltrans/2
54		% A predicate that checks if a state is initialised. Its argument is a State
55		,is_initialised_state = is_init/1
56		% Pretty-print a transition, the first argument is the transition, the
57		% second -the result- is a list of codes.
58		%,prettyprint_transition = pp_trans/2
59		% Pretty-print a property, the first argument is the property, the
60		% second -the result- is a list of codes.
61		%,prettyprint_property = pp_prop/2
62		% Syntax colouring is defined by specifying a list of rules, each
63		% containing of a regular expression and a colour class
64		,syntax_colouring = [pair('/\\*', '\\*/',syntax_comment),
65		expression('(?=\\m)(start|trans|prop)(?=\\M)', syntax_keyword),
66		expression('(?=\\m)(true|fail|atomic|nonvar|var|functor|op|is|ground|member|append|length)(?=\\M)|=', syntax_type),
67		expression(':-|!|-->|;|\\.', syntax_assignment),
68		expression('%(.*)', syntax_comment)]
69		]).
70
71		:- use_module(probsrc(module_information)).
72		:- module_info(group,plugin_xtl).
73		:- module_info(description,'This module provides the experimental XTL (LTS definition with a Prolog-like syntax) support.').
74		:- module_info(revision,'$Rev$').
75		:- module_info(lastchanged,'$LastChangedDate$').
76
77		:- public load_spec/1, do_transition/4, do_initialisation/3, find_state_property/2, parse_spec/6, eval/2, evaltrans/2, is_init/1.
78
79		load_spec(File) :-
80		reset,
81		'$load'(File).
82
83		reset :-
84		predicate_property(xtl_program:H,dynamic),
85		H \== '$load',
86		retractall(xtl_program:H),
87		fail.
88		reset.
89
90		do_initialisation(start_xtl_system,State,[]) :-
91		xtl_program:start(State).
92		do_transition(State,Operation,NewState,[]) :-
93		xtl_program:trans(Operation,State,NewState).
94
95		find_state_property(State,Property) :-
96		xtl_program:prop(State,Property).
97
98		parse_spec(ExprStrings,PredStrings,TransStrings,Exprs,Preds,Trans) :-
99		parse_list(ExprStrings,Exprs),
100		parse_list(PredStrings,Preds),
101		parse_list(TransStrings,Trans).
102		parse_list([],[]).
103		parse_list([I|Irest],[Term|Trest]) :-
104		append(I,".",Codes),
105		read_from_codes(Codes,Term),
106		parse_list(Irest,Trest).
107
108		eval(Pred,State) :-
109		find_state_property(State,Pred).
110
111		evaltrans(Pred,Trans) :-
112		copy_term(Pred,P),P=Trans.
113
114		is_init(State) :- State \== root.