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 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 to a specific contingent node. So, if there is a contingent node 'C' and an oracle 'OC' for it, node OC ha in its observation field the value 'C'.
New upper/lower case rules and oracle rule determines new rules labeled by the fact the oracle is involved or not.
In particular, each value determined by oracle rule involving an oracle 'OC' having observation field = 'C' is labeled by 'C'. Each value determined by new lower/upper rule that involve contingent node 'C' is labeled by '¬C'.
In other words, label 'C' and label '¬C' represent two possible values generated considering contingent node 'C' that cannot be combined because they are alternative. 'C' and '¬C' can be considered literals of a boolean proposition 'C'.
Other rules, consider and propagate only values having label that are consistent, i.e., labels that not present 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:

    • checkStatus

      OSTNU.OSTNUCheckStatus checkStatus
      Agile status

    • activationNode

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

    • oracleNode

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

    • contingentAlsoAsOrdinary

      boolean contingentAlsoAsOrdinary
      Represent contingent links also as ordinary constraints.

    • lowerContingentEdge

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

  • Constructor Details

    • OSTNU

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

      This constructor is useful for making easier the use of this class in 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 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 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 upper case 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 a negative loop at least.
      After a check, AbstractCSTN.getGChecked() returns the graph resulting after the check and AbstractCSTN.getCheckStatus() 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 a negative loop at least.
      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 the 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.

    • 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 calls also AbstractCSTN.addUpperBounds() for adding such bounds as constraints between Z and each node. Calls and, then, check 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 - time instant limit allowed to the computation.
      Returns:
      the update status (for convenience. It is not necessary because return 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 adding the new scenario in 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 scenario 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 - other node for which it is necessary to determine the label for constraint involving contingent and node.
      straight - true if the label is relative to value determined using oracle rule, false otherwise.
      Returns:
      the label used by lower case/upper case/oracle rules to label values involving contingent node.

    • isAllMaxMinimalGraphConsistent

      boolean isAllMaxMinimalGraphConsistent(@Nonnull TNGraph<OSTNUEdgePluggable> graph)
      Determines the minimal distance between all pairs of vertexes 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

      void labeledLetterRemovalRule(@Nonnull LabeledNode nX, @Nonnull LabeledNode nA, @Nonnull OSTNUEdgePluggable eXA)
      Labeled Letter Removal 
       X ---(v,ℵ,β)--→ A ---(x,c,α)--→ C
 adds
 X ---(m,ℵ',β)---→ A

 if C ∈ ℵ, m = max(v, −x), β entails α.
 ℵ'=ℵ'/C
      Parameters:
      nX - node
      nA - node
      eXA - edge

    • 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 it is not subsumed by a negative scenario,
 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 upper case
 A ←--(-y,C,𝛂)---- C ←-(v,◇,β)-------- X
   ---(x,C,𝛂)----→   --(-u,◇,β')-----→
 adds
 A ←---(y+v,C,¬c𝛂ββ')----------------- X
 when ¬c𝛂ββ' is consistent and it is not subsumed by a negative scenario.
 Oracle for Y does not exist or v-u ≥ y-x.
      Parameters:
      nX - node
      nC - node
      nA - 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.