Package it.univr.di.cstnu.algorithms

Class OSTNU

java.lang.Object
it.univr.di.cstnu.algorithms.AbstractCSTN<OSTNUEdgePluggable>
it.univr.di.cstnu.algorithms.OSTNU
public class OSTNU extends AbstractCSTN<OSTNUEdgePluggable>
Represents a Simple Temporal Network with Uncertainty and Oracles (OSTNU).

This class implementation considers instantaneous reactions and checks the agile controllability, assuming that the network can be executed by adopting an early execution strategy.

At 2024-02-14, the agile controllability is checked, propagating a modified version of Morris' rules:

  1. No case rule
  2. new upper case rule
  3. new lower case rule
  4. cross-case rule
  5. label removal rule
  6. oracle rule

Each oracle is associated with a specific contingent node. So, if there is a contingent node 'C' and an oracle 'OC' for it, node OC has in its observation field the value 'c' ('c' is just a label).
New upper/lower case rules and oracle rule determine new rules labeled by the fact that the oracle is involved or not.
In particular, each value determined by the oracle rule involving an oracle 'OC' having observation field = 'c' is labeled by 'c'. Each value is determined by a lower / upper rule (without exploiting the associated oracle) that involves the contingent node 'C', which is labeled by '¬c'.
In other words, label 'c' and label '¬c' represent two possible values generated considering the contingent node 'C' that cannot be combined because they are alternatives. 'c' and '¬c' can be considered literals of a boolean proposition 'c'.
Other rules consider and propagate only values having a label that are consistent, i.e., labels that have no opposite literals.


