plugin_info([
% The name of the Plugin
name = 'Demonstration of a B Plugin'
% Author is not used yet
%,author = 'Mark Mustermann'
% marks the plugin as unstable or stable
,status = unstable
% A list of supported file extensions together with a file description
% (They are not used here because the plugin is used for an already loaded
% file, see plugin_for_modes)
% ,file_extensions = [ ('Plugin demonstration spec', ['.xtl2', '.PPP']) ]
% The predicate that is used to load a file. The first argument is the
% filename, the second the file extension (like '.mch').
%,load_file = load_spec/1
% The transition skeleton initialises a transition variable in such
% way that only a part of all transitions match it. It is used to
% separate time outs and maximum number of computations for several
% transition classes (like different operations).
%,transition_skeleton = trans_skel/1
% The predicate that computes a transition in the state-space, its
% arguments are SourceState,Operation,DestinationState,ListOfOperationInfos.
,transition = do_transition/4
% The predicate that computes an initial state, its arguments are
% Operation,DestinationState,ListOfOperationInfos.
,initialisation = do_initialisation/3
% A predicate that returns a property for a given state, its arguments
% are State,Property.
,state_property = find_state_property/2
% A predicate that receives a list of expressions,predicates and
% predicates on transitions as input (list of codes) and returns
% the parsed expressions.
% Its arguments are ListOfExpressionStrings,ListOfPredicateStrings,
% ListOfTransitionPredicateStrings,ListOfExpressions,ListOfPredicates,
% ListOfTransitionPredicates.
%,parser = parse_spec/6
% A predicate that computes a value of an expression (returned by
% the parser above) in a state. Its arguments are Expression,State
%,compute_expression = compute/2
% A predicate that evaluates a predicate (returned by the parser above)
% in a state. Its arguments are Predicate,State
%,evaluate_predicate = eval/2
% A predicate that evaluates a predicate (returned by the parser above)
% for a transition. Its arguments are Predicate,Transition
%,evaluate_transition = evaltrans/2
% A predicate that checks if a state is initialised. Its argument is a State
%,is_initialised_state = is_init/1
% Pretty-print a transition, the first argument is the transition, the
% second -the result- is a list of codes.
%,prettyprint_transition = pp_trans/2
% Pretty-print a property, the first argument is the property, the
% second -the result- is a list of codes.
%,prettyprint_property = pp_prop/2
% Syntax colouring is defined by specifying a list of rules, each
% containing of a regular expression and a colour class
%,syntax_colouring = [pair('/\\*', '\\*/',syntax_comment),
% expression('(?=\\m)(start|trans|prop)(?=\\M)', syntax_keyword),
% expression('(?=\\m)(true|fail|atomic|nonvar|var|functor|op|is|ground|member|append|length)(?=\\M)|=', syntax_type),
% expression(':-|!|-->|;|\\.', syntax_assignment),
% expression('%(.*)', syntax_comment)]
,plugin_for_modes = [b,z]
,plugin_init=plugin_init/0
,new_transition_notification=newtrans/4
]).