example Petri

options  
	diverge_warn = false

schema Net = literal : empty {
	entities
		Input Place Trans Output
	foreign_keys
		place : Input -> Place
	    trans : Input -> Trans
	    place : Output -> Place
	    trans : Output -> Trans
} 

/*
 * p1 ->t1-> p2 ->t2-> p3
 */
instance N = literal : Net {
	generators
		p1 p2 p3 : Place
		t1 t2 : Trans
		i1 i2 : Input
		o1 o2 : Output
	equations
		i1.place = p1
		i1.trans = t1
		o1.trans = t1
		o1.place = p2

		i2.place = p2
		i2.trans = t2
		o2.trans = t2
		o2.place = p3
		
	options
		interpret_as_algebra = true	
}

/*
 entities
	i1 i2 o1 o2 p1 p2 p3 t1 t2
foreign_keys
	trans : o2 -> t2
	place : o2 -> p3
	place : o1 -> p2
	trans : o1 -> t1
	trans : i2 -> t2
	place : i2 -> p2
	place : i1 -> p1
	trans : i1 -> t1
*/	
schema intN = pivot N 

mapping proj = pivot N // intN -> Net

constraints injectivity = literal : Net {
	forall x y : Input
	where x.place = y.place -> where x = y

	forall x y : Output
	where x.trans = y.trans -> where x = y
}

///////////////////////////////////////////////////////////////
//example: 

//this is an instance on intN and passes the injectivity check
instance I = literal : intN {
	generators
		token1time1 : p1
		token1time2 : p2
		token1time3 : p3
		fire12 : t1
		fire23 : t2	

	equations

	options
		interpret_as_algebra = true	
}

instance J = sigma proj I // have J = N

command validate1 = check injectivity J
Keywords:

constraints_literal
sigma
pivot
check
pivot
instance_literal
schema_literal

Options:

interpret_as_algebra



instance N

Input
IDplacetrans
047
158
Output
IDplacetrans
257
368
Place
ID
4
5
6
Trans
ID
7
8


instance J

Input
IDplacetrans
Output
IDplacetrans
Place
ID
0
1
2
Trans
ID
3
4


instance I

i1
IDplacetrans
i2
IDplacetrans
o1
IDplacetrans
o2
IDplacetrans
p1
ID
0
p2
ID
1
p3
ID
2
t1
ID
3
t2
ID
4


command validate1

Satisfies