Try encoding a Petri net and a history as a CQL instance

[wisnesky]

For each example, write the corresponding instance on the 4 table AQL schema below. Then, give the example to Ryan who will compute the grothendieck construction. Then, pick a few execution histories, and write each history as an instance on the grothendieck construction schema.

schema S = literal : empty {
    entities
        Input Output Place Trans
    foreign_keys
        f1 : Input -> Trans
        f2 : Input -> Place
        g1 : Output -> Place
        g2 : Output -> Trans  
}

//Petri net goes here
instance I = literal : S {
    generators 
        //todo
    equations 
        //todo
} 

schema IntI = elements I

instance history = literal : IntI {
    ... 
}

[epost]

Also see the pivot feature in Java AQL:

• https://github.com/CategoricalData/fql/blob/master/src/main/java/catdata/aql/AqlPivot.java
• https://github.com/CategoricalData/fql/commit/efaea9217ea4ef40f0d6e82d41eb14c250b47b5e
• https://github.com/CategoricalData/fql/commit/a58d1cd13b59b422f37d69a20b91657b961eb891

[FabrizioRomanoGenovese]

Just to see if I get it. Imagine a net with only one place and one transition. Place is transition's input and output. Is this correct?

schema S = literal : empty {
    entities
        Input Output Place Trans
    foreign_keys
        f1 : Input -> Trans
        f2 : Input -> Place
        g1 : Output -> Place
        g2 : Output -> Trans  
}

//Petri net goes here
instance I = literal : S {
    generators 
        i:Input, o:Output, p:Place, t:Transition
    equations 
        f1(i) = t, 
        f2(i) = p,
        g1(o) = t, 
        g2(o) = p
} 

schema IntI = elements I

instance history = literal : IntI {
    ... 
}

I just want to make sure I understand how to use this stuff. If I got it correctly each time a place is connected to a transition as its input (output) then a witness of type Input (resp Output) has to be provided, and suitably mapped by the edge functions. Is this correct?

[wisnesky]

I’m pretty sure this is correct, the example is ‘unitary’ net. One way to build an instance is as you suggest, specifying an explicit witness for all the ‘connections’, and that’s what you’d do to build such a DB in say SQL. Another way is to say the instance is the initial algebra of the equations, so that you don’t have to explicitly witness everything, you can just present the instance.

On Oct 26, 2018, at 10:44 AM, Fabrizio Romano Genovese notifications@github.com wrote:

Just to see if I get it. Imagine a net with only one place and one transition. Place is transition's input and output. Is this correct?

schema S = literal : empty { entities Input Output Place Trans foreign_keys f1 : Input -> Trans f2 : Input -> Place g1 : Output -> Place g2 : Output -> Trans
}

//Petri net goes here instance I = literal : S { generators i:Input, o:Output, p:Place, t:Transition equations f1(i) = t, f2(i) = p, g1(o) = t, g2(o) = p }

schema IntI = elements I

instance history = literal : IntI { ... }

I just want to make sure I understand how to use this stuff. If I got it correctly each time a place is connected to a transition as its input (output) then a witness of type Input (resp Output) has to be provided, and suitably mapped by the edge functions. Is this correct?

— You are receiving this because you were assigned. Reply to this email directly, view it on GitHub, or mute the thread.

[FabrizioRomanoGenovese]

@wisnesky, this is interesting. I think I get this from the categorical point of view, but could you provide an example of how to do it in practice? For instance, take the simple net I sketched above. How would you present the same net as an initial algebra?

[wisnesky]

Here's the same net (Net instance) given as a presentation of an initial algebra:

instance N = literal : Net {
    generators
        i : Input
        o : Output
    equations
        i.f1 = o.g1
        i.f2 = o.g2 
}

The difference is that the places and transitions are now implicitly defined (e.g., referred to as i.f1 rather than p).

Presenting an instance rather than giving it explicitly does require automated theorem proving, which impacts scalability.

[wisnesky]

Example:

schema Net = literal : empty {
        entities
            Input Place Trans Output
        foreign_keys
            inFrom : Input -> Place
            inTo  : Input -> Trans
            outTo  : Output -> Place
            outFrom  : 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.inFrom = p1
                i1.inTo  = t1
                o1.outFrom  = t1
                o1.outTo  = p2

                i2.inFrom = p2
                i2.inTo  = t2
                o2.outFrom  = t2
                o2.outTo  = p3
        options
                interpret_as_algebra = true     
}

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

mapping proj = pivot N // intN -> Net

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

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

constraints properFiring = literal : intN {
//for each input i and output o we need a constraint, in this case 4 total.
        forall fire: t1  
    ->
    exists input: i1 where inTo(input)=fire

        forall fire: t2  
    ->
    exists input: i2 where inTo(input)=fire

        forall fire: t1  
    ->
    exists input: o1 where outFrom(input)=fire

        forall fire: t2
    ->
    exists input: o2 where outFrom(input)=fire
}

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

//this is a bad instance on intN: it fails the proper firing test
instance IBad = literal : intN {
        generators
                token1time1 : p1
                token1time2 : p2
                token1time3 : p3
                fire12 : t1
                fire23 : t2     

        equations

        options
                interpret_as_algebra = true     
}

//command validateIBad = check properFiring IBad

//this is a good instance on intN: it passes both proper firing and injectivity
instance IGood = literal : intN {
        generators
                token1time1 : p1
                token1time2 : p2
                token1time3 : p3
                fire12 : t1
                fire23 : t2     
        input1 : i1
        input2 : i2
        output1: o1
        output2: o2
        equations
        inFrom(input1)   = token1time1  inTo(input1)   = fire12
        outFrom(output1) = fire12       outTo(output1) = token1time2
        inFrom(input2)   = token1time2  inTo(input2)   = fire23 
        outFrom(output2) = fire23       outTo(output2) = token1time3
        options
                interpret_as_algebra = true     
}
//the above could also be done with many fewer lines, if we drop the option.

command validateIGood = check properFiring IGood

instance J = sigma proj IGood

command validate2 = check injectivity J