456 lines
12 KiB
Go
456 lines
12 KiB
Go
package recursion_test
|
|
|
|
/* ---------------------------------------------------------------- *
|
|
* UNIT TESTING
|
|
* ---------------------------------------------------------------- */
|
|
|
|
import (
|
|
"logik/aussagenlogik/formulae"
|
|
"logik/aussagenlogik/recursion"
|
|
"logik/aussagenlogik/schema"
|
|
"logik/core/utils"
|
|
"testing"
|
|
|
|
"github.com/stretchr/testify/assert"
|
|
)
|
|
|
|
/* ---------------------------------------------------------------- *
|
|
* TESTCASE eval(·, ·)
|
|
* ---------------------------------------------------------------- */
|
|
|
|
func TestEvalLiteral(test *testing.T) {
|
|
var assert = assert.New(test)
|
|
var val int
|
|
var fml formulae.Formula
|
|
var I []string
|
|
|
|
fml = schema.ParseExpr("A0")
|
|
I = []string{"A0"}
|
|
val = recursion.Eval(fml, I)
|
|
assert.Equal(1, val)
|
|
|
|
fml = schema.ParseExpr("A0")
|
|
I = []string{}
|
|
val = recursion.Eval(fml, I)
|
|
assert.Equal(0, val)
|
|
|
|
fml = schema.ParseExpr("! A0")
|
|
I = []string{"A0"}
|
|
val = recursion.Eval(fml, I)
|
|
assert.Equal(0, val)
|
|
|
|
fml = schema.ParseExpr("! A0")
|
|
I = []string{}
|
|
val = recursion.Eval(fml, I)
|
|
assert.Equal(1, val)
|
|
}
|
|
|
|
func TestEvalNegation(test *testing.T) {
|
|
var assert = assert.New(test)
|
|
var val int
|
|
var fml formulae.Formula
|
|
var I []string
|
|
|
|
fml = schema.ParseExpr("A4 || ! A4")
|
|
I = []string{}
|
|
val = recursion.Eval(fml, I)
|
|
assert.Equal(1, val)
|
|
|
|
fml = schema.ParseExpr("A4 && ! A4")
|
|
I = []string{}
|
|
val = recursion.Eval(fml, I)
|
|
assert.Equal(0, val)
|
|
}
|
|
|
|
func TestEvalConjunction(test *testing.T) {
|
|
var assert = assert.New(test)
|
|
var val int
|
|
var fml formulae.Formula
|
|
var I []string
|
|
|
|
fml = schema.ParseExpr("A0 && A1")
|
|
I = []string{"A0"}
|
|
val = recursion.Eval(fml, I)
|
|
assert.Equal(0, val)
|
|
|
|
fml = schema.ParseExpr("A0 && A1")
|
|
I = []string{"A0", "A1"}
|
|
val = recursion.Eval(fml, I)
|
|
assert.Equal(1, val)
|
|
}
|
|
|
|
func TestEvalDisjunction(test *testing.T) {
|
|
var assert = assert.New(test)
|
|
var val int
|
|
var fml formulae.Formula
|
|
var I []string
|
|
|
|
fml = schema.ParseExpr("A0 || A1")
|
|
I = []string{"A0"}
|
|
val = recursion.Eval(fml, I)
|
|
assert.Equal(1, val)
|
|
|
|
fml = schema.ParseExpr("A0 || A1")
|
|
I = []string{"A7"}
|
|
val = recursion.Eval(fml, I)
|
|
assert.Equal(0, val)
|
|
}
|
|
|
|
func TestEvalImplication(test *testing.T) {
|
|
var assert = assert.New(test)
|
|
var val int
|
|
var fml formulae.Formula
|
|
var I []string
|
|
|
|
fml = schema.ParseExpr("A0 -> A1")
|
|
I = []string{"A0"}
|
|
val = recursion.Eval(fml, I)
|
|
assert.Equal(0, val)
|
|
|
|
fml = schema.ParseExpr("A0 -> A1")
|
|
I = []string{"A0", "A1"}
|
|
val = recursion.Eval(fml, I)
|
|
assert.Equal(1, val)
|
|
|
|
fml = schema.ParseExpr("A0 -> A1")
|
|
I = []string{"A7"}
|
|
val = recursion.Eval(fml, I)
|
|
assert.Equal(1, val)
|
|
}
|
|
|
|
func TestEvalIff(test *testing.T) {
|
|
var assert = assert.New(test)
|
|
var val int
|
|
var fml formulae.Formula
|
|
var I []string
|
|
|
|
fml = schema.ParseExpr("A0 <-> A1")
|
|
I = []string{"A0"}
|
|
val = recursion.Eval(fml, I)
|
|
assert.Equal(0, val)
|
|
|
|
fml = schema.ParseExpr("A0 <-> A1")
|
|
I = []string{"A0", "A1"}
|
|
val = recursion.Eval(fml, I)
|
|
assert.Equal(1, val)
|
|
|
|
fml = schema.ParseExpr("A0 <-> A1")
|
|
I = []string{"A7"}
|
|
val = recursion.Eval(fml, I)
|
|
assert.Equal(1, val)
|
|
}
|
|
|
|
func TestEvalComplex(test *testing.T) {
|
|
var assert = assert.New(test)
|
|
var val int
|
|
var fml formulae.Formula
|
|
var I []string
|
|
fml = schema.ParseExpr("( ! A0 || (( A0 && A3 ) || A2 ))")
|
|
I = []string{"A0", "A2"}
|
|
val = recursion.Eval(fml, I)
|
|
assert.Equal(1, val)
|
|
|
|
I = []string{"A0", "A3"}
|
|
val = recursion.Eval(fml, I)
|
|
assert.Equal(1, val)
|
|
|
|
I = []string{"A0"}
|
|
val = recursion.Eval(fml, I)
|
|
assert.Equal(0, val)
|
|
|
|
I = []string{"A4", "A8"}
|
|
val = recursion.Eval(fml, I)
|
|
assert.Equal(1, val)
|
|
|
|
fml = schema.ParseExpr("( ! A0 || (( A0 && A3 ) || ! A2 ))")
|
|
I = []string{"A0", "A2"}
|
|
val = recursion.Eval(fml, I)
|
|
assert.Equal(0, val)
|
|
|
|
I = []string{"A0", "A3"}
|
|
val = recursion.Eval(fml, I)
|
|
assert.Equal(1, val)
|
|
}
|
|
|
|
/* ---------------------------------------------------------------- *
|
|
* TESTCASE Atoms(·)
|
|
* ---------------------------------------------------------------- */
|
|
|
|
func TestAtomsNoduplicates(test *testing.T) {
|
|
test.Skip("Methode noch nicht implementiert")
|
|
var assert = assert.New(test)
|
|
var fml formulae.Formula
|
|
var val []string
|
|
fml = schema.ParseExpr("( A4 && ( A4 || A4 ))")
|
|
val = recursion.Atoms(fml)
|
|
var n int = len(utils.FilterStrings(&val, func(x string) bool { return x == "A4" }))
|
|
assert.Equal(1, n, "Atome dürfen nicht mehrfach vorkommen!")
|
|
}
|
|
|
|
func TestAtomsNoNonAtoms(test *testing.T) {
|
|
test.Skip("Methode noch nicht implementiert")
|
|
var assert = assert.New(test)
|
|
var fml formulae.Formula
|
|
var val []string
|
|
fml = schema.ParseExpr("( {F} || A3 )")
|
|
val = recursion.Atoms(fml)
|
|
utils.SortStrings(&val)
|
|
assert.NotContains(val, "F", "Nichtatomare Formeln dürfen nicht vorkommen!")
|
|
}
|
|
|
|
func TestAtomsCalc1(test *testing.T) {
|
|
test.Skip("Methode noch nicht implementiert")
|
|
var assert = assert.New(test)
|
|
var fml formulae.Formula
|
|
var val []string
|
|
fml = schema.ParseExpr("A0")
|
|
val = recursion.Atoms(fml)
|
|
assert.ElementsMatch([]string{"A0"}, val)
|
|
}
|
|
|
|
func TestAtomsCalc2(test *testing.T) {
|
|
test.Skip("Methode noch nicht implementiert")
|
|
var assert = assert.New(test)
|
|
var fml formulae.Formula
|
|
var val []string
|
|
fml = schema.ParseExpr("((( ! A8 && A3 ) || A4 ) && A0 )")
|
|
val = recursion.Atoms(fml)
|
|
assert.ElementsMatch([]string{"A0", "A3", "A4", "A8"}, val)
|
|
}
|
|
|
|
/* ---------------------------------------------------------------- *
|
|
* TESTCASE depth(·, ·)
|
|
* ---------------------------------------------------------------- */
|
|
|
|
func TestDepthCalc1(test *testing.T) {
|
|
test.Skip("Methode noch nicht implementiert")
|
|
var assert = assert.New(test)
|
|
var val int
|
|
var fml formulae.Formula
|
|
fml = schema.ParseExpr("A0")
|
|
val = recursion.FmlDepth(fml)
|
|
assert.Equal(0, val)
|
|
}
|
|
|
|
func TestDepthCalc2(test *testing.T) {
|
|
test.Skip("Methode noch nicht implementiert")
|
|
var assert = assert.New(test)
|
|
var val int
|
|
var fml formulae.Formula
|
|
fml = schema.ParseExpr("!! A8")
|
|
val = recursion.FmlDepth(fml)
|
|
assert.Equal(2, val)
|
|
}
|
|
|
|
func TestDepthCalc3(test *testing.T) {
|
|
test.Skip("Methode noch nicht implementiert")
|
|
var assert = assert.New(test)
|
|
var val int
|
|
var fml formulae.Formula
|
|
fml = schema.ParseExpr("( ! A0 && A3 )")
|
|
val = recursion.FmlDepth(fml)
|
|
assert.Equal(2, val)
|
|
}
|
|
|
|
func TestDepthCalc4(test *testing.T) {
|
|
test.Skip("Methode noch nicht implementiert")
|
|
var assert = assert.New(test)
|
|
var val int
|
|
var fml formulae.Formula
|
|
fml = schema.ParseExpr("((( ! A0 && A3 ) || A4 ) && A8 )")
|
|
val = recursion.FmlDepth(fml)
|
|
assert.Equal(4, val)
|
|
}
|
|
|
|
func TestDepthCalc5(test *testing.T) {
|
|
test.Skip("Methode noch nicht implementiert")
|
|
var assert = assert.New(test)
|
|
var val int
|
|
var fml formulae.Formula
|
|
fml = schema.ParseExpr("! ((( ! A0 && A3 ) || A4 ) && A8 )")
|
|
val = recursion.FmlDepth(fml)
|
|
assert.Equal(5, val)
|
|
}
|
|
|
|
/* ---------------------------------------------------------------- *
|
|
* TESTCASE length(·)
|
|
* ---------------------------------------------------------------- */
|
|
|
|
func TestLengthCalc1(test *testing.T) {
|
|
test.Skip("Methode noch nicht implementiert")
|
|
var assert = assert.New(test)
|
|
var val int
|
|
var fml formulae.Formula
|
|
fml = schema.ParseExpr("A0")
|
|
val = recursion.FmlLength(fml)
|
|
assert.Equal(1, val)
|
|
}
|
|
|
|
func TestLengthCalc2(test *testing.T) {
|
|
test.Skip("Methode noch nicht implementiert")
|
|
var assert = assert.New(test)
|
|
var val int
|
|
var fml formulae.Formula
|
|
fml = schema.ParseExpr("!! A8")
|
|
val = recursion.FmlLength(fml)
|
|
assert.Equal(3, val)
|
|
}
|
|
|
|
func TestLengthCalc3(test *testing.T) {
|
|
test.Skip("Methode noch nicht implementiert")
|
|
var assert = assert.New(test)
|
|
var val int
|
|
var fml formulae.Formula
|
|
fml = schema.ParseExpr("( ! A0 && A3 )")
|
|
val = recursion.FmlLength(fml)
|
|
assert.Equal(4, val)
|
|
}
|
|
|
|
func TestLengthCalc4(test *testing.T) {
|
|
test.Skip("Methode noch nicht implementiert")
|
|
var assert = assert.New(test)
|
|
var val int
|
|
var fml formulae.Formula
|
|
fml = schema.ParseExpr("((( ! A0 && A3 ) || A4 ) && A8 )")
|
|
val = recursion.FmlLength(fml)
|
|
assert.Equal(8, val)
|
|
}
|
|
|
|
func TestLengthCalc5(test *testing.T) {
|
|
test.Skip("Methode noch nicht implementiert")
|
|
var assert = assert.New(test)
|
|
var val int
|
|
var fml formulae.Formula
|
|
fml = schema.ParseExpr("! ((( ! A0 && A3 ) || A4 ) && A8 )")
|
|
val = recursion.FmlLength(fml)
|
|
assert.Equal(9, val)
|
|
}
|
|
|
|
/* ---------------------------------------------------------------- *
|
|
* TESTCASE #Parentheses(·)
|
|
* ---------------------------------------------------------------- */
|
|
|
|
func TestParenthesesCalc1(test *testing.T) {
|
|
test.Skip("Methode noch nicht implementiert")
|
|
var assert = assert.New(test)
|
|
var val int
|
|
var fml formulae.Formula
|
|
fml = schema.ParseExpr("A0")
|
|
val = recursion.NrParentheses(fml)
|
|
assert.Equal(0, val)
|
|
}
|
|
|
|
func TestParenthesesCalc2(test *testing.T) {
|
|
test.Skip("Methode noch nicht implementiert")
|
|
var assert = assert.New(test)
|
|
var val int
|
|
var fml formulae.Formula
|
|
fml = schema.ParseExpr("!! A8")
|
|
val = recursion.NrParentheses(fml)
|
|
assert.Equal(0, val)
|
|
}
|
|
|
|
func TestParenthesesCalc3(test *testing.T) {
|
|
test.Skip("Methode noch nicht implementiert")
|
|
var assert = assert.New(test)
|
|
var val int
|
|
var fml formulae.Formula
|
|
fml = schema.ParseExpr("( ! A0 && A3 )")
|
|
val = recursion.NrParentheses(fml)
|
|
assert.Equal(2, val)
|
|
}
|
|
|
|
func TestParenthesesCalc4(test *testing.T) {
|
|
test.Skip("Methode noch nicht implementiert")
|
|
var assert = assert.New(test)
|
|
var val int
|
|
var fml formulae.Formula
|
|
fml = schema.ParseExpr("((( ! A0 && A3 ) || A4 ) && A8 )")
|
|
val = recursion.NrParentheses(fml)
|
|
assert.Equal(6, val)
|
|
}
|
|
|
|
func TestParenthesesCalc5(test *testing.T) {
|
|
test.Skip("Methode noch nicht implementiert")
|
|
var assert = assert.New(test)
|
|
var val int
|
|
var fml formulae.Formula
|
|
fml = schema.ParseExpr("! ((( ! A0 && A3 ) || A4 ) && A8 )")
|
|
val = recursion.NrParentheses(fml)
|
|
assert.Equal(6, val)
|
|
}
|
|
|
|
/* ---------------------------------------------------------------- *
|
|
* TESTCASE NNF
|
|
* ---------------------------------------------------------------- */
|
|
|
|
func TestNNFatoms(test *testing.T) {
|
|
var assert = assert.New(test)
|
|
var fml formulae.Formula
|
|
var nnf_expected formulae.Formula
|
|
|
|
nnf_expected = formulae.Atom("A7")
|
|
fml = schema.ParseExpr("A7")
|
|
assert.Equal(nnf_expected.GetExpr(), recursion.NNF(fml).GetExpr())
|
|
|
|
fml = schema.ParseExpr("!! A7")
|
|
assert.Equal(nnf_expected.GetExpr(), recursion.NNF(fml).GetExpr())
|
|
|
|
nnf_expected = formulae.NegatedAtom("A7")
|
|
fml = schema.ParseExpr("! A7")
|
|
assert.Equal(nnf_expected.GetExpr(), recursion.NNF(fml).GetExpr())
|
|
|
|
fml = schema.ParseExpr("!!! A7")
|
|
assert.Equal(nnf_expected.GetExpr(), recursion.NNF(fml).GetExpr())
|
|
}
|
|
|
|
func TestNNFconj(test *testing.T) {
|
|
var assert = assert.New(test)
|
|
var fml formulae.Formula
|
|
var nnf_expected formulae.Formula
|
|
|
|
nnf_expected = formulae.Disjunction2(formulae.NegatedAtom("A0"), formulae.NegatedAtom("A1"))
|
|
fml = schema.ParseExpr("! (A0 && A1)")
|
|
assert.Equal(nnf_expected.GetExpr(), recursion.NNF(fml).GetExpr())
|
|
|
|
nnf_expected = formulae.Disjunction2(formulae.Atom("A0"), formulae.Atom("A1"))
|
|
fml = schema.ParseExpr("! (! A0 && ! A1)")
|
|
assert.Equal(nnf_expected.GetExpr(), recursion.NNF(fml).GetExpr())
|
|
|
|
nnf_expected = formulae.Conjunction2(formulae.Atom("A0"), formulae.NegatedAtom("A1"))
|
|
fml = schema.ParseExpr("(A0 && ! A1)")
|
|
assert.Equal(nnf_expected.GetExpr(), recursion.NNF(fml).GetExpr())
|
|
}
|
|
|
|
func TestNNFdisj(test *testing.T) {
|
|
var assert = assert.New(test)
|
|
var fml formulae.Formula
|
|
var nnf_expected formulae.Formula
|
|
|
|
nnf_expected = formulae.Conjunction2(formulae.NegatedAtom("A0"), formulae.NegatedAtom("A1"))
|
|
fml = schema.ParseExpr("! (A0 || A1)")
|
|
assert.Equal(nnf_expected.GetExpr(), recursion.NNF(fml).GetExpr())
|
|
|
|
nnf_expected = formulae.Conjunction2(formulae.Atom("A0"), formulae.Atom("A1"))
|
|
fml = schema.ParseExpr("! (! A0 || ! A1)")
|
|
assert.Equal(nnf_expected.GetExpr(), recursion.NNF(fml).GetExpr())
|
|
|
|
nnf_expected = formulae.Disjunction2(formulae.Atom("A0"), formulae.NegatedAtom("A1"))
|
|
fml = schema.ParseExpr("(A0 || ! A1)")
|
|
assert.Equal(nnf_expected.GetExpr(), recursion.NNF(fml).GetExpr())
|
|
}
|
|
|
|
func TestNNFcalcComplex(test *testing.T) {
|
|
var assert = assert.New(test)
|
|
var fml formulae.Formula
|
|
var nnf_expected formulae.Formula
|
|
|
|
fml = schema.ParseExpr("! (! (!A0 || A1) || ! ! A8)")
|
|
nnf_expected = schema.ParseExpr("((!A0 || A1) && ! A8)")
|
|
assert.Equal(nnf_expected.GetExpr(), recursion.NNF(fml).GetExpr())
|
|
|
|
fml = schema.ParseExpr("! (! (!A0 || !(A1 && ! A7)) && ! A8)")
|
|
nnf_expected = schema.ParseExpr("((!A0 || (! A1 || A7)) || A8)")
|
|
assert.Equal(nnf_expected.GetExpr(), recursion.NNF(fml).GetExpr())
|
|
}
|