Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

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

Open
wisnesky opened this issue Oct 11, 2018 · 6 comments
Open

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

wisnesky opened this issue Oct 11, 2018 · 6 comments
Assignees
Labels
research Research, also into code-related subjects.

Comments

@wisnesky
Copy link
Contributor

wisnesky commented Oct 11, 2018

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
Copy link
Member

epost commented Oct 24, 2018

@FabrizioRomanoGenovese
Copy link

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
Copy link
Contributor Author

wisnesky commented Oct 29, 2018 via email

@FabrizioRomanoGenovese
Copy link

@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
Copy link
Contributor Author

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
Copy link
Contributor Author

wisnesky commented Nov 1, 2018

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

@epost epost added the research Research, also into code-related subjects. label Nov 2, 2018
@epost epost changed the title Try encoding a Petri net and a history as an AQL instance Try encoding a Petri net and a history as a CQL instance Aug 5, 2019
@wires wires assigned wires and unassigned wires Nov 5, 2021
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
research Research, also into code-related subjects.
Projects
None yet
Development

No branches or pull requests

4 participants