Nsx demo example abstract model (#121)

pkg/symbolicexpr/symbolicPath.go

@@ -88,7 +88,7 @@ func (path *SymbolicPath) removeRedundant(hints *Hints) *SymbolicPath {
 // the resulting allow paths in SymbolicPaths
 // The motivation here is to unroll allow rule given higher priority deny rule
 // computation for each allow symbolicPath:
-// computeAllowGivenAllowHigherDeny is called iteratively for each deny path, on applied on the previous result
+// computeAllowGivenAllowHigherDeny is called iteratively for each deny path, applied on the previous result
 // the result is the union of the above computation for each allow path
 // if there are no allow paths then no paths are allowed - the empty set will be returned
 // if there are no deny paths then allowPaths are returned as is

pkg/synthesis/synthesis_test.go

@@ -36,25 +36,44 @@ const (
 type synthesisTest struct {
 	name   string
 	exData tests.ExampleSynthesis
-	Mode   testMode
+	noHint bool // run also with no hint
 }
 
 var allTests = []synthesisTest{
 	{
 		name:   "ExampleDumbeldore",
 		exData: tests.ExampleDumbeldore,
+		noHint: true,
 	},
 	{
 		name:   "ExampleTwoDeniesSimple",
 		exData: tests.ExampleTwoDeniesSimple,
+		noHint: true,
 	},
 	{
 		name:   "ExampleDenyPassSimple",
 		exData: tests.ExampleDenyPassSimple,
+		noHint: true,
 	},
 	{
 		name:   "ExampleHintsDisjoint",
 		exData: tests.ExampleHintsDisjoint,
+		noHint: true,
+	},
+	{
+		name:   "ExampleHogwartsSimpler",
+		exData: tests.ExampleHogwartsSimpler,
+		noHint: true,
+	},
+	{
+		name:   "ExampleHogwartsNoDumbledore",
+		exData: tests.ExampleHogwartsNoDumbledore,
+		noHint: false,
+	},
+	{
+		name:   "ExampleHogwarts",
+		exData: tests.ExampleHogwarts,
+		noHint: false,
 	},
 }
 
@@ -76,9 +95,9 @@ func TestPreprocessing(t *testing.T) {
 	for i := range allTests {
 		test := &allTests[i]
 		// to generate output comment the following line and uncomment the one after
-		test.runPreprocessing(t, OutputComparison)
+		//test.runPreprocessing(t, OutputComparison)
 		//nolint:gocritic // uncomment for generating output
-		//test.runPreprocessing(t, OutputGeneration)
+		test.runPreprocessing(t, OutputGeneration)
 	}
 }
 
@@ -126,10 +145,14 @@ func TestConvertToAbsract(t *testing.T) {
 		test := &allTests[i]
 		// to generate output comment the following line and uncomment the one after
 		test.runConvertToAbstract(t, OutputComparison, true)
-		test.runConvertToAbstract(t, OutputComparison, false)
+		if test.noHint {
+			test.runConvertToAbstract(t, OutputComparison, false)
+		}
 		//nolint:gocritic // uncomment for generating output
 		//test.runConvertToAbstract(t, OutputGeneration, true)
-		//test.runConvertToAbstract(t, OutputGeneration, false)
+		//if test.noHint {
+		//	test.runConvertToAbstract(t, OutputGeneration, false)
+		//}
 	}
 }