1		% (c) 2009 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(testaddon, [plugin_info/1]).
8
9		plugin_info([
10		% The name of the Plugin
11		name = 'Demonstration of a B Plugin'
12		% Author is not used yet
13		%,author = 'Mark Mustermann'
14		% marks the plugin as unstable or stable
15		,status = unstable
16		% A list of supported file extensions together with a file description
17		% (They are not used here because the plugin is used for an already loaded
18		% file, see plugin_for_modes)
19		% ,file_extensions = [ ('Plugin demonstration spec', ['.xtl2', '.PPP']) ]
20		% The predicate that is used to load a file. The first argument is the
21		% filename, the second the file extension (like '.mch').
22		%,load_file = load_spec/1
23		% The transition skeleton initialises a transition variable in such
24		% way that only a part of all transitions match it. It is used to
25		% separate time outs and maximum number of computations for several
26		% transition classes (like different operations).
27		%,transition_skeleton = trans_skel/1
28		% The predicate that computes a transition in the state-space, its
29		% arguments are SourceState,Operation,DestinationState,ListOfOperationInfos.
30		,transition = do_transition/4
31		% The predicate that computes an initial state, its arguments are
32		% Operation,DestinationState,ListOfOperationInfos.
33		,initialisation = do_initialisation/3
34		% A predicate that returns a property for a given state, its arguments
35		% are State,Property.
36		,state_property = find_state_property/2
37		% A predicate that receives a list of expressions,predicates and
38		% predicates on transitions as input (list of codes) and returns
39		% the parsed expressions.
40		% Its arguments are ListOfExpressionStrings,ListOfPredicateStrings,
41		% ListOfTransitionPredicateStrings,ListOfExpressions,ListOfPredicates,
42		% ListOfTransitionPredicates.
43		%,parser = parse_spec/6
44		% A predicate that computes a value of an expression (returned by
45		% the parser above) in a state. Its arguments are Expression,State
46		%,compute_expression = compute/2
47		% A predicate that evaluates a predicate (returned by the parser above)
48		% in a state. Its arguments are Predicate,State
49		%,evaluate_predicate = eval/2
50		% A predicate that evaluates a predicate (returned by the parser above)
51		% for a transition. Its arguments are Predicate,Transition
52		%,evaluate_transition = evaltrans/2
53		% A predicate that checks if a state is initialised. Its argument is a State
54		%,is_initialised_state = is_init/1
55		% Pretty-print a transition, the first argument is the transition, the
56		% second -the result- is a list of codes.
57		%,prettyprint_transition = pp_trans/2
58		% Pretty-print a property, the first argument is the property, the
59		% second -the result- is a list of codes.
60		%,prettyprint_property = pp_prop/2
61		% Syntax colouring is defined by specifying a list of rules, each
62		% containing of a regular expression and a colour class
63		%,syntax_colouring = [pair('/\\*', '\\*/',syntax_comment),
64		% expression('(?=\\m)(start|trans|prop)(?=\\M)', syntax_keyword),
65		% expression('(?=\\m)(true|fail|atomic|nonvar|var|functor|op|is|ground|member|append|length)(?=\\M)|=', syntax_type),
66		% expression(':-|!|-->|;|\\.', syntax_assignment),
67		% expression('%(.*)', syntax_comment)]
68		,plugin_for_modes = [b,z]
69		,plugin_init=plugin_init/0
70		,new_transition_notification=newtrans/4
71		]).
72
73		:- use_module(probsrc(bmachine)).
74		:- use_module(probsrc(translate)).
75		:- use_module(probsrc(state_space),[state_space_initialise/0]).
76
77		:- use_module(probsrc(module_information)).
78		:- module_info(group,plugin).
79		:- module_info(description,'This is an example plugin for the experimental plugin structure.').
80		:- module_info(revision,'$Rev$').
81		:- module_info(lastchanged,'$LastChangedDate$').
82
83		:- public plugin_init/0.
84		plugin_init :-
85		state_space_initialise.
86
87		:- public do_initialisation/3.
88		do_initialisation(Operation,operation(Operation),[]) :-
89		b_top_level_operation(Operation).
90		:- public do_transition/4.
91		do_transition(_State,_Operation,_NewState,[]) :-
92		fail.
93
94		:- public find_state_property/2.
95		find_state_property(operation(Operation),Property) :-
96		b_get_machine_operation(Operation,_,Params,_),
97		member(P,Params),
98		translate_bexpression(P,Property).
99
100		:- public newtrans/4.
101		newtrans(FromId,TransId,DstId,Exists) :-
102		write('**testaddon** new transition from '),
103		write(FromId), write(' to '),
104		( Exists==exists -> write('existing '); write('new ')),
105		write(DstId), write(': '),
106		write(TransId),nl.
107
108