master
Daan Vanoverloop 4 months ago
parent d11378bf2c
commit 140a5211a8
  1. BIN
      Computergrafiek Project/2022-03-02_08-28-34_sheet.rnote
  2. 2
      Computergrafiek Project/graphics_project_21-22-Danacus
  3. BIN
      Computergrafiek Project/sessie2(2).pdf
  4. BIN
      Digitale elektronica en processoren/2022-02-25_12-12-04_sheet.rnote
  5. BIN
      Gvdi/les2
  6. BIN
      Gvdi/les2.rnote
  7. BIN
      Internet Infrastructure/ii-crypto.pdf
  8. BIN
      Internet Infrastructure/ii-crypto.rnote
  9. BIN
      Internet Infrastructure/ii-dns.rnote
  10. 1
      MAS/PacketWorld
  11. BIN
      Modellering van complexe systemen/2022-02-18_15-17-40_sheet.rnote
  12. BIN
      Modellering van complexe systemen/chapter4.pdf
  13. 21
      Modellering van complexe systemen/idp/Schur/schur.idp
  14. 5
      Modellering van complexe systemen/idp/Scienceweek/hanoi/hanoi.idp
  15. 11
      Modellering van complexe systemen/idp/Scienceweek/nqueens/nqueens.idp
  16. 21
      Modellering van complexe systemen/idp/Scienceweek/roster/roster.idp
  17. 7
      Modellering van complexe systemen/idp/Scienceweek/sudoku/sudoku.idp
  18. BIN
      Swarch/2022-03-03_10-32-59_sheet.rnote
  19. BIN
      Swarch/2022-03-03_10-53-04_sheet.rnote
  20. BIN
      Swarch/2022-03-03_11-35-37_sheet.rnote
  21. BIN
      Swarch/SA2022-Lecture03-01_Intro.pdf
  22. BIN
      Swarch/SA2022-Lecture03-02_SystemContext(1).pdf
  23. BIN
      Swarch/SA2022-Lecture03-03_Architecture-Defined.pdf

@ -1 +1 @@
Subproject commit be68a16d8e0763b22aa4b258ae7dfb37624f9ba5
Subproject commit 7f64b1ede2c00fe3e314166b8f57cd2c4e5b9ab4

Binary file not shown.

Binary file not shown.

@ -0,0 +1 @@
Subproject commit 7d8b5d383460d83e0cc5ca300599c372ed7329f2

@ -0,0 +1,21 @@
/*************
Schur
*************/
vocabulary V {
type number isa int
type partition isa int
maxNumber : number
inPartition(number, partition)
}
theory T:V {
!n [number]: n < maxNumber.
}
structure S:V {
maxNumber = 70
}

@ -56,13 +56,16 @@ vocabulary V {
theory T : V {
// At the end, all discs are on the right
!d [disc]: onPosition(end, d, right).
// A disc can only be moved when no discs are on the disc.
!t [Time]: !d [disc]: moveDisc(t) = d => ((?o [disc]: onTopOf(t, o, d)) => ~?p: moveTo(t) = p).
// There can never be a larger disc on top of a smaller one.
!t [Time]: ~(?d1 [disc]: ?d2 [disc]: d1 > d2 & onTopOf(t, d1, d2)).
// Express how the position of disc changes over time.
{ onPosition(0,disc,left).

@ -13,12 +13,17 @@ theory T : V {
{ diag2(x, y) = x + y - 1. }
// There is exactly one queen in every row
!r [index]: ?1c [index]: queen(r, c).
// There is exactly one queen in every column
!c [index]: ?1r [index]: queen(r, c).
// There can not be more than one queen on any diagonal (2 constraints)
!r1 [index]: !c1 [index]: !r2 [index]: !c2 [index]:
queen(r1, c1) & queen(r2, c2) & (r1 ~= r2 | c1 ~= c2)
=> diag1(r1, c1) ~= diag1(r2, c2) & diag2(r1, c1) ~= diag2(r2, c2).
//!d [diag]: ?=<1r [index]: ?=<1c [index]: diag1(r, c) = d & queen(r, c).
//!d [diag]: ?=<1r [index]: ?=<1c [index]: diag2(r, c) = d & queen(r, c).
}

@ -34,22 +34,31 @@ vocabulary V{
theory T:V{
// A course must be taught the correct number of hours per week.
//TODO
!c [course]: !g [group]: card { d [day], h [hour] : has(c, g, d, h) } = hoursPerWeek(g, c).
// A teacher can only teach one class at any time.
//TODO
!t [teacher]: !d [day]: !h [hour]: !g1, g2 [group]:
mustTeach(t, g1, d, h) & mustTeach(t, g2, d, h)
=> g1 = g2.
// A teacher must have the right degree to teach a course.
//TODO
!t [teacher]: !c [course]: !g [group]: taughtBy(g, c) = t => degree(t, c).
// No courses wednesday afternoon
//TODO
!c [course]: !g [group]: !h [hour]: h > 4 => ~has(c, g, wednesday, h).
// A classgroup can only follow one class at any time.
//TODO
!g [group]: !d [day]: !h [hour]: !c1, c2 [course]: has(c1, g, d, h) & has(c2, g, d, h) => c1 = c2.
// If a classgroup has a course at a certain time, that course's teacher must teach that group at that time.
//TODO
/*
!c [course]: !g [group]: !d [day]: !h [hour]: !t [teacher]:
has(c, g, d, h) & taughtBy(g, c) = t
=> mustTeach(t, g, d, h).
*/
{
mustTeach(t, g, d, h) <- has(c, g, d, h) & taughtBy(g, c) = t.
}
}
include "idpd3/run.idp"

@ -22,13 +22,16 @@ vocabulary V {
theory T : V {
//On every row every number is present.
!r [row]: !c1 [column]: !c2 [column]: c1 ~= c2 => solution(r, c1) ~= solution(r, c2).
//In every column every number is present.
!c [column]: !r1 [row]: !r2 [row]: r1 ~= r2 => solution(r1, c) ~= solution(r2, c).
//In every block every number is present.
!b [block]: !r1 [row]: !r2 [row]: !c1 [column]: !c2 [column]:
liesInBlock(r1, c1, b) & liesInBlock(r2, c2, b) & (r1 ~= r2 | c1 ~= c2)
=> solution(r1, c1) ~= solution(r2, c2).
//Define which cells lie in which block
{

Loading…
Cancel
Save