public class JoinAppIntermediate extends BuiltInAppIntermediate
Modifier and Type | Field and Description |
---|---|
private String |
distinguishingFormula |
private int |
id |
private String |
joinProc |
private int |
nrPartners |
Constructor and Description |
---|
JoinAppIntermediate(String ruleName,
Pair<Integer,PosInTerm> pos,
int id,
String joinProc,
int nrPartners,
ImmutableList<Name> newNames,
String distinguishingFormula)
Constructs a new join rule.
|
Modifier and Type | Method and Description |
---|---|
String |
getDistinguishingFormula() |
int |
getId() |
String |
getJoinProc() |
int |
getNrPartners() |
getBuiltInIfInsts, getContract, getNewNames, getPosInfo, getRuleName
getLineNr, setLineNr
private int id
private String joinProc
private String distinguishingFormula
private int nrPartners
public JoinAppIntermediate(String ruleName, Pair<Integer,PosInTerm> pos, int id, String joinProc, int nrPartners, ImmutableList<Name> newNames, String distinguishingFormula)
ruleName
- Name of the rule; should be "JoinRule".pos
- Position information for the join rule application (Symbolic
State - Program Counter formula).id
- ID of the join rule application (should have been stored
during proof saving and should match the joinNodeId fields of
the corresponding partner nodes).joinProc
- The name of the join procedure used during joining.nrPartners
- Number of involved join partners.newNames
- New names registered in the course of the join rule
application.distinguishingFormula
- The user-supplied distinguishing formula for the join.public int getId()
public String getJoinProc()
public int getNrPartners()
public String getDistinguishingFormula()