Constraint values (represented as edge values) are integers.
Version:
$Rev: 840 $
Author:
Roberto Posenato

  • Field Details

    • VERSIONandDATE

      public static final String VERSIONandDATE
      Version of the class
      See Also:

    • activationNode

      it.unimi.dsi.fastutil.objects.Object2ObjectMap<LabeledNode,LabeledNode> activationNode
      Utility map that returns the activation time point (node) associated with a contingent link, given the contingent timepoint, i.e., contingent link A ===> C determines the entry (C, A) in this map.

    • checkStatus

      OSTNU.OSTNUCheckStatus checkStatus
      Agile status

    • contingentAlsoAsOrdinary

      boolean contingentAlsoAsOrdinary
      Represent contingent links also as ordinary constraints.

    • lowerContingentEdge

      it.unimi.dsi.fastutil.objects.Object2ObjectMap<LabeledNode,OSTNUEdgePluggable> lowerContingentEdge
      Utility map that returns the edge containing the lower-case constraint of a contingent link given the contingent timepoint.

    • oracleNode

      it.unimi.dsi.fastutil.objects.Object2ObjectMap<LabeledNode,LabeledNode> oracleNode
      Utility map that returns the oracle node O_C associated with a contingent node C. The oracle node contains the contingent node name in its 'proposition' field. The map is '(C, O_C)'.

  • Constructor Details

    • OSTNU

      public OSTNU(String graphXML) throws IOException, ParserConfigurationException, SAXException
      Helper constructor for CSTNU.

      This constructor is useful for making the use of this class easier in an environment like 'Node.js-Java'.

      Parameters:
      graphXML - the TNGraph to check in GraphML format
      Throws:
      IOException - if any error occurs during the graphXML reading
      ParserConfigurationException - if graphXML contains a character that cannot be parsed
      SAXException - if graphXML is not valid

    • OSTNU

      public OSTNU(TNGraph<OSTNUEdgePluggable> graph, int giveTimeOut)
      Constructor for CSTNU
      Parameters:
      graph - TNGraph to check
      giveTimeOut - timeout for the check in seconds

    • OSTNU

      public OSTNU(TNGraph<OSTNUEdgePluggable> graph)
      Constructor for CSTNU
      Parameters:
      graph - TNGraph to check

    • OSTNU

      OSTNU()
      Default constructor, package use only!

  • Method Details

    • lowerCaseValueAsString

      static String lowerCaseValueAsString(ALabel nodeName, int value, Label label)
      Parameters:
      nodeName - node name to put as a lower-case label
      value - value
      label - label to represent
      Returns:
      the conventional representation of a labeled value

    • main

      public static void main(String[] args) throws IOException, ParserConfigurationException, SAXException
      Reads a CSTNU file and checks it.
      Parameters:
      args - an array of String objects.
      Throws:
      IOException - if any.
      ParserConfigurationException - if any.
      SAXException - if any.

    • upperCaseValueAsString

      static String upperCaseValueAsString(ALabel nodeName, int value, Label label)
      Parameters:
      nodeName - node name to put as an uppercase label
      value - value
      label - label to represent
      Returns:
      the conventional representation of a labeled value

    • agileControllabilityCheck

      public OSTNU.OSTNUCheckStatus agileControllabilityCheck() throws WellDefinitionException
      Checks the agile controllability (AC) of the given network (see OSTNU(TNGraph) or AbstractCSTN.setG(TNGraph)).

      If the network is AC, it determines all the minimal ranges for the constraints.

      During the execution of this method, the given network is modified.

      If the check is successful, all constraints to node Z in the network are minimized; otherwise, the network contains at least one negative loop.

      After a check, AbstractCSTN.getGChecked() returns the graph resulting from the check, and getCheckStatus() returns the result of the checking action with some statistics, and the node with the negative loop is the network is NOT DC.
      In any case, before returning, this method call AbstractCSTN.saveGraphToFile() for saving the computed graph.

      Returns:
      an OSTNU.OSTNUCheckStatus object containing the final status and some statistics about the executed checking.
      Throws:
      WellDefinitionException - if any.

    • dynamicConsistencyCheck

      public OSTNU.OSTNUCheckStatus dynamicConsistencyCheck() throws WellDefinitionException
      Checks the dynamic consistency (DC) of a CSTN instance within timeout seconds. During the execution of this method, the given network is modified.

      If the check is successful, all constraints to node Z in the network are minimized; otherwise, the network contains at least one negative loop.

      After a check, AbstractCSTN.getGChecked() returns the network determined by the check and AbstractCSTN.getCheckStatus() the result of the checking action with some statistics, and the node having a negative loop if the network is NOT DC.

      In any case, before returning, this method call AbstractCSTN.saveGraphToFile() for saving the computed graph. Wrapper method for agileControllabilityCheck()

      Specified by:
      dynamicConsistencyCheck in class AbstractCSTN<OSTNUEdgePluggable>
      Returns:
      the final status of the checking with some statistics.
      Throws:
      WellDefinitionException - if any.

    • getCheckStatus

      public OSTNU.OSTNUCheckStatus getCheckStatus()
      Getter for the field checkStatus, the status of a checking algorithm.
      Overrides:
      getCheckStatus in class AbstractCSTN<OSTNUEdgePluggable>
      Returns:
      the status of a checking algorithm. At the end of the run, the final status and some statistics are presented.

    • initAndCheck

      public void initAndCheck() throws WellDefinitionException
      Checks and initializes the CSTN instance represented by graph g. The check is made by AbstractCSTN.coreCSTNInitAndCheck().

      Since many DC checking algorithms are complete if and only if the CSTN instance contains an upper bound to the distance from Z (the first node) for each node, this method also calls AbstractCSTN.addUpperBounds() for adding such bounds as constraints between Z and each node.

      Calls and then checks all contingent links. This method works only with streamlined instances!

      Overrides:
      initAndCheck in class AbstractCSTN<OSTNUEdgePluggable>
      Throws:
      WellDefinitionException - if the initial graph is not well-defined. We preferred to throw an exception instead of returning a negative status to stress that any further operation cannot be made on this instance.
      See Also:

    • oneStepAgileControllability

      public OSTNU.OSTNUCheckStatus oneStepAgileControllability(AbstractCSTN.EdgesToCheck<OSTNUEdgePluggable> edgesToCheck, Instant timeoutInstant)
      Executes one step of the agile controllability check.

      Before the first execution of this method, it is necessary to execute initAndCheck().

      Parameters:
      edgesToCheck - set of edges that have to be checked.
      timeoutInstant - the time instant limit allowed for the computation.
      Returns:
      the updated status (for convenience, it is not necessary because it returns the same parameter status).

    • reset

      public void reset()
      Resets all internal structures
      Overrides:
      reset in class AbstractCSTN<OSTNUEdgePluggable>

    • checkAndManageIfNewLabeledValueIsANegativeLoop

      boolean checkAndManageIfNewLabeledValueIsANegativeLoop(int value, @Nonnull Label label, @Nonnull LabeledNode source, @Nonnull LabeledNode destination, @Nonnull OSTNUEdgePluggable newEdge)
      Checks if a new labeled value is negative and represents a negative cycle. In such a case, update the status by adding the new scenario to the list of negative scenarios.
      Parameters:
      value - value
      label - label of the value
      source - source node
      destination - destination node
      newEdge - new edge
      Returns:
      true if a negative loop has been found in the given scenario, and that there is no alternative scenario to it (i.e., there are two scenarios that present negative loop w.r.t. the value generated by a contingent time point, one using oracle, one not using oracle).

    • getLabel4ValueInvolvingContingent

      @Nonnull Label getLabel4ValueInvolvingContingent(@Nonnull LabeledNode contingent, @Nonnull LabeledNode node, boolean straight)
      Parameters:
      contingent - contingent node
      node - the other node for which it is necessary to determine the label for the constraint involving the contingent node.
      straight - true if the label is relative to the value determined by the oracle rule; otherwise, it is false.
      Returns:
      the label used by lower case/upper case/oracle rules to label values involving the contingent node.

    • isAllMaxMinimalGraphConsistent

      boolean isAllMaxMinimalGraphConsistent(@Nonnull TNGraph<OSTNUEdgePluggable> graph)
      Determines the minimal distance between all pairs of vertices of the given graph if the graph is consistent, i.e., it does not contain any negative cycles.
      Parameters:
      graph - the graph. It will be modified
      Returns:
      true if the input graph is consistent, i.e., it does not contain any negative cycle; false otherwise.

    • labeledCrossCaseRule

      void labeledCrossCaseRule(@Nonnull LabeledNode nA, @Nonnull LabeledNode nC, @Nonnull LabeledNode nX, @Nonnull OSTNUEdgePluggable eAC, @Nonnull OSTNUEdgePluggable eCX, @Nonnull OSTNUEdgePluggable eAX)
      Labeled Cross-Case Rule 
       A ---(u,c,α)--→ C ---(v,D,β)--→ X
 adds
 A ---(u+v,D,αβ)--→ X

 if αβ∈P, C != D, and v ≤ 0.
      Since it is assumed that L(C)=L(A)=α, there is only ONE lower-case labeled value u,c,α!
      Parameters:
      nA - node
      nC - node
      nX - node
      eAC - CANNOT BE NULL
      eCX - CANNOT BE NULL
      eAX - CANNOT BE NULL

    • labeledLetterRemovalRule

      boolean labeledLetterRemovalRule(@Nonnull LabeledNode nX, @Nonnull LabeledNode nA, @Nonnull OSTNUEdgePluggable eXA)
      Labeled Letter Removal Since this algorithm does not manage if two contingent timepoints have a strict range, and they require oracles, one way to capture such a situation is to not remove the letter to a wait when X is an activation or contingent time point.

      2025-03-17: After some tests, I verified that in case of NOT AC instance, it is better not to execute this method because the check is faster. In the case of the 'AC' instance, without this method, the check is a little longer, and the final instance contains many positive waits that can be simplified by removing the letter. I maintain the use of the method only to avoid a 'dirty' AC instance. 

       X ---(v,ℵ,β)--→ A ---(x,c,α)--→ C
 adds
 X ---(m,ℵ',β)---→ A

 if C ∈ ℵ, m = max(v, −x), β entails α, and X is not an activation timepoint.
 ℵ'=ℵ'/C
      Parameters:
      nX - node external node
      nA - activation node
      eXA - edge
      Returns:
      true if a letter was removed

    • labeledLowerCaseRule

      void labeledLowerCaseRule(@Nonnull LabeledNode nA, @Nonnull LabeledNode nC, @Nonnull LabeledNode nX, @Nonnull OSTNUEdgePluggable eAC, @Nonnull OSTNUEdgePluggable eCX, @Nonnull OSTNUEdgePluggable eAX)
      Labeled Lower Case Rule 
       X ←--(-u,◇,β)--- C ←--(x,c,α)----- A
   ---(v,◇,β')---→   --(-y,◇,-----→
 adds
 X ←-----(x-u,◇,¬cαββ')------------ A

 if ¬cαββ'∈P, -u≤0, and (Oracle O_C does not exist or v-u≥y-x).

      Since it is assumed that L(C)=L(A), there is only ONE lower-case labeled value u,c,α!

      Parameters:
      nA - node
      nC - node
      nX - node
      eAC - CANNOT BE NULL
      eCX - CANNOT BE NULL
      eAX - CANNOT BE NULL

    • labeledOracleRule

      void labeledOracleRule(@Nonnull LabeledNode nA, @Nonnull LabeledNode nC, @Nonnull LabeledNode nX, @Nonnull OSTNUEdgePluggable eAC, @Nonnull OSTNUEdgePluggable eCX, @Nonnull OSTNUEdgePluggable eAX)
      Oracle rule. 
       X ---(v,◇,β)-→ C ---(-y,C,α)-→ A
  ←--(-u,◇,β')--|  ←--(x,c,α)---
                |
                (0)
                |
                ↓
               O_C
 adds
 X ---(v-x,◇,αcβ)--------------→ A
  ←--(y-u,◇,αcβ')-----------------|
  |              C              |
  |              |              |
  |             (-u,◇,αcββ')     |
  |             |               |
  |             ↓               |
  |-(0,◇,αcββ')→ O_C ←(x-u,◇,αcββ')

 when X is not contingent,
 αcββ' is consistent, and a negative scenario does not subsume it,
 and v-u < y-x
      Parameters:
      nA - node
      nC - node
      nX - node
      eAC - CANNOT BE NULL
      eCX - CANNOT BE NULL
      eAX - CANNOT BE NULL

    • labeledPropagationRule

      void labeledPropagationRule(@Nonnull LabeledNode nX, @Nonnull LabeledNode nY, @Nonnull LabeledNode nW, @Nonnull OSTNUEdgePluggable eXY, @Nonnull OSTNUEdgePluggable eYW, @Nonnull OSTNUEdgePluggable eXW)
      Applies 'labeled no case' or 'labeled upper case propagation' rules.
       1) CASE labeled no case, labeled upper case propagation
 X ----(u,◇,α)---→ Y ----(v,ℵ,β)-----→ W
 adds
 X -----------(u+v,ℵ,αβ)------------→  W
 ℵ can be empty. αβ must be consistent and not in negative scenarios
      Parameters:
      nX - node
      nY - node
      nW - node
      eXY - CANNOT BE NULL
      eYW - CANNOT BE NULL
      eXW - CANNOT BE NULL

    • labeledUpperCaseRule

      void labeledUpperCaseRule(@Nonnull LabeledNode nX, @Nonnull LabeledNode nC, @Nonnull LabeledNode nA, @Nonnull OSTNUEdgePluggable eXC, @Nonnull OSTNUEdgePluggable eCA, @Nonnull OSTNUEdgePluggable eXA)
      Applies 'labeled upper case' rules.
       2) labeled in case
 A ←--(-y,C,𝛂)---- C ←-(v,◇,β)-------- X
   ---(x,C,𝛂)----→   --(-u,◇,β')-----→
 adds
 A ←---(y+v,C,¬c𝛂ββ')----------------- X
 when ¬c𝛂ββ' is consistent and a negative scenario does not subsume it.
 Oracle for Y does not exist, or v-u ≥ y-x.
      Parameters:
      nX - external node
      nC - contingent node
      nA - activation node
      eXC - CANNOT BE NULL
      eCA - CANNOT BE NULL
      eXA - CANNOT BE NULL

    • makeAllMaxProjection

      TNGraph<OSTNUEdgePluggable> makeAllMaxProjection()

    • removeLabeledValuesBelongingToNegativeScenarios

      void removeLabeledValuesBelongingToNegativeScenarios()
      Removes all labeled values belonging to negative scenarios.