Notes

Computergrafiek Project/graphics_project_21-22-Danacus

@@ -1 +1 @@
-Subproject commit 2336352aac675c6081457227a22a4226c1e768da
+Subproject commit b16362d5ac9d252d09e4fb49ee8cc497c59d6f1d

MAS/PacketWorld

@@ -1 +1 @@
-Subproject commit fc4614f954530d3090d55fc6f33a131cb7616317
+Subproject commit 6584acab72f449c3f8ccd0f8772df9e5266bc830

MCS/idp/session2/database.idp

@@ -0,0 +1,68 @@
+/**
+ * A Database as a logical structure
+ */
+vocabulary Sigma {
+    /*
+     * The assignment uses untyped first order logic. This is why we use a type "object" representing all object in the domain.
+     * In real applications, we would make types like  person, instructor, student, course etc.
+     * It is a good idea to try this.
+     *
+     * constructed from already includes UNA and DCA!!!!!!
+     */
+    type domain constructed from { A, AA, AAA, Ann, B, Bill, C, CS148, CS230, CS238, D, F, Flo, Hec, Jack, Jill, M100, M200, May, Pat, Ray, Sam, Sue, Tom }
+
+    Instructor(domain, domain)
+    Prerequ(domain, domain)
+    Enrolled(domain, domain)
+    Grade(domain, domain, domain)
+    PassGrade(domain)
+}
+ 
+structure Database : Sigma {
+    Instructor = {
+        Ray(), CS230();
+        Hec(), CS230();
+        Sue(), M100();
+        Sue(), M200();
+        Pat(), CS238();
+    }
+    Prerequ = {
+        CS230(), CS238();
+        CS148(), CS230();
+        M100(), M200();
+    }
+    Enrolled = {
+        Jill(),  CS230();
+        Jack(),  CS230();
+        Sam(),  CS230();
+        Bill(),  CS230();
+        May(),  CS238();
+        Ann(),  CS238();
+        Tom(),  M100();
+        Ann(),  M100();
+        Jill(),  M200();
+        Sam(),  M200();
+        Flo(),  M200();
+    }
+    Grade = {
+        Sam(), CS148(), AAA();
+        Bill(), CS148(), D();
+        Jill(), CS148(), A();
+        Jack(), CS148(), C();
+        Flo(), CS230(), AA();
+        May(), CS230(), AA();
+        Bill(), CS230(), F();
+        Ann(), CS230(), C();
+        Jill(), M100(), B();
+        Sam(), M100(), AA();
+        Flo(), M100(), D();
+        Flo(), M100(), B()
+    }
+    PassGrade = {
+        AAA();
+        AA();
+        A();
+        B();
+        C();
+    }
+}

MCS/idp/session2/exercise2.idp

@@ -0,0 +1,40 @@
+include "database.idp"
+include "run_queries.idp"
+
+procedure main() {
+    queries = {O1Q1;O1Q2;O1Q3;O1Q4;O1Q5;O1Q6;O1Q7}
+    runTrueFalseQueries(queries)
+}
+
+/*
+ * TODO: complete the queries. Since these are true/false queries, nothing should be added in front of the colon
+ * (there are no variables)
+ * replace true or false by the relevant formula (the values as they are given are insignificatn)
+ */
+query O1Q1: Sigma {
+    { : ?x: Prerequ(x, CS238) }
+}
+
+query O1Q2: Sigma {
+    { : ?x: Grade(May, CS230, x) & PassGrade(x) }
+}
+
+query O1Q3: Sigma {
+    { : !x: Prerequ(x, M100) => Instructor(Ray, x) }
+}
+
+query O1Q4: Sigma {
+    { : !x: Enrolled(x, CS230) => ?g: Grade(x, CS230, g) & PassGrade(g)}
+}
+
+query O1Q5: Sigma {
+    { : /*?g: Grade(John, CS230, g)*/ false}
+}
+
+query O1Q6: Sigma {
+    { : ?s: !i: ?c: Enrolled(s, c) & Instructor(i, c)}
+}
+
+query O1Q7: Sigma {
+    { : ?s: ?1c: Enrolled(s, c) }
+}

MCS/idp/session2/exercise3.idp

@@ -0,0 +1,21 @@
+include "database.idp"
+include "run_queries.idp"
+ 
+procedure main() {
+    queries = {O2Q1;O2Q2;O2Q3}
+    displayQueryAnswers(queries)
+}
+
+// TODO: complete queries.
+
+query O2Q1: Sigma{
+    {s[domain] c[domain] : ?g: Grade(s, c, g) & PassGrade(g)}
+}
+
+query O2Q2: Sigma{
+    {s[domain] : ?1c: Enrolled(s, c)}
+}
+
+query O2Q3: Sigma{
+    {s[domain] : Enrolled(s, CS230) & !c: !g: Grade(s, c, g) => PassGrade(g)}
+}

MCS/idp/session2/exercise4.idp

@@ -0,0 +1,29 @@
+include "database.idp"
+include "run_queries.idp"
+
+procedure main() {
+    integrityConstraints = {IntegrityConstraint1,IntegrityConstraint2,IntegrityConstraint3,IntegrityConstraint4}
+
+    allIntegrityConstraints = merge(IntegrityConstraint1,IntegrityConstraint2)
+    allIntegrityConstraints = merge(allIntegrityConstraints,IntegrityConstraint3)
+    allIntegrityConstraints = merge(allIntegrityConstraints,IntegrityConstraint4)
+    // This way, you can combine all the integrityConstraints to One big theory representing integrity of the database.
+
+    testIntegrityConstraints(integrityConstraints)
+}
+
+// TODO: add integrity constraints
+
+theory IntegrityConstraint1 : Sigma {
+    false.
+}
+
+theory IntegrityConstraint2 : Sigma {
+    false.
+}
+theory IntegrityConstraint3 : Sigma {
+    false.
+}
+theory IntegrityConstraint4 : Sigma {
+    false.
+}

MCS/idp/session2/run_queries.idp

@@ -0,0 +1,35 @@
+include <table_utils>
+
+procedure runTrueFalseQueries(queries) {
+    for index = 1, #queries do
+        result = query(queries[index], Database)
+        print("Query "..index.." evaluates to ", result)
+    end
+}
+
+procedure displayQueryAnswers(queries) {
+    for index = 1, #queries do
+        print("Running query "..index)
+        result = query(queries[index], Database)
+
+        print("Result is:")
+        print(result)
+    end
+}
+
+procedure testIntegrityConstraints(constraints) {
+    // We assume that database is two-valued. Hence: all we should check is: is database a model of every constraint.
+
+    for index = 1, #constraints do
+        print("Testing constraint "..index)
+        stdoptions.nbmodels = 1
+        result = (#modelexpand(constraints[index], Database) > 0)
+        // Alternatively to using the sat-inferences, we could use modelexpand and check if the result has at least one model
+        // (in our case: exactly one model)
+        if result then
+            print("Database satisfies constraint "..index)
+        else
+            print("Database does not satisfy constraint "..index)
+        end
+    end
+}