Module dev.civl.mc
Package dev.civl.mc.model.IF

Interface Fragment

public interface Fragment
A fragment is a sequence of statements. It has a "pointer" to the start location and a set of statements as its final statements which should all emanate from the same location.

  • Method Details

    • addGuardToStartLocation

      void addGuardToStartLocation(Expression guard, ModelFactory factory)
      Add a specified guard to the all statements of the start location. If a statement has an existing guard, then it will have a new guard which is a conjunction of the both. This method is used for translating a when statement, where it adds the guard of the when statement to the start location of its body fragment.
      Parameters:
      guard - The guard that is to be combined with
      factory - The model factory that provides some helper methods that are useful in checking if an expression is True.

    • addFinalStatement

      void addFinalStatement(Statement statement)
      Add a statement to the final statement set
      Parameters:
      statement - the new statement to be added to the final statement set

    • addFinalStatementSet

      void addFinalStatementSet(Set<Statement> stmtSet)
      Add a set of statements to the final statement set
      Parameters:
      stmtSet - the set of new statements to be added to the final statement set

    • addNewStatement

      void addNewStatement(Statement statement)
      Add a new statement to the fragment, which will be considered the subsequent statement of the current final statements.s
      Parameters:
      statement - the new statement to be added to the fragment

    • combineWith

      Fragment combineWith(Fragment next)
      Combine two fragment in sequential order.
      Precondition: this.lastStatement == null
      Parameters:
      next - the fragment that comes after the current fragment
      Returns:
      the sequential combination of both fragments

    • isEmpty

      boolean isEmpty()
      Check if the fragment is empty
      Returns:
      true iff both the start location and the last statement are null

    • finalStatements

      Set<Statement> finalStatements()
      Returns:
      The set of final statements of this fragment

    • uniqueFinalStatement

      Statement uniqueFinalStatement()
      Precondition: finalStatements().size() == 1
      Returns:
      The unique final statement of this fragment

    • parallelCombineWith

      Fragment parallelCombineWith(Fragment parallel)
      Combine this fragment and another fragment in parallel, i.e., merge the start location, and add the last statement of both fragments as the last statement of the result fragment
      Parameters:
      parallel - the second fragment to be combined with
      Preconditions:
      this.startLocation.id() === parallel.startLocation.id()
      Returns:
      the new fragment after the combination

    • print

      void print(PrintStream out)
      Print the fragment
      Parameters:
      out - the print stream

    • setStartLocation

      void setStartLocation(Location location)
      Update the start location of this fragment
      Parameters:
      location - The new start location

    • setFinalStatements

      void setFinalStatements(Set<Statement> statements)
      Update the last statement of this fragment
      Parameters:
      statements - The new last statements

    • startLocation

      Location startLocation()
      Returns:
      The start location of this fragment

    • updateStartLocation

      void updateStartLocation(Location newLocation)
      Update the start location with a new location
      Parameters:
      newLocation - the new start location