Package edu.udel.cis.vsl.civl.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 Detail

      • 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​(java.util.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

        java.util.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​(java.io.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​(java.util.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