Name: |
generalized_buffer_5.tlsf |
md5: |
755a27c332312e154e3ffc73e391eb93 |
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: "Parameterized Generalized Buffer"
DESCRIPTION: "Parameterized Generalized Buffer (generalized version of the Acacia+ benchmark)"
SEMANTICS: Mealy
TARGET: Mealy
}
GLOBAL {
PARAMETERS {
n = 5;
}
DEFINITIONS {
// ensures mutual exclusion on an n-ary bus
mutual_exclusion(bus) =
mone(bus,0,(SIZEOF bus) - 1);
// ensures that none of the signals
// bus[i] - bus[j] is HIGH
none(bus,i,j) =
&&[i <= t <= j]
!bus[t];
// ensure
... [truncated 1.1 kB]
- 1) % n]))));
}
}
MAIN {
INPUTS {
s2b_req[2];
r2b_ack[n];
}
OUTPUTS {
b2s_ack[2];
b2r_req[n];
}
GUARANTEES {
&&[0 <= i < 2]
spec_unit_s2b(s2b_req, b2s_ack, i);
&&[0 <= i < n]
spec_unit_b2r(b2r_req, r2b_ack, i);
||[0 <= i < n]
(!r2b_ack[i] && G (!b2r_req[i] -> X !r2b_ack[i]) && G (b2r_req[i] -> X F r2b_ack[i]))
-> (G ((s2b_req[0] || s2b_req[1]) -> X F ||[0 <= i < n] b2r_req[i]) &&
G mutual_exclusion(b2r_req));
}
}