Modelling data pipelines with Alloy (with temporal logic). Model and customised theme file for Alloy 6

MDPWALWTL-theme.thm

<?xml version="1.0"?>
<alloy>

<view>

<defaultnode/>

<defaultedge/>

<node>
   <type name="Database"/>
   <type name="Int"/>
   <type name="Load"/>
   <type name="Process"/>
   <type name="Storage"/>
   <type name="String"/>
   <type name="Stutter"/>
   <type name="univ"/>
   <type name="ordering/Ord"/>
   <type name="seq/Int"/>
</node>

<node hideunconnected="yes">
   <type name="File"/>
   <type name="Table"/>
</node>

<node hideunconnected="yes" color="Red">
   <type name="Event"/>
</node>

<node visible="no">
   <type name="Datum"/>
</node>

<node visible="yes" hideunconnected="no" showlabel="no" showinattr="no">
   <set name="$stutter_happens" type="Event"/>
</node>

<edge style="inherit">
   <relation name="contents"> <type name="Storage"/> <type name="File"/> </relation>
   <relation name="tables"> <type name="Database"/> <type name="Table"/> </relation>
</edge>

<edge style="inherit" visible="no" attribute="yes">
   <relation name="data"> <type name="Table"/> <type name="Datum"/> </relation>
</edge>

<edge visible="no" attribute="yes">
   <relation name="data"> <type name="File"/> <type name="Datum"/> </relation>
</edge>

</view>

</alloy>

MDPWALWTL.als

// A version of _Modelling data pipelines with Alloy_ with temporal logic

// This time pipelines will be predicates that use/modify an external state store

sig Datum {}

sig File {
	data: set Datum
}

fact always_data {
	all f: File | #f.data > 2
}

one sig Storage {
	var contents: set File
}

sig Table {
	var data: set Datum
}

one sig Database {
	var tables: set Table
}

enum Event { Stutter, Process, Load }

pred Process[output: File] {
	historically Storage -> output not in contents and
	contents' = contents + Storage -> output and
	tables' = tables and
	Table.data' = Table.data
}

fun process_happens : Event -> File -> Storage {
  { e: Process, f: File, st: Storage | Process[f] }
}

pred Load[input: File] {
	historically input.data not in Table.data and
	Storage -> input in contents and
	one t: Table |
		{
			t.data' = t.data + input.data and 
			tables' = tables + Database -> t
		} and
	contents' = contents
}

fun load_happens : Event -> File {
  { e: Load, f: File | Load[f] }
}

pred Stutter {
	tables' = tables and 
	contents' = contents and
	Table.data' = Table.data
}

fun stutter_happens : set Event {
  { e: Stutter | Stutter }
}

fact init {
	no contents and
	no tables and
	no Table.data and
	#File > 2
}

fact transitions {
	always (some f: File | Process[f] or 
			some f: File | Load[f] or 
			Stutter)
}

pred fairness {
	some f: File {
		(eventually always  Storage -> f in contents) implies 
		(always eventually Load[f])
	}
}

run { fairness implies 
		eventually (#tables > 0 and #Table.data > 0)
	} for 5