Class PCSTNU


public class PCSTNU extends CSTNU
Simple class that extends CSTNU for representing and managing also 'parameter nodes'. Parameter nodes have been introduced in the paper "Dynamic Controllability of Parameterized CSTNUs".
Author:
posenato
  • Field Details

    • VERSIONandDATE

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

      static final Logger LOG
      logger
    • parameterNodes

      it.unimi.dsi.fastutil.objects.ObjectArrayList<LabeledNode> parameterNodes
      The set of parameter nodes
  • Constructor Details

  • Method Details

    • main

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

      public CSTNU.CSTNUCheckStatus oneStepDynamicControllability(AbstractCSTN.EdgesToCheck<CSTNUEdge> edgesToCheck, Instant timeoutInstant)
      Description copied from class: CSTNU
      Executes one step of the dynamic controllability check.
      Before the first execution of this method, it is necessary to execute CSTNU.initAndCheck().
      Overrides:
      oneStepDynamicControllability in class CSTNU
      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).
    • 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! Calls and, then, check all constraints about parameter nodes. This method works only with streamlined instances!
      Overrides:
      initAndCheck in class CSTNU
      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:
    • oneStepDynamicControllabilityLimitedToZ

      public CSTNU.CSTNUCheckStatus oneStepDynamicControllabilityLimitedToZ(AbstractCSTN.EdgesToCheck<CSTNUEdge> edgesToCheck, Instant timeoutInstant)
      Executes one step of the dynamic controllability check considering only a pair of edges going to/from Z or parameter nodes.
      The name says limited to Z because it is inherited from CSTNU, but such method calls other that consider also parameter nodes as Z node.
      Before the first execution of this method, it is necessary to execute initAndCheck().
      Note: this version is not optimized with respect to the number of times and edge is considered at each call. Future versions will improve such an aspect.
      Overrides:
      oneStepDynamicControllabilityLimitedToZ in class CSTNU
      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).
    • labelPropagation

      boolean labelPropagation(LabeledNode nX, LabeledNode nY, LabeledNode nW, CSTNUEdge eXY, CSTNUEdge eYW, CSTNUEdge eXW)
      Apply A, A-Parameter, C rules of paper about Parameter-CSTNU.
       1) CASE A
              ℵ:v,β           u,α
       W==Z <------------ Y <------------ X
       adds
           ℵ:u+v,𝛾
       Z <------------------------------X
       𝛾=αβ has to be consistent and u+v < 0.
       ℵ can be empty.
       if X is parameter, set ℵ and 𝛾 empty in the generated edge
      
       2) CASE A-Parameter
              v,β           ℵ:u,α
       W==P <------------ Y <------------ X
       adds
           ℵ:u+v,𝛾
       P <------------------------------X
       P is a parameter, 𝛾=αβ has to be consistent.
       ℵ can be empty.
       if X is parameter or Z, set ℵ and 𝛾 empty in the generated edge
      
       2) CASE C
           ℵ:v,β           C:u,α
       Z <------------ Y <------------ C
       adds
           Cℵ:u+v,αβ
       Z <------------------------------C
       if u+v < 0 and αβ is consistent
       ℵ can be empty.
       
      Overrides:
      labelPropagation in class CSTNU
      Parameters:
      nX - node
      nY - node
      nW - node
      eXY - CANNOT BE NULL
      eYW - CANNOT BE NULL
      eXW - CANNOT BE NULL
      Returns:
      true if a reduction is applied at least
    • labeledCrossLowerCaseRule

      boolean labeledCrossLowerCaseRule(LabeledNode nA, LabeledNode nC, LabeledNode nX, CSTNUEdge eAC, CSTNUEdge eCX, CSTNUEdge eAX)
      Apply B and B-parameter rules of paper about Parameter-CSTNU. 1) Case B
           ℵ:v,β           c:u,α
       Z <------------ C <------------ A
       adds
                   ℵ:u+v,αβ
       Z <----------------------------A
      
       Conditions: αβ∈P*, C ∉ ℵ, u+v < 0
       

      2) Case B-parameter

           v,β             c:u,α
       X <------------ C <------------ A
       adds
                   u+v,αβ
       X <----------------------------A
      
       X is a parameter node.
       Conditions: αβ∈P*
       

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

      Overrides:
      labeledCrossLowerCaseRule in class CSTNU
      Parameters:
      nA - node
      nC - node
      nX - node
      eAC - CANNOT BE NULL
      eCX - CANNOT BE NULL
      eAX - CANNOT BE NULL
      Returns:
      true if the rule has been applied.
    • labelModificationR1

      boolean labelModificationR1(LabeledNode nW, CSTNUEdge eWP, LabeledNode nObs)
      Apply zR1 rule assuming instantaneous reaction and a streamlined network.
             v,pβ
       W ------------> P?
       adds
             v,β
       W ------------> P?
       W can be Z or a parameter node. Value v has to be >= 0
       
      Parameters:
      nW - the parameter or the Z node.
      eWP - the edge connecting W ---> P?
      nObs - the observation node
      Returns:
      true if the rule has been applied one time at least.
    • labelModificationqR2

      boolean labelModificationqR2(LabeledNode nY, CSTNUEdge eZY)
      Apply zR2 rule assuming instantaneous reaction and a streamlined network.
             v,pβ            w,𝛾
       Y <------------Z <------------ Obs?
       adds
                v,β
       Y <------------ Z
       Value w < 0, v < -w
       
      Parameters:
      nY - node destination of the edge to simplify
      eZY - edge to simplify
      Returns:
      true if a rule has been applied.
    • ruleAPlus_AparameterPlus

      boolean ruleAPlus_AparameterPlus(LabeledNode nW, LabeledNode nY, LabeledNode nX, CSTNUEdge eWY, CSTNUEdge eYX, CSTNUEdge eWX)
      Apply A^+, or A^+-Parameter of paper about Parameter-CSTNU.
       1) CASE A^+
              v,β           u,α
       W==Z ------------> Y ------------> X
       adds
           u+v,𝛾
       Z ------------------------------> X
       𝛾=αβ has to be consistent.
       if X is parameter, set 𝛾 empty in the generated edge
      
       2) CASE A^+-Parameter
              v,β           ℵ:u,α
       W==P ------------> Y ------------> X
       adds
           u+v,𝛾
       P ------------------------------>X
       P is a parameter, 𝛾=αβ has to be consistent.
       ℵ can be empty.
       if X is parameter or Z, set 𝛾 empty in the generated edge
       
      Parameters:
      nW - node
      nY - node
      nX - node
      eWY - CANNOT BE NULL
      eYX - CANNOT BE NULL
      eWX - CANNOT BE NULL
      Returns:
      true if a reduction is applied at least
    • ruleBPlus_BparameterPlus

      boolean ruleBPlus_BparameterPlus(LabeledNode nW, LabeledNode nC, LabeledNode nA, CSTNUEdge eWC, CSTNUEdge eCA, CSTNUEdge eWA)
      Apply B^+, or B^+-Parameter of paper about Parameter-CSTNU.
       1) CASE B^+ (W==Z) or CASE CASE B^+-parameter (W==parameter)
              v,β           C:u,α
       W ------------> C ------------> A
       adds
           u+v,𝛾
       Z ------------------------------> A
       𝛾=αβ has to be consistent.
       
      Parameters:
      nW - node
      nC - node
      nA - node
      eWC - CANNOT BE NULL
      eCA - CANNOT BE NULL
      eWA - CANNOT BE NULL
      Returns:
      true if a reduction is applied at least