public class JoinIsApplicable
extends java.lang.Object
JoinProcessor
Modifier and Type | Field and Description |
---|---|
static JoinIsApplicable |
INSTANCE |
Modifier | Constructor and Description |
---|---|
private |
JoinIsApplicable() |
Modifier and Type | Method and Description |
---|---|
private ProspectivePartner |
areProspectivePartners(Goal g1,
PosInOccurrence pio,
Goal g2)
Checks if two given goals are possible join partners for a given selected
sequent formula (defined by pio); returns a ProspectivePartner object if
this is the case and null otherwise.
|
java.util.List<ProspectivePartner> |
computeProspecitvePartner(Goal goal,
PosInOccurrence pio)
Computes the partners for the given selection.
|
java.util.List<ProspectivePartner> |
isApplicable(Goal goal,
PosInOccurrence pio) |
public static final JoinIsApplicable INSTANCE
public java.util.List<ProspectivePartner> isApplicable(Goal goal, PosInOccurrence pio)
goal
- The goal to join.pio
- Selected formula (symblic state - program counter part) for
the join.public java.util.List<ProspectivePartner> computeProspecitvePartner(Goal goal, PosInOccurrence pio)
goal
- Goal which should be joined.pio
- Selected formula (symblic state - program counter part) for
the join.private ProspectivePartner areProspectivePartners(Goal g1, PosInOccurrence pio, Goal g2)
g1
- Goal for the first node to join.pio
- Selected formula (symbolic state - program counter part) for
the join.g2
- Second goal for the join.