Name: |
loadfull5.tlsf |
md5: |
84df53a9e758a8a1363abdb58d48b39e |
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: "Load Balancing - 5 Clients"
DESCRIPTION: "One of the Acacia+ Example files"
SEMANTICS: Mealy
TARGET: Mealy
}
MAIN {
INPUTS {
idle;
request0;
request1;
request2;
request3;
request4;
}
OUTPUTS {
grant0;
grant1;
grant2;
grant3;
grant4;
}
ASSUMPTIONS {
G F idle;
G (!(idle && X !grant0 && X !grant1 && X !grant2 && X !grant3 && X !grant4) || X idle);
G (X !grant0 || X ((!request0 && !idle) U (!request0 && i
... [truncated 383 Bytes]
| X !grant4;
X !grant3 || X !grant4;
X !grant0 || request0;
X !grant1 || request1;
X !grant2 || request2;
X !grant3 || request3;
X !grant4 || request4;
(X !grant0 && X !grant1 && X !grant2 && X !grant3 && X !grant4) || idle;
}
GUARANTEES {
! F G (request0 && X !grant0);
! F G (request1 && X !grant1);
! F G (request2 && X !grant2);
! F G (request3 && X !grant3);
! F G (request4 && X !grant4);
}
}
//#!SYNTCOMP
//STATUS : realizable
//REF_SIZE : 127
//#.