Name: |
genbuf5.tlsf |
md5: |
604c86d724b7bacb01518b0c91307349 |
FractionOfBinaryClauses |
None |
FractionOfNegativeLiteralsPerClauseEntropy |
None |
FractionOfNegativeLiteralsPerClauseMax |
None |
FractionOfNegativeLiteralsPerClauseMean |
None |
FractionOfNegativeLiteralsPerClauseMin |
None |
FractionOfNegativeLiteralsPerClauseVariationCoefficient |
None |
FractionOfNegativeVariablesEntropy |
None |
FractionOfNegativeVariablesMax |
None |
FractionOfNegativeVariablesMean |
None |
FractionOfNegativeVariablesMin |
None |
FractionOfNegativeVariablesVariationCoefficient |
None |
FractionOfPositiveLiteralsPerClauseEntropy |
None |
FractionOfPositiveLiteralsPerClauseMax |
None |
FractionOfPositiveLiteralsPerClauseMean |
None |
FractionOfPositiveLiteralsPerClauseMin |
None |
FractionOfPositiveLiteralsPerClauseVariationCoefficient |
None |
FractionOfPositiveVariablesEntropy |
None |
FractionOfPositiveVariablesMax |
None |
FractionOfPositiveVariablesMean |
None |
FractionOfPositiveVariablesMin |
None |
FractionOfPositiveVariablesVariationCoefficient |
None |
FractionOfTernaryClauses |
None |
FractionOfUnaryClauses |
None |
ClausesToVariablesRatio |
None |
ClausesToVariablesRatioCubic |
None |
ClausesToVariablesRatioQuadratic |
None |
LinearizedClausesToVariablesRatio |
None |
LinearizedClausesToVariablesRatioQuadratic |
None |
LinearizedClaustesToVariablesRatioCubic |
None |
NumberOfClauses |
None |
NumberOfVariables |
None |
VariablesToClausesRatio |
None |
VariablesToClausesRatioCubic |
None |
VariablesToClausesRatioQuadratic |
None |
ClauseNodeDegreesEntropy |
None |
ClauseNodeDegreesMax |
None |
ClauseNodeDegreesMean |
None |
ClauseNodeDegreesMin |
None |
ClauseNodeDegreesVariationCoefficient |
None |
VariableNodeDegreesEntropy |
None |
VariableNodeDegreesMax |
None |
VariableNodeDegreesMean |
None |
VariableNodeDegreesMin |
None |
VariableNodeDegreesVariationCoefficient |
None |
DegreeEntropy |
None |
DegreeMax |
None |
DegreeMean |
None |
DegreeMin |
None |
DegreeVariationCoefficient |
None |
INFO {
TITLE: "Generalized Buffer - 5 Receivers"
DESCRIPTION: "One of the Acacia+ Example files"
SEMANTICS: Mealy
TARGET: Mealy
}
MAIN {
INPUTS {
s2b_req0;
s2b_req1;
r2b_ack0;
r2b_ack1;
r2b_ack2;
r2b_ack3;
r2b_ack4;
}
OUTPUTS {
b2s_ack0;
b2s_ack1;
b2r_req0;
b2r_req1;
b2r_req2;
b2r_req3;
b2r_req4;
}
GUARANTEES {
// [spec_unit s2b_0]
(!s2b_req0 && G (s2b_req0 && !b2s_ack0 -> X s2b_req0) && G (b2s_ack0 -> X !s2
... [truncated 3.6 kB]
2r_req4 && X !b2r_req4 -> X (!b2r_req4 U (!b2r_req4 && b2r_req3))) &&
G ((s2b_req0 || s2b_req1) -> X F (b2r_req0 || b2r_req1 || b2r_req2 || b2r_req3 || b2r_req4)) &&
G ((!b2r_req0 && !b2r_req1 && !b2r_req2 && !b2r_req3) ||
(!b2r_req1 && !b2r_req2 && !b2r_req3 && !b2r_req4) ||
(!b2r_req2 && !b2r_req3 && !b2r_req4 && !b2r_req0) ||
(!b2r_req3 && !b2r_req4 && !b2r_req0 && !b2r_req1) ||
(!b2r_req4 && !b2r_req0 && !b2r_req1 && !b2r_req2)));
}
}