Function TestTemporalValidation

analysis/temporal_validation_test.go:11–104

(t *testing.T)

)

func TestTemporalValidation(t *testing.T) {
	tests := []struct {
		name    string
		program string
		wantErr bool
		err     string
	}{
		{
			name: "valid temporal predicate",
			program: `
				Decl p(X) temporal bound [/any].
				p(1) @[2020-01-01, 2021-01-01].
			`,
			wantErr: false,
		},
		{
			name: "valid synthetic temporal predicate",
			program: `
				p(1) @[2020-01-01, 2021-01-01].
				p(2) @[2021-01-01, 2022-01-01].
			`,
			wantErr: false,
		},
		{
			name: "invalid non-temporal predicate with annotation",
			program: `
				Decl p(X) bound [/any].
				p(1) @[2020-01-01, 2021-01-01].
			`,
			wantErr: true,
			err:     "predicate p(A0) is not declared temporal",
		},
		{
			name: "invalid eternal fact for temporal predicate",
			program: `
				Decl p(X) temporal bound [/any].
				p(1).
			`,
			wantErr: true,
			err:     "defined without temporal annotation",
		},
		{
			name: "valid annotated fact for temporal predicate",
			program: `
				Decl p(X) temporal bound [/any].
				p(1) @[2020-01-01, 2021-01-01].
			`,
			wantErr: false,
		},
		{
			name: "mixed usage synthetic (invalid)",
			program: `
				p(1) @[2020-01-01, 2021-01-01].
				p(2).
			`,
			wantErr: true,
			err:     "defined without temporal annotation",
		},