Class PCSTNU
java.lang.Object
it.univr.di.cstnu.algorithms.AbstractCSTN<CSTNUEdge>
it.univr.di.cstnu.algorithms.CSTNU
it.univr.di.cstnu.algorithms.PCSTNU
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
-
Nested Class Summary
Nested classes/interfaces inherited from class it.univr.di.cstnu.algorithms.CSTNU
CSTNU.CSTNUCheckStatus
Nested classes/interfaces inherited from class it.univr.di.cstnu.algorithms.AbstractCSTN
AbstractCSTN.CheckAlgorithm, AbstractCSTN.CSTNCheckStatus, AbstractCSTN.DCSemantics, AbstractCSTN.EdgesToCheck<E extends Edge>, AbstractCSTN.NodesToCheck
-
Field Summary
FieldsModifier and TypeFieldDescription(package private) static final Logger
logger(package private) it.unimi.dsi.fastutil.objects.ObjectArrayList
<LabeledNode> The set of parameter nodesstatic final String
Version of the classFields inherited from class it.univr.di.cstnu.algorithms.CSTNU
activationNode, contingentAlsoAsOrdinary, lowerContingentEdge
Fields inherited from class it.univr.di.cstnu.algorithms.AbstractCSTN
checkStatus, cleanCheckedInstance, FILE_NAME_SUFFIX, fInput, fOutput, g, gCheckedCleaned, horizon, maxWeight, propagationOnlyToZ, reactionTime, timeOut, versionReq, withNodeLabels, ZERO_NODE_NAME
-
Constructor Summary
Constructors -
Method Summary
Modifier and TypeMethodDescriptionvoid
Checks and initializes the CSTN instance represented by graphg
.(package private) 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(package private) boolean
labelModificationqR2
(LabeledNode nY, CSTNUEdge eZY) Apply zR2 rule assuming instantaneous reaction and a streamlined network.(package private) boolean
labelModificationR1
(LabeledNode nW, CSTNUEdge eWP, LabeledNode nObs) Apply zR1 rule assuming instantaneous reaction and a streamlined network.(package private) 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.static void
Reads a PCSTNU file and checks it.oneStepDynamicControllability
(AbstractCSTN.EdgesToCheck<CSTNUEdge> edgesToCheck, Instant timeoutInstant) Executes one step of the dynamic controllability check.
Before the first execution of this method, it is necessary to executeCSTNU.initAndCheck()
.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 executeinitAndCheck()
.
Note: this version is not optimized with respect to the number of times and edge is considered at each call.(package private) 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.(package private) 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.Methods inherited from class it.univr.di.cstnu.algorithms.CSTNU
checkAndManageIfNewLabeledValueIsANegativeLoop, checkWellDefinitionProperty1and3, dynamicConsistencyCheck, dynamicControllabilityCheck, getActivationNode, getCheckStatus, getLowerContingentLink, isActivationNode, isContingentAlsoAsOrdinary, labeledLetterRemovalRule, labelModificationqR0, labelModificationqR3, lowerCaseValueAsString, mainConditionForRestrictedLP, mainConditionForSkippingInR0qR0, reset, setContingentAlsoAsOrdinary, upperCaseValueAsString, zLabeledLetterRemovalRule
Methods inherited from class it.univr.di.cstnu.algorithms.AbstractCSTN
addUpperBounds, checkWellDefinitionProperties, checkWellDefinitionProperty2, coreCSTNInitAndCheck, getEdgeFromObserversToNode, getfOutput, getG, getGChecked, getGCheckedAsGraphML, getMaxWeight, getMinimalDistanceGraph, getReactionTime, getVersionAndCopyright, isOutputCleaned, isWithNodeLabels, labelModificationR0qR0, labelModificationR0qR0Core, mainConditionForSkippingInR3qR3, makeAlphaBetaGammaPrime4R3, makeAlphaPrime, makeBetaGammaDagger4qR3, makeNewEdge, manageParameters, newValueInR3qR3, pairAsString, removeChildrenOfUnknown, saveGraphToFile, setfOutput, setG, setOutputCleaned, setPropagationOnlyToZ, setWithNodeLabels
-
Field Details
-
VERSIONandDATE
-
LOG
logger -
parameterNodes
it.unimi.dsi.fastutil.objects.ObjectArrayList<LabeledNode> parameterNodesThe set of parameter nodes
-
-
Constructor Details
-
PCSTNU
- Parameters:
graphXML
- an XML description of a parameterized PCSTNU instance- Throws:
IOException
- any problem in reading the XMLParserConfigurationException
- any problem in the XML formatSAXException
- any problem in the XML format
-
PCSTNU
-
PCSTNU
-
PCSTNU
PCSTNU()Constructor only for the main and possible extensions.
-
-
Method Details
-
main
public static void main(String[] args) throws IOException, ParserConfigurationException, SAXException Reads a PCSTNU file and checks it.- Parameters:
args
- an array ofString
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 executeCSTNU.initAndCheck()
.- Overrides:
oneStepDynamicControllability
in classCSTNU
- 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
Checks and initializes the CSTN instance represented by graphg
. The check is made byAbstractCSTN.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 alsoAbstractCSTN.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 classCSTNU
- 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 executeinitAndCheck()
.
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 classCSTNU
- 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 classCSTNU
- Parameters:
nX
- nodenY
- nodenW
- nodeeXY
- CANNOT BE NULLeYW
- CANNOT BE NULLeXW
- 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 classCSTNU
- Parameters:
nA
- nodenC
- nodenX
- nodeeAC
- CANNOT BE NULLeCX
- CANNOT BE NULLeAX
- CANNOT BE NULL- Returns:
- true if the rule has been applied.
-
labelModificationR1
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
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 simplifyeZY
- 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
- nodenY
- nodenX
- nodeeWY
- CANNOT BE NULLeYX
- CANNOT BE NULLeWX
- 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
- nodenC
- nodenA
- nodeeWC
- CANNOT BE NULLeCA
- CANNOT BE NULLeWA
- CANNOT BE NULL- Returns:
- true if a reduction is applied at least
-