From f32210b3dab07f6a9f04f175e2c6813cbf9d6316 Mon Sep 17 00:00:00 2001 From: nick_battle Date: Mon, 13 Nov 2023 19:42:27 +0000 Subject: [PATCH] Define PO definition for some more obligations --- .../java/com/fujitsu/vdmj/pog/SatisfiabilityObligation.java | 2 ++ .../src/main/java/com/fujitsu/vdmj/pog/StateInitObligation.java | 1 + 2 files changed, 3 insertions(+) diff --git a/vdmj/src/main/java/com/fujitsu/vdmj/pog/SatisfiabilityObligation.java b/vdmj/src/main/java/com/fujitsu/vdmj/pog/SatisfiabilityObligation.java index 130235cad..ff83f4b83 100644 --- a/vdmj/src/main/java/com/fujitsu/vdmj/pog/SatisfiabilityObligation.java +++ b/vdmj/src/main/java/com/fujitsu/vdmj/pog/SatisfiabilityObligation.java @@ -43,6 +43,7 @@ public class SatisfiabilityObligation extends ProofObligation public SatisfiabilityObligation(POImplicitFunctionDefinition func, POContextStack ctxt) { super(func.location, POType.FUNC_SATISFIABILITY, ctxt); + this.definition = func; StringBuilder sb = new StringBuilder(); if (func.predef != null) @@ -137,6 +138,7 @@ public SatisfiabilityObligation(POTypeDefinition typedef, POContextStack ctxt) public SatisfiabilityObligation(POStateDefinition statedef, POContextStack ctxt) { super(statedef.location, POType.INV_SATISFIABILITY, ctxt); + this.definition = statedef.invdef; StringBuilder sb = new StringBuilder(); sb.append("exists "); diff --git a/vdmj/src/main/java/com/fujitsu/vdmj/pog/StateInitObligation.java b/vdmj/src/main/java/com/fujitsu/vdmj/pog/StateInitObligation.java index 4d3374b50..06235616d 100644 --- a/vdmj/src/main/java/com/fujitsu/vdmj/pog/StateInitObligation.java +++ b/vdmj/src/main/java/com/fujitsu/vdmj/pog/StateInitObligation.java @@ -31,6 +31,7 @@ public class StateInitObligation extends ProofObligation public StateInitObligation(POStateDefinition def, POContextStack ctxt) { super(def.location, POType.STATE_INIT, ctxt); + this.definition = def.initdef; value = ctxt.getObligation("exists " + def.initPattern + " : " + def.name + " & " + def.initExpression); } }