Api (tmpl_dcr.Core.Api)

Api

This module provides the API for the TDCR interpreter. It includes functions to initialize, execute, and view the program, as well as functions to parse and unparse the program in different formats.

val initialize : 
  Ast.Syntax.program ->
  (Ast.Syntax.program
   * (Ast.Syntax.type_expr' Common.Env.env
      * Typing.Helper.event_type_value Stdlib.Hashtbl.Make(Stdlib.String).t
      * Ast.Syntax.expr' Ast.Syntax.annotated Common.Env.env
      * Ast.Syntax.event' Ast.Syntax.annotated Common.Env.env),
    Ast.Error.detailed_error list)
    Stdlib.result

initialize program initializes the program by ensuring that:

All event expressions are well-typed according to the event_env.
Template instance expressions are well-typed according to the event_env, expr_env and template definitions.
All relations find their corresponding events in the event_env.

parameter program
The program to initialize.

returns
A result containing the initialized program if the program is well-typed, or a list of errors if the program is not well-typed.

val execute : 
  event_id:string ->
  ?expr:Ast.Syntax.expr' ->
  ?ty_env:Ast.Syntax.type_expr' Common.Env.env ->
  ?label_types:
    Typing.Helper.event_type_value Stdlib.Hashtbl.Make(Stdlib.String).t ->
  ?expr_env:Ast.Syntax.expr Common.Env.env ->
  ?event_env:Ast.Syntax.event Common.Env.env ->
  Ast.Syntax.program ->
  (Ast.Syntax.program
   * Ast.Syntax.event' Ast.Syntax.annotated Common.Env.env
   * Ast.Syntax.expr' Ast.Syntax.annotated Common.Env.env
   * Ast.Syntax.type_expr' Common.Env.env
   * Typing.Helper.event_type_value Stdlib.Hashtbl.Make(Stdlib.String).t,
    Ast.Error.detailed_error list)
    Stdlib.result

execute ~event_id ?expr ?ty_env ?label_types ?expr_env ?event_env program executes the event with the given event_id and propagate its effects in the program. This function may return a error if the program does not meet the following conditions:

The event is not found in the event_env.
The event is not enabled.
The expression is not well-typed.
The value of the marking is not the same as the received type.

parameter event_id
The id of the event to execute.

parameter expr
The expression to execute the event with.

parameter ty_env
The environment of types to typecheck against.

parameter label_types
The environment of event's label types to typecheck against.

parameter expr_env
The environment of expressions to typecheck against.

parameter event_env
The environment of events to typecheck against.

parameter program
The program to execute.

returns
A result containing the executed program, event environment, expression environment, type environment and event type environment if the program is well-typed, or a list of errors.

val parse_program_from_file : 
  string ->
  (Ast.Syntax.program, Ast.Error.detailed_error list) Stdlib.result

parse_program_from_file filename parses the program from the given filename. This function may return a error if the file does not exist.

parameter filename
The name of the file to parse the program from.

returns
A result containing the parsed program, or a list of errors.

val parse_expression_from_string : 
  string list ->
  (Ast.Syntax.expr' Ast.Syntax.annotated, Ast.Error.detailed_error list)
    Stdlib.result

parse_expression_from_string expr_tokens parses the expression from the given expr_tokens. This function may return a error if the expression is not well-formed.

parameter expr_tokens
The tokens of the expression to parse.

returns
A result containing the parsed expression, or a list of errors.

val unparse_program_tdcr : 
  ?should_print_value:bool ->
  ?should_print_executed_marking:bool ->
  Ast.Syntax.program ->
  (string, 'a) Stdlib.result

unparse_program_tdcr ?should_print_value ?should_print_executed_marking program unparses the program in string format, based on optional flags.

parameter should_print_value
A flag to indicate whether to print the value of the marking.

parameter should_print_executed_marking
A flag to indicate whether to print the executed marking.

parameter program
The program to unparse.

returns
A result containing the unparsed program, or a list of errors.

val unparse_program_json : Ast.Syntax.program -> (string, 'a) Stdlib.result

unparse_program_json program unparses the program in JSON format.

parameter program
The program to unparse.

returns
A result containing the unparsed program, or a list of errors.

val unparse_program_dot : Ast.Syntax.program -> (string, 'a) Stdlib.result

unparse_program_dot program unparses the program in DOT format.

parameter program
The program to unparse.

returns
A result containing the unparsed program, or a list of errors.

val view : 
  ?filter:
    (Ast.Syntax.event ->
      (Ast.Syntax.event Common.Env.env * Ast.Syntax.expr Common.Env.env) ->
      Ast.Syntax.event option) ->
  ?should_print_template_decls:bool ->
  ?should_print_events:bool ->
  ?should_print_value:bool ->
  ?should_print_relations:bool ->
  ?expr_env:Ast.Syntax.expr Common.Env.env ->
  ?event_env:Ast.Syntax.event Common.Env.env ->
  Ast.Syntax.program ->
  (string, 'a) Stdlib.result

view ?filter ?should_print_template_decls ?should_print_events ?should_print_value ?should_print_relations ?expr_env ?event_env program views the program in string format, based on optional flags. Is the same as unparse_program_tdcr but with more options.

parameter filter
A function to filter the events to view.

parameter should_print_template_decls
A flag to indicate whether to print the template declarations.

parameter should_print_events
A flag to indicate whether to print the events.

parameter should_print_value
A flag to indicate whether to print the value of the marking.

parameter should_print_relations
A flag to indicate whether to print the relations.

parameter expr_env
The environment of expressions to typecheck against.

parameter event_env
The environment of events to typecheck against.

parameter program
The program to view.

returns
A result containing the viewed program, or a list of errors.

val view_debug : Ast.Syntax.program -> (string, 'a) Stdlib.result

view_debug program views the program in string format, with debug information.

parameter program
The program to view.

returns
A result containing the viewed program, or a list of errors.

val view_enabled : 
  ?should_print_template_decls:bool ->
  ?should_print_value:bool ->
  ?should_print_relations:bool ->
  ?expr_env:Ast.Syntax.expr Common.Env.env ->
  ?event_env:Ast.Syntax.event Common.Env.env ->
  Ast.Syntax.program ->
  (string, 'a) Stdlib.result

view_enabled ?should_print_template_decls ?should_print_value ?should_print_relations ?expr_env ?event_env program views the enabled events in the program in string format, based on optional flags.

parameter should_print_template_decls
A flag to indicate whether to print the template declarations.

parameter should_print_value
A flag to indicate whether to print the value of the marking.

parameter should_print_relations
A flag to indicate whether to print the relations.

parameter expr_env
The environment of expressions to typecheck against.

parameter event_env
The environment of events to typecheck against.

parameter program
The program to view.

returns
A result containing the viewed program, or a list of errors.

val view_disabled : 
  ?should_print_template_decls:bool ->
  ?should_print_value:bool ->
  ?should_print_relations:bool ->
  ?expr_env:Ast.Syntax.expr Common.Env.env ->
  ?event_env:Ast.Syntax.event Common.Env.env ->
  Ast.Syntax.program ->
  (string, 'a) Stdlib.result

view_disabled ?should_print_template_decls ?should_print_value ?should_print_relations ?expr_env ?event_env program views the disabled events in the program in string format, based on optional flags.

parameter should_print_template_decls
A flag to indicate whether to print the template declarations.

parameter should_print_value
A flag to indicate whether to print the value of the marking.

parameter should_print_relations
A flag to indicate whether to print the relations.

parameter expr_env
The environment of expressions to typecheck against.

parameter event_env
The environment of events to typecheck against.

parameter program
The program to view.

returns
A result containing the viewed program, or a list of errors.