Function TestTemporalAtomNormalization

analysis/temporal_validation_test.go:190–268

(t *testing.T)

}

func TestTemporalAtomNormalization(t *testing.T) {
	// Identify predicates.
	p := ast.PredicateSym{"p", 1}
	q := ast.PredicateSym{"q", 1}

	// Declare p and q as temporal.
	// We use a custom analyzer to bypass the parser and manually inject declarations and clauses.
	analyzer, err := New(nil, nil, ErrorForBoundsMismatch)
	if err != nil {
		t.Fatalf("New() error = %v", err)
	}
	analyzer.decl[p] = ast.Decl{
		DeclaredAtom: ast.Atom{p, []ast.BaseTerm{ast.Variable{"X"}}},
		Descr:        []ast.Atom{ast.NewAtom(ast.DescrTemporal)},
	}
	analyzer.decl[q] = ast.Decl{
		DeclaredAtom: ast.Atom{q, []ast.BaseTerm{ast.Variable{"X"}}},
		Descr:        []ast.Atom{ast.NewAtom(ast.DescrTemporal)},
	}

	// Helper to create *ast.Interval
	mkInterval := func(start, end string) *ast.Interval {
		i := ast.NewInterval(ast.NewVariableBound(ast.Variable{start}), ast.NewVariableBound(ast.Variable{end}))
		return &i
	}

	// Case 1: Valid TemporalAtom (should be normalized and pass)
	// p(X) :- q(X) @[S, E]
	validClause := ast.Clause{
		Head:     ast.Atom{p, []ast.BaseTerm{ast.Variable{"X"}}},
		HeadTime: mkInterval("S", "E"),
		Premises: []ast.Term{
			ast.TemporalAtom{
				Atom:     ast.Atom{q, []ast.BaseTerm{ast.Variable{"X"}}},
				Interval: mkInterval("S", "E"),
			},
		},
	}

	// Analyze the clause.
	_, err = analyzer.Analyze([]ast.Clause{validClause})
	if err != nil {
		t.Errorf("Analyze(validClause) unexpected error: %v", err)
	}

	// Verify normalization
	info, err := analyzer.Analyze([]ast.Clause{validClause})
	if err != nil {
		t.Errorf("Analyze(validClause) unexpected error: %v", err)
	}
	if len(info.Rules) != 1 {
		t.Fatalf("Expected 1 rule, got %d", len(info.Rules))
	}
	rule := info.Rules[0]
	if _, ok := rule.Premises[0].(ast.TemporalLiteral); !ok {
		t.Errorf("Premise was not normalized to TemporalLiteral: %T", rule.Premises[0])
	}