Class maude

Method Details

• init

  public static boolean init(boolean loadPrelude, int randomSeed, boolean advise, boolean handleInterrupts)

  Init Maude.
  
  This function must be called before anything else.
  
  

  Parameters:

  loadPrelude - Whether the Maude prelude should be loaded.
  

  randomSeed - Seed for the pseudorandom number generator in
  the RANDOM module.
  

  advise - Whether debug messages should be printed.
  

  handleInterrupts - Whether interrupts are handled by Maude.

• init

  public static boolean init(boolean loadPrelude, int randomSeed, boolean advise)

  Init Maude.
  
  This function must be called before anything else.
  
  

  Parameters:

  loadPrelude - Whether the Maude prelude should be loaded.
  

  randomSeed - Seed for the pseudorandom number generator in
  the RANDOM module.
  

  advise - Whether debug messages should be printed.
  

• init

  public static boolean init(boolean loadPrelude, int randomSeed)

  Init Maude.
  
  This function must be called before anything else.
  
  

  Parameters:

  loadPrelude - Whether the Maude prelude should be loaded.
  

  randomSeed - Seed for the pseudorandom number generator in
  the RANDOM module.
  
  

• init

  public static boolean init(boolean loadPrelude)

  Init Maude.
  
  This function must be called before anything else.
  
  

  Parameters:

  loadPrelude - Whether the Maude prelude should be loaded.
  
  
  

• init

  public static boolean init()

  Init Maude.
  
  This function must be called before anything else.
  
  
  
  
  

• load

  public static boolean load(String name)

  Load the file with the given name.
  
  

  Parameters:

  name - The name of the file (absolute or relative to the current
  working directory or MAUDE_LIB).

• input

  public static boolean input(String text)

  Process the given text as direct input to Maude.
  
  

  Parameters:

  text - Maude modules or commands.

• getCurrentModule

  public static Module getCurrentModule()

  Get the current module (the last module inserted or explicitly selected,
  like in the Maude interpreter).

• getModule

  public static Module getModule(String name)

  Get a module or theory by name.
  
  

  Parameters:

  name - Name of the module or theory (module expressions are not allowed).

• downModule

  public static Module downModule(Term term)

  Get a module object from its metarepresentation in this
  module, which must include the META-LEVEL module.
  
  

  Parameters:

  term - The metarepresentation of a module, that is,
  a valid element of the Module sort in META-MODULE.
  The term will be reduced.
  
  

  Returns:

  The module object or null if the given term was not
  a valid module metarepresentation.

• tokenize

  public static TokenVector tokenize(String str)

  Tokenize a string according to Maude lexer rules.
  
  
  
  

  Returns:

  A vector of tokens.

• getModules

  public static ModuleHeaderVector getModules()

  Get the list of loaded modules.
  
  

  Returns:

  A list of module headers (this may change).

• getView

  public static View getView(String name)

  Get a view by name.
  
  

  Parameters:

  name - Name of the view (view expressions are not allowed).

• getViews

  public static ViewVector getViews()

  Get the list of loaded views.

• setAllowProcesses

  public static void setAllowProcesses(boolean flag)

  Allow or disallow running arbitrary executables from Maude code.
  
  

  Parameters:

  flag - Whether process creation should be allowed.

• setAllowFiles

  public static void setAllowFiles(boolean flag)

  Allow or disallow operations on files from Maude code.
  
  

  Parameters:

  flag - Whether file access should be allowed.

• setAllowDir

  public static void setAllowDir(boolean flag)

  Allow or disallow operations on directories from Maude code.
  
  

  Parameters:

  flag - Whether directory access should be allowed.

• setRandomSeed

  public static void setRandomSeed(int randomSeed)

  Set the pseudorandom number generator seed.
  
  

• setAssocUnifDepth

  public static boolean setAssocUnifDepth(float m)

  Set depth multiplier for associative unification.
  
  

• connectEqHook

  public static boolean connectEqHook(String name, Hook hook)

  Connect a callback for the reduction of a special operator declared with
  the SpecialHubSymbol id-hook.
  
  

  Parameters:

  name - The name of the operator to be bound to this callback.
  In case the id-hook contains arguments, the name is instead the first
  of these. A null value may be passed to assign a default callback for
  those operators without an explicitly associated one.
  

  hook - An instance of a subclass of Hook defining its run method.
  The object must be alive as long as the binding is active. A null value
  can be passed to disconnect the current one.
  
  

  Returns:

  Whether this call overwrites a previous binding.

• connectRlHook

  public static boolean connectRlHook(String name, Hook hook)

  Connect a callback for rule rewriting a special operator declared with
  the SpecialHubSymbol id-hook.
  
  

  Parameters:

  name - The name of the operator to be bound to this callback.
  In case the id-hook contains arguments, the name is instead the first
  of these. A null value may be passed to assign a default callback for
  those operators without an explicitly associated one.
  

  hook - An instance of a subclass of Hook defining its run method.
  The object must be alive as long as the binding is active. A null value
  can be passed to disconnect the current one.
  
  

  Returns:

  Whether this call overwrites a previous binding.