From 9618ecb7e7738a8cb6a566f9959fe65ee9822acf Mon Sep 17 00:00:00 2001 From: Nick Battle Date: Fri, 18 Oct 2024 10:09:50 +0100 Subject: [PATCH 1/4] Defend qcrun against state POs --- .../main/java/com/fujitsu/vdmj/pog/ProofObligation.java | 7 +++++++ 1 file changed, 7 insertions(+) diff --git a/vdmj/src/main/java/com/fujitsu/vdmj/pog/ProofObligation.java b/vdmj/src/main/java/com/fujitsu/vdmj/pog/ProofObligation.java index 0f81390ca..846650796 100644 --- a/vdmj/src/main/java/com/fujitsu/vdmj/pog/ProofObligation.java +++ b/vdmj/src/main/java/com/fujitsu/vdmj/pog/ProofObligation.java @@ -28,7 +28,9 @@ import com.fujitsu.vdmj.po.annotations.POAnnotationList; import com.fujitsu.vdmj.po.definitions.PODefinition; import com.fujitsu.vdmj.po.definitions.POExplicitFunctionDefinition; +import com.fujitsu.vdmj.po.definitions.POExplicitOperationDefinition; import com.fujitsu.vdmj.po.definitions.POImplicitFunctionDefinition; +import com.fujitsu.vdmj.po.definitions.POImplicitOperationDefinition; import com.fujitsu.vdmj.po.patterns.POPattern; import com.fujitsu.vdmj.po.patterns.POPatternList; import com.fujitsu.vdmj.po.patterns.visitors.POGetMatchingConstantVisitor; @@ -277,6 +279,11 @@ else if (definition instanceof POImplicitFunctionDefinition) POImplicitFunctionDefinition ifd = (POImplicitFunctionDefinition)definition; return launchImplicitFunction(ifd, ctxt); } + else if (definition instanceof POExplicitOperationDefinition || + definition instanceof POImplicitOperationDefinition) + { + return null; // Can't do these yet + } else if (kind.isStandAlone()) { // PO is a stand alone expression, so just execute that From 393a1c556c5830f719cf1f68075181297eceda9d Mon Sep 17 00:00:00 2001 From: Nick Battle Date: Fri, 18 Oct 2024 11:53:02 +0100 Subject: [PATCH 2/4] Add operations to qcrun launches --- .../POExplicitOperationDefinition.java | 8 +- .../POImplicitFunctionDefinition.java | 8 +- .../POImplicitOperationDefinition.java | 8 +- .../vdmj/pog/ParameterPatternObligation.java | 3 +- .../com/fujitsu/vdmj/pog/ProofObligation.java | 135 ++++++++++-------- 5 files changed, 83 insertions(+), 79 deletions(-) diff --git a/vdmj/src/main/java/com/fujitsu/vdmj/po/definitions/POExplicitOperationDefinition.java b/vdmj/src/main/java/com/fujitsu/vdmj/po/definitions/POExplicitOperationDefinition.java index 9ef11795c..00b8db519 100644 --- a/vdmj/src/main/java/com/fujitsu/vdmj/po/definitions/POExplicitOperationDefinition.java +++ b/vdmj/src/main/java/com/fujitsu/vdmj/po/definitions/POExplicitOperationDefinition.java @@ -24,9 +24,6 @@ package com.fujitsu.vdmj.po.definitions; -import java.util.List; -import java.util.Vector; - import com.fujitsu.vdmj.Release; import com.fujitsu.vdmj.Settings; import com.fujitsu.vdmj.lex.Dialect; @@ -35,6 +32,7 @@ import com.fujitsu.vdmj.po.expressions.POExpression; import com.fujitsu.vdmj.po.patterns.POPattern; import com.fujitsu.vdmj.po.patterns.POPatternList; +import com.fujitsu.vdmj.po.patterns.POPatternListList; import com.fujitsu.vdmj.po.statements.POStatement; import com.fujitsu.vdmj.pog.OperationPostConditionObligation; import com.fujitsu.vdmj.pog.POContextStack; @@ -213,9 +211,9 @@ else if (precondition != null) // pre_op undefined in VDM++ return obligations; } - public List getParamPatternList() + public POPatternListList getParamPatternList() { - List list = new Vector(); + POPatternListList list = new POPatternListList(); list.add(parameterPatterns); return list; } diff --git a/vdmj/src/main/java/com/fujitsu/vdmj/po/definitions/POImplicitFunctionDefinition.java b/vdmj/src/main/java/com/fujitsu/vdmj/po/definitions/POImplicitFunctionDefinition.java index 58a2d68a4..de1724377 100644 --- a/vdmj/src/main/java/com/fujitsu/vdmj/po/definitions/POImplicitFunctionDefinition.java +++ b/vdmj/src/main/java/com/fujitsu/vdmj/po/definitions/POImplicitFunctionDefinition.java @@ -24,15 +24,13 @@ package com.fujitsu.vdmj.po.definitions; -import java.util.List; -import java.util.Vector; - import com.fujitsu.vdmj.po.annotations.POAnnotationList; import com.fujitsu.vdmj.po.definitions.visitors.PODefinitionVisitor; import com.fujitsu.vdmj.po.expressions.POExpression; import com.fujitsu.vdmj.po.expressions.PONotYetSpecifiedExpression; import com.fujitsu.vdmj.po.patterns.POPattern; import com.fujitsu.vdmj.po.patterns.POPatternList; +import com.fujitsu.vdmj.po.patterns.POPatternListList; import com.fujitsu.vdmj.po.types.POPatternListTypePair; import com.fujitsu.vdmj.po.types.POPatternListTypePairList; import com.fujitsu.vdmj.po.types.POPatternTypePair; @@ -214,9 +212,9 @@ public ProofObligationList getProofObligations(POContextStack ctxt, Environment return obligations; } - public List getParamPatternList() + public POPatternListList getParamPatternList() { - List list = new Vector(); + POPatternListList list = new POPatternListList(); POPatternList onelist = new POPatternList(); for (POPatternListTypePair p: parameterPatterns) diff --git a/vdmj/src/main/java/com/fujitsu/vdmj/po/definitions/POImplicitOperationDefinition.java b/vdmj/src/main/java/com/fujitsu/vdmj/po/definitions/POImplicitOperationDefinition.java index 01cbb1039..050655b17 100644 --- a/vdmj/src/main/java/com/fujitsu/vdmj/po/definitions/POImplicitOperationDefinition.java +++ b/vdmj/src/main/java/com/fujitsu/vdmj/po/definitions/POImplicitOperationDefinition.java @@ -24,9 +24,6 @@ package com.fujitsu.vdmj.po.definitions; -import java.util.List; -import java.util.Vector; - import com.fujitsu.vdmj.Release; import com.fujitsu.vdmj.Settings; import com.fujitsu.vdmj.lex.Dialect; @@ -35,6 +32,7 @@ import com.fujitsu.vdmj.po.expressions.POExpression; import com.fujitsu.vdmj.po.patterns.POPattern; import com.fujitsu.vdmj.po.patterns.POPatternList; +import com.fujitsu.vdmj.po.patterns.POPatternListList; import com.fujitsu.vdmj.po.statements.POErrorCaseList; import com.fujitsu.vdmj.po.statements.POExternalClauseList; import com.fujitsu.vdmj.po.statements.POStatement; @@ -251,9 +249,9 @@ else if (precondition != null) // pre_op state param undefined in VDM++ return obligations; } - public List getListParamPatternList() + public POPatternListList getListParamPatternList() { - List list = new Vector(); + POPatternListList list = new POPatternListList(); for (POPatternListTypePair p: parameterPatterns) { diff --git a/vdmj/src/main/java/com/fujitsu/vdmj/pog/ParameterPatternObligation.java b/vdmj/src/main/java/com/fujitsu/vdmj/pog/ParameterPatternObligation.java index f0e3666f1..acf349f71 100644 --- a/vdmj/src/main/java/com/fujitsu/vdmj/pog/ParameterPatternObligation.java +++ b/vdmj/src/main/java/com/fujitsu/vdmj/pog/ParameterPatternObligation.java @@ -41,6 +41,7 @@ import com.fujitsu.vdmj.po.expressions.POExpression; import com.fujitsu.vdmj.po.patterns.POPattern; import com.fujitsu.vdmj.po.patterns.POPatternList; +import com.fujitsu.vdmj.po.patterns.POPatternListList; import com.fujitsu.vdmj.tc.types.TCFunctionType; import com.fujitsu.vdmj.tc.types.TCType; import com.fujitsu.vdmj.tc.types.TCTypeList; @@ -85,7 +86,7 @@ public ParameterPatternObligation( generate(def.getListParamPatternList(), def.type.parameters, def.type.result)); } - private String generate(List plist, TCTypeList params, TCType result) + private String generate(POPatternListList plist, TCTypeList params, TCType result) { StringBuilder foralls = new StringBuilder(); StringBuilder argnames = new StringBuilder(); diff --git a/vdmj/src/main/java/com/fujitsu/vdmj/pog/ProofObligation.java b/vdmj/src/main/java/com/fujitsu/vdmj/pog/ProofObligation.java index 846650796..7f93b7c0c 100644 --- a/vdmj/src/main/java/com/fujitsu/vdmj/pog/ProofObligation.java +++ b/vdmj/src/main/java/com/fujitsu/vdmj/pog/ProofObligation.java @@ -33,14 +33,17 @@ import com.fujitsu.vdmj.po.definitions.POImplicitOperationDefinition; import com.fujitsu.vdmj.po.patterns.POPattern; import com.fujitsu.vdmj.po.patterns.POPatternList; +import com.fujitsu.vdmj.po.patterns.POPatternListList; import com.fujitsu.vdmj.po.patterns.visitors.POGetMatchingConstantVisitor; import com.fujitsu.vdmj.po.patterns.visitors.POGetMatchingExpressionVisitor; import com.fujitsu.vdmj.po.patterns.visitors.PORemoveIgnoresVisitor; import com.fujitsu.vdmj.po.types.POPatternListTypePair; +import com.fujitsu.vdmj.po.types.POPatternListTypePairList; import com.fujitsu.vdmj.runtime.Context; import com.fujitsu.vdmj.runtime.Interpreter; import com.fujitsu.vdmj.tc.expressions.TCExistsExpression; import com.fujitsu.vdmj.tc.expressions.TCExpression; +import com.fujitsu.vdmj.tc.lex.TCNameToken; import com.fujitsu.vdmj.tc.types.TCParameterType; import com.fujitsu.vdmj.tc.types.TCType; import com.fujitsu.vdmj.tc.types.TCTypeList; @@ -269,48 +272,69 @@ public String getWitnessLaunch() public String getLaunch(Context ctxt) { - if (definition instanceof POExplicitFunctionDefinition) + try { - POExplicitFunctionDefinition efd = (POExplicitFunctionDefinition)definition; - return launchExplicitFunction(efd, ctxt); - } - else if (definition instanceof POImplicitFunctionDefinition) - { - POImplicitFunctionDefinition ifd = (POImplicitFunctionDefinition)definition; - return launchImplicitFunction(ifd, ctxt); - } - else if (definition instanceof POExplicitOperationDefinition || - definition instanceof POImplicitOperationDefinition) - { - return null; // Can't do these yet + if (definition instanceof POExplicitFunctionDefinition) + { + POExplicitFunctionDefinition efd = (POExplicitFunctionDefinition)definition; + return + launchNameTypes(efd.name, efd.typeParams, ctxt) + + launchArguments(efd.paramPatternList, ctxt); + } + else if (definition instanceof POImplicitFunctionDefinition) + { + POImplicitFunctionDefinition ifd = (POImplicitFunctionDefinition)definition; + return + launchNameTypes(ifd.name, ifd.typeParams, ctxt) + + launchArguments(ifd.parameterPatterns, ctxt); + } + else if (definition instanceof POExplicitOperationDefinition) + { + POExplicitOperationDefinition eop = (POExplicitOperationDefinition)definition; + return + launchNameTypes(eop.name, null, ctxt) + + launchArguments(eop.getParamPatternList(), ctxt); + } + else if (definition instanceof POImplicitOperationDefinition) + { + POImplicitOperationDefinition iop = (POImplicitOperationDefinition)definition; + return + launchNameTypes(iop.name, null, ctxt) + + launchArguments(iop.parameterPatterns, ctxt); + } + else if (kind.isStandAlone()) + { + // PO is a stand alone expression, so just execute that + return source.trim(); + } } - else if (kind.isStandAlone()) + catch (Exception e) { - // PO is a stand alone expression, so just execute that - return source.trim(); + // Cannot match all parameters from context } - return null; // Unexpected definition + return null; } - private String launchExplicitFunction(POExplicitFunctionDefinition efd, Context ctxt) + private String launchNameTypes(TCNameToken name, TCTypeList typeParams, Context ctxt) throws Exception { - StringBuilder callString = new StringBuilder(efd.name.getName()); + StringBuilder callString = new StringBuilder(name.getName()); PORemoveIgnoresVisitor.init(); - if (efd.typeParams != null) + if (typeParams != null) { - String inst = addTypeParams(efd.typeParams, ctxt); - - if (inst == null) - { - return null; - } - + String inst = addTypeParams(typeParams, ctxt); callString.append(inst); } - - for (POPatternList pl: efd.paramPatternList) + + return callString.toString(); + } + + private String launchArguments(POPatternListList paramPatternList, Context ctxt) throws Exception + { + StringBuilder callString = new StringBuilder(); + + for (POPatternList pl: paramPatternList) { String sep = ""; callString.append("("); @@ -318,12 +342,6 @@ private String launchExplicitFunction(POExplicitFunctionDefinition efd, Context for (POPattern p: pl) { String match = paramMatch(p.removeIgnorePatterns(), ctxt); - - if (match == null) - { - return null; // Can't match some params - } - callString.append(sep); callString.append(match); sep = ", "; @@ -335,37 +353,17 @@ private String launchExplicitFunction(POExplicitFunctionDefinition efd, Context return callString.toString(); } - private String launchImplicitFunction(POImplicitFunctionDefinition ifd, Context ctxt) + private String launchArguments(POPatternListTypePairList parameterPatterns, Context ctxt) throws Exception { - StringBuilder callString = new StringBuilder(ifd.name.getName()); - PORemoveIgnoresVisitor.init(); - - if (ifd.typeParams != null) - { - String inst = addTypeParams(ifd.typeParams, ctxt); - - if (inst == null) - { - return null; - } - - callString.append(inst); - } - + StringBuilder callString = new StringBuilder(); String sep = ""; callString.append("("); - for (POPatternListTypePair pl: ifd.parameterPatterns) + for (POPatternListTypePair pl: parameterPatterns) { for (POPattern p: pl.patterns) { String match = paramMatch(p.removeIgnorePatterns(), ctxt); - - if (match == null) - { - return null; // Can't match some params - } - callString.append(sep); callString.append(match); sep = ", "; @@ -376,8 +374,8 @@ private String launchImplicitFunction(POImplicitFunctionDefinition ifd, Context return callString.toString(); } - - private String addTypeParams(TCTypeList params, Context ctxt) + + private String addTypeParams(TCTypeList params, Context ctxt) throws Exception { StringBuilder callString = new StringBuilder(); String sep = ""; @@ -390,7 +388,7 @@ private String addTypeParams(TCTypeList params, Context ctxt) if (inst == null) { - return null; // Missing type parameter? + throw new Exception("Can't match type param " + param); } callString.append(sep); @@ -402,13 +400,24 @@ private String addTypeParams(TCTypeList params, Context ctxt) return callString.toString(); } - private String paramMatch(POPattern p, Context ctxt) + private String paramMatch(POPattern p, Context ctxt) throws Exception { POGetMatchingConstantVisitor visitor = new POGetMatchingConstantVisitor(); String result = p.apply(visitor, ctxt); - return visitor.hasFailed() ? null : result; + + if (visitor.hasFailed()) + { + throw new Exception("Can't match param " + p); + } + else + { + return result; + } } + /** + * True if the PO itself generates proof obligations. + */ public boolean hasObligations() { return hasObligations ; From e588ab3156bcd7b030b77387cbf131d6460b23c7 Mon Sep 17 00:00:00 2001 From: Nick Battle Date: Fri, 18 Oct 2024 12:14:19 +0100 Subject: [PATCH 3/4] Remove unused method --- .../java/com/fujitsu/vdmj/pog/POLetDefContext.java | 10 ---------- 1 file changed, 10 deletions(-) diff --git a/vdmj/src/main/java/com/fujitsu/vdmj/pog/POLetDefContext.java b/vdmj/src/main/java/com/fujitsu/vdmj/pog/POLetDefContext.java index 39d7c0d0c..90626b8bc 100644 --- a/vdmj/src/main/java/com/fujitsu/vdmj/pog/POLetDefContext.java +++ b/vdmj/src/main/java/com/fujitsu/vdmj/pog/POLetDefContext.java @@ -24,11 +24,8 @@ package com.fujitsu.vdmj.pog; -import com.fujitsu.vdmj.po.definitions.POAssignmentDefinition; import com.fujitsu.vdmj.po.definitions.PODefinition; import com.fujitsu.vdmj.po.definitions.PODefinitionList; -import com.fujitsu.vdmj.po.definitions.POValueDefinition; -import com.fujitsu.vdmj.po.patterns.POIdentifierPattern; public class POLetDefContext extends POContext { @@ -45,13 +42,6 @@ public POLetDefContext(PODefinition localDef) this.localDefs.add(localDef); } - public POLetDefContext(POAssignmentDefinition dcl) - { - this.localDefs = new PODefinitionList(); - this.localDefs.add(new POValueDefinition(null, - new POIdentifierPattern(dcl.name), dcl.type, dcl.expression, dcl.expType, new PODefinitionList())); - } - @Override public boolean isScopeBoundary() { From f63b67cf25c4df10bf27ded215dfe4957835799b Mon Sep 17 00:00:00 2001 From: Nick Battle Date: Fri, 18 Oct 2024 12:33:04 +0100 Subject: [PATCH 4/4] Add POGState getProofObligations to Definitions --- .../definitions/POAssignmentDefinition.java | 4 +++- .../vdmj/po/definitions/PODefinition.java | 10 +++++++++- .../vdmj/po/definitions/PODefinitionList.java | 19 +++++++++++++++++++ .../vdmj/po/statements/POBlockStatement.java | 2 +- .../java/com/fujitsu/vdmj/pog/POGState.java | 8 ++++++++ 5 files changed, 40 insertions(+), 3 deletions(-) diff --git a/vdmj/src/main/java/com/fujitsu/vdmj/po/definitions/POAssignmentDefinition.java b/vdmj/src/main/java/com/fujitsu/vdmj/po/definitions/POAssignmentDefinition.java index d06f98790..105e2c48b 100644 --- a/vdmj/src/main/java/com/fujitsu/vdmj/po/definitions/POAssignmentDefinition.java +++ b/vdmj/src/main/java/com/fujitsu/vdmj/po/definitions/POAssignmentDefinition.java @@ -27,6 +27,7 @@ import com.fujitsu.vdmj.po.definitions.visitors.PODefinitionVisitor; import com.fujitsu.vdmj.po.expressions.POExpression; import com.fujitsu.vdmj.pog.POContextStack; +import com.fujitsu.vdmj.pog.POGState; import com.fujitsu.vdmj.pog.ProofObligationList; import com.fujitsu.vdmj.pog.SubTypeObligation; import com.fujitsu.vdmj.tc.lex.TCNameToken; @@ -66,10 +67,11 @@ public TCType getType() } @Override - public ProofObligationList getProofObligations(POContextStack ctxt, Environment env) + public ProofObligationList getProofObligations(POContextStack ctxt, POGState pogState, Environment env) { ProofObligationList obligations = new ProofObligationList(); obligations.addAll(expression.getProofObligations(ctxt, env)); + obligations.stateUpdate(pogState, expression); if (!TypeComparator.isSubType(ctxt.checkType(expression, expType), type)) { diff --git a/vdmj/src/main/java/com/fujitsu/vdmj/po/definitions/PODefinition.java b/vdmj/src/main/java/com/fujitsu/vdmj/po/definitions/PODefinition.java index 63addfa20..715a35bd8 100644 --- a/vdmj/src/main/java/com/fujitsu/vdmj/po/definitions/PODefinition.java +++ b/vdmj/src/main/java/com/fujitsu/vdmj/po/definitions/PODefinition.java @@ -32,6 +32,7 @@ import com.fujitsu.vdmj.po.definitions.visitors.PODefinitionVisitor; import com.fujitsu.vdmj.po.definitions.visitors.POGetVariableNamesVisitor; import com.fujitsu.vdmj.pog.POContextStack; +import com.fujitsu.vdmj.pog.POGState; import com.fujitsu.vdmj.pog.ProofObligationList; import com.fujitsu.vdmj.tc.lex.TCNameList; import com.fujitsu.vdmj.tc.lex.TCNameToken; @@ -161,7 +162,9 @@ public boolean readsState() abstract public TCType getType(); /** - * Get a list of proof obligations for the definition. + * Get a list of proof obligations for the definition. The second method is used + * to track the POG state for updates to state variables, which is only used + * by a few definition types (eg. POAssignmentDefinitions). * * @param ctxt The call context. * @return A list of POs. @@ -170,6 +173,11 @@ public ProofObligationList getProofObligations(POContextStack ctxt, Environment { return new ProofObligationList(); } + + public ProofObligationList getProofObligations(POContextStack ctxt, POGState pogState, Environment env) + { + return getProofObligations(ctxt, env); // Default to stateless version + } /** * Implemented by all definitions to allow visitor processing. diff --git a/vdmj/src/main/java/com/fujitsu/vdmj/po/definitions/PODefinitionList.java b/vdmj/src/main/java/com/fujitsu/vdmj/po/definitions/PODefinitionList.java index 1d3e2e1f7..75a21e371 100644 --- a/vdmj/src/main/java/com/fujitsu/vdmj/po/definitions/PODefinitionList.java +++ b/vdmj/src/main/java/com/fujitsu/vdmj/po/definitions/PODefinitionList.java @@ -26,6 +26,7 @@ import com.fujitsu.vdmj.po.POMappedList; import com.fujitsu.vdmj.pog.POContextStack; +import com.fujitsu.vdmj.pog.POGState; import com.fujitsu.vdmj.pog.POLetDefContext; import com.fujitsu.vdmj.pog.PONameContext; import com.fujitsu.vdmj.pog.ProofObligationList; @@ -72,6 +73,9 @@ public String toString() return sb.toString(); } + /** + * Get the proof obligations from every definition in the list. + */ public ProofObligationList getProofObligations(POContextStack ctxt, Environment env) { ProofObligationList obligations = new ProofObligationList(); @@ -86,6 +90,21 @@ public ProofObligationList getProofObligations(POContextStack ctxt, Environment return obligations; } + /** + * Get the proof obligations from every definition in the list and track POGState. + */ + public ProofObligationList getProofObligations(POContextStack ctxt, POGState pogState, Environment env) + { + ProofObligationList obligations = new ProofObligationList(); + + for (PODefinition d: this) + { + obligations.addAll(d.getProofObligations(ctxt, pogState, env)); + } + + return obligations; + } + /** * This method gets obligations for each definition, but adds a context for each * one. This is used in let/def expressions, where definitions can depend on diff --git a/vdmj/src/main/java/com/fujitsu/vdmj/po/statements/POBlockStatement.java b/vdmj/src/main/java/com/fujitsu/vdmj/po/statements/POBlockStatement.java index b30d35fd7..c8c62745d 100644 --- a/vdmj/src/main/java/com/fujitsu/vdmj/po/statements/POBlockStatement.java +++ b/vdmj/src/main/java/com/fujitsu/vdmj/po/statements/POBlockStatement.java @@ -49,7 +49,7 @@ public POBlockStatement(LexLocation location, PODefinitionList assignmentDefs, P @Override public ProofObligationList getProofObligations(POContextStack ctxt, POGState pogState, Environment env) { - ProofObligationList obligations = assignmentDefs.getProofObligations(ctxt, env); + ProofObligationList obligations = assignmentDefs.getProofObligations(ctxt, pogState, env); ctxt.push(new POScopeContext()); obligations.addAll(super.getProofObligations(ctxt, pogState, env)); diff --git a/vdmj/src/main/java/com/fujitsu/vdmj/pog/POGState.java b/vdmj/src/main/java/com/fujitsu/vdmj/pog/POGState.java index 4abe4b574..26529f422 100644 --- a/vdmj/src/main/java/com/fujitsu/vdmj/pog/POGState.java +++ b/vdmj/src/main/java/com/fujitsu/vdmj/pog/POGState.java @@ -35,6 +35,7 @@ public class POGState public POGState() { hasUpdatedState = false; + hasReadState = false; } private POGState(boolean hasUpdatedState, boolean hasReadState) @@ -43,6 +44,13 @@ private POGState(boolean hasUpdatedState, boolean hasReadState) this.hasReadState = hasReadState; } + @Override + public String toString() + { + return (hasUpdatedState ? "has" : "has not") + " updated state; " + + (hasReadState ? "has" : "has not") + " read state"; + } + public POGState getCopy() { return new POGState(hasUpdatedState, hasReadState);