Dynamic Predicates: state_schema/2 init/3 operation/4

360 Lines

42 Predicates

Imported Modules: lists tools bmachine bsyntaxtree probvm_compiler probvm_interpreter probvm_optimize module_information

1 Exports

3 specified Imports

Imports	Exports
Name: translate_bvalue/2 Module: translate Name: state_space_initialise/0 Module: state_space Name: add_error_and_fail/3 Module: error_manager	Name: plugin_info/1

Imports

Exports

Name: translate_bvalue/2

Module: translate

Name: state_space_initialise/0

Module: state_space

Name: add_error_and_fail/3

Module: error_manager

Name: plugin_info/1

balance_substitutions/3

balance_substitutions2/3

balance_substitutions3/3

balance_substitutions_l/3

compile_op/1

compile_ops/1

create_constants_setup/3

create_else/2

create_initialisation/4

create_name_var_tuples/3

create_state_schema/3

create_subst/2

do_initialisation/3

do_transition/4

find_state_property/2

operation_state_schema/2

parameter_names/1

plugin_info/1

plugin_info([
    % The name of the Plugin
    name = 'ProB Virtual Machine'
    % Author is not used yet
    ,author = 'Daniel Plagge'
    % marks the plugin as unstable or stable
    ,status = unstable
    % A list of supported file extensions together with a file description
    %,file_extensions = [ ('Plugin demonstration spec', ['.bvm']) ]
    % 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
    ,plugin_for_modes = [b]
    ,plugin_init=plugin_init/0
    ]).

register_initialisation/0

Determinacy Checker:

! Existence error in argument 1 of absolute_file_name/3
! file probsrc(tools) does not exist
! goal: absolute_file_name(probsrc(tools),_6449,[access(exist),file_type(source),relative_to('/home/hudson/build/workspace/ProB PL-Documentation/prolog/plugins/probvm/probvm.pl')])
! Existence error in argument 1 of absolute_file_name/3
! file probsrc(bmachine) does not exist
! goal: absolute_file_name(probsrc(bmachine),_6849,[access(exist),file_type(source),relative_to('/home/hudson/build/workspace/ProB PL-Documentation/prolog/plugins/probvm/probvm.pl')])
! Existence error in argument 1 of absolute_file_name/3
! file probsrc(bsyntaxtree) does not exist
! goal: absolute_file_name(probsrc(bsyntaxtree),_7249,[access(exist),file_type(source),relative_to('/home/hudson/build/workspace/ProB PL-Documentation/prolog/plugins/probvm/probvm.pl')])
! Existence error in argument 1 of absolute_file_name/3
! file probsrc(translate) does not exist
! goal: absolute_file_name(probsrc(translate),_273,[access(exist),file_type(source),relative_to('/home/hudson/build/workspace/ProB PL-Documentation/prolog/plugins/probvm/probvm.pl')])

Name: register_initialisation/0	Module: probvm
Name: compile_op/1	Module: probvm

Name: RECURSIVE_CALL/4	Module: probvm
Name: balance_iflist2/4	Module: probvm

Name: create_texpr/4	Module: foo_error
Name: create_subst/2	Module: probvm
Name: otherwise
Name: ->/2
Name: =/2
Name: ==/2
Name: ->/3
Name: remove_all/3	Module: foo_error
Name: get_accessed_vars/4	Module: btypechecker
Name: get_texpr_expr/2	Module: foo_error

Name: balance_substitutions2/3	Module: probvm
Name: get_texpr_ids/2	Module: foo_error

Name: balance_substitutions3/3	Module: probvm
Name: remove_bt/4	Module: foo_error

Name: balance_substitutions/3	Module: probvm
Name: balance_substitutions3/3	Module: probvm
Name: balance_substitutions_l/3	Module: probvm

Name: create_else/2	Module: probvm
Name: append/3
Name: otherwise
Name: ->/2
Name: =/2
Name: has_else/1	Module: probvm
Name: ->/3
Name: balance_iflist/4	Module: probvm
Name: get_accessed_vars/4	Module: btypechecker
Name: create_texpr/4	Module: foo_error
Name: balance_substitutions2/3	Module: probvm
Name: balance_substitutions_l/3	Module: probvm

Name: RECURSIVE_CALL/3	Module: probvm
Name: balance_substitutions2/3	Module: probvm

Name: nl
Name: write/1
Name: otherwise
Name: ->/2
Name: assert_op/4	Module: probvm
Name: optimize_instructions/2	Module: foo_error
Name: op_instructions/8	Module: probvm
Name: ->/3
Name: operation_state_schema/2	Module: probvm
Name: memberchk/2

Name: RECURSIVE_CALL/1	Module: probvm
Name: compile_op/1	Module: probvm

Name: RECURSIVE_CALL/3	Module: probvm
Name: get_texpr_id/2	Module: foo_error

Name: make_pseudotyped/2	Module: probvm
Name: create_texpr/4	Module: foo_error

Name: interpret/1	Module: foo_error
Name: init/3	dynamic predicate

Name: interpret/1	Module: foo_error
Name: operation/4	dynamic predicate

Name: ajoin/2	Module: foo_error
Name: translate_bvalue/2	Module: translate
Name: member/2
Name: state_schema/2	dynamic predicate

Name: is_truth/1	Module: foo_error
Name: get_texpr_expr/2	Module: foo_error
Name: last/2	Module: foo_error

Name: pp_init/0	Module: probvm
Name: pp_operations/0	Module: probvm

Name: RECURSIVE_CALL/3	Module: probvm
Name: is/2
Name: true
Name: otherwise
Name: ->/2
Name: =/2
Name: atom_codes/2
Name: append/3
Name: number_codes/2
Name: var/1
Name: ->/3

Name: RECURSIVE_CALL/2	Module: probvm
Name: create_texpr/4	Module: foo_error

Name: compile_substitution/4	Module: foo_error
Name: balance_substitutions/3	Module: probvm
Name: op_skeleton/7	Module: probvm
Name: create_cmp_env/3	Module: foo_error
Name: unmodified_vars/3	Module: probvm

Name: add_enumerated_identifier/6	Module: foo_error
Name: =../2
Name: functor/3
Name: length/2

Name: !
Name: state_schema/2	dynamic predicate
Name: =/2
Name: otherwise
Name: ->/2
Name: b_machine_has_constants	Module: foo_error
Name: ->/3

Name: !
Name: state_names2/2	Module: probvm
Name: create_name_var_tuples/3	Module: probvm
Name: get_texpr_ids/2	Module: foo_error
Name: b_get_machine_operation/4	Module: foo_error
Name: =../2

Name: pretty_print/0	Module: probvm
Name: register_ops/0	Module: probvm
Name: register_initialisation/0	Module: probvm
Name: register_variables/0	Module: probvm
Name: reset/0	Module: probvm
Name: state_space_initialise/0	Module: state_space

Name: fail
Name: pp_spec/1	Module: probvm
Name: pp_state/2	Module: probvm
Name: pp_op/1	Module: probvm
Name: local_names/2	Module: probvm
Name: state_names/2	Module: probvm
Name: write/1
Name: init/3	dynamic predicate

../../prolog/plugins/probvm/probvm.pl

Modules

Predicates of probvm

Module Information