Package org.mpi_sws.jmc.strategies.trust

Class LocationStore

java.lang.Object
org.mpi_sws.jmc.strategies.trust.LocationStore
public class LocationStore extends Object
A single class to store references to locations and to keep track of location aliases.

Location objects are shared objects used in the program. Whenever a new iteration of the model checker runs, we will replace the Location object associated with the old hashcode with the new one and add an alias that points the new hash code to the old one.

LocationStore is accessed when events are accessed.

The lifetime of a location store is that of the algorithm.

  • Field Details

    • ThreadLocation

      public static Integer ThreadLocation

  • Constructor Details

    • LocationStore

      public LocationStore()
      Constructs a new location store.

  • Method Details

    • addLocation

      public void addLocation(Integer location)
      Add a location to the store.

    • clear

      public void clear()
      Remove all locations from the store.

    • clearAliases

      public void clearAliases()
      Remove all aliases from the store.

    • contains

      public boolean contains(Integer hashCode)
      Returns if a location is contained in the store.

    • containsAlias

      public boolean containsAlias(Integer hashCode)
      Returns if an alias is contained in the store.

    • addAlias

      public void addAlias(Integer oldL, Integer newL)
      Adds an alias between the two location codes.

    • getAlias

      public Integer getAlias(Integer hashCode)
      Returns the location alias for the given hash code.