Browse Source

Changes were made

main
Sam Hatfield 3 months ago
parent
commit
cb5eb543cf
  1. 4
      database.als
  2. 38
      storage.als

4
database.als

@ -2,7 +2,7 @@ module tiltsys/database
open tiltsys/storage as S
open tiltsys/evaluator as E
some sig Database {
sig Database {
storage: one S/Storage,
evaluator: one E/Evaluator
} {
@ -12,4 +12,4 @@ some sig Database {
}
pred show [] {}
run show for 3
run show for 3 but 5 S/Node, exactly 1 Database

38
storage.als

@ -1,40 +1,14 @@
module tiltsys/storage
sig Storage {
graphs: set Graph
nodes: set Node,
to: Node -> Node
} {
// Capture instances
Graph in graphs
}
some sig Graph {
// tops are the opposite of Bottom: they serve as starting points for traversal
tops: some Datum,
to: Node -> Node,
types: set Type
} {
// Capture instances
Node in tops + tops.^to
Type in types
// Bottom only gets pointed at
all n: Node | Bottom -> n not in to
// All paths lead to Bottom
all d: Datum | Bottom in d.^to
// Nodes cannot point to themselves
no to & iden
}
abstract sig Node, Type {}
// Bottom signals the end of traversal
one sig Bottom extends Node {}
Node in nodes
sig Datum extends Node {
value: Type
// Acyclic
no ^to & iden
}
pred show [] {}
run show for 4
sig Node {}
Loading…
Cancel
Save