Class PCSTNU
- 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 the paper about Parameter-CSTNU.(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, and C rules of the 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.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.(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
Version of the class- See Also:
-
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
- Parameters:
graph
- a parameterized CSTNU
-
PCSTNU
- Parameters:
graph
- a parameterized CSTNUgiveTimeOut
- maximum duration (in seconds) for the DC checking.
-
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.
-
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 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!
Calls and then checks 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:
-
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 classCSTNU
- 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).
-
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 is limited to Z because it is inherited from CSTNU, but such a method also calls others that consider parameter nodes as Z nodes.
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 this aspect.
- Overrides:
oneStepDynamicControllabilityLimitedToZ
in classCSTNU
- 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).
-
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 at least once.
-
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.
-
labelPropagation
boolean labelPropagation(LabeledNode nX, LabeledNode nY, LabeledNode nW, CSTNUEdge eXY, CSTNUEdge eYW, CSTNUEdge eXW) Apply A, A-Parameter, and C rules of the 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 a 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 a 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 the 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.
-
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 a 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 a 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
-