BNGSOS

From BioNetWiki

Revision as of 04:19, 24 October 2009; view current revision
←Older revision | Newer revision→
Jump to: navigation, search

Structured Operational Semantics (SOS) description of the BioNetGen language

Edmund M. Clarke, Sumit Kumar Jha and Chris Langmead,
Carnegie Mellon University

James Faeder
University of Pittsburgh

Contents

[edit]

Abstract Syntax for BioNetGen

  • container = New-Container (name, compartment, list-of-states, binding-state, tree-of-containers)
  • container-selector = New-Container-Selector ( name, compartment, list-of-states, binding-state, tree-of-containers )
  • container-match = container.Match ( container-selector )
  • container = container.getmatch(container-selector).selector-element
  • Add-Bond ( container1, container2 )
  • Delete-Bond (container1, container2 )
  • container.Change-State ( state-name, new-state )
  • container.clone()



.

[edit]

Semantics of BioNetGen

[edit]

container = New-Container (name, compartment, list-of-states, binding-state, tree-of-containers)

name:String, compartment: String, binding-state:Boolean

list-of-states = state1::state2::...::staten

state1: (String, String), .... , staten: (String,String)

tree: Tree of containers

[container = New-Container (name, compartment, state1::state2::...::staten, binding-state, tree), σ] --> [ {container : Container = < name, compartment, state1::state2::...::staten, binding-state, tree > }, σ ]



.

[edit]

container-selector = New-Container-Selector ( name, compartment, list-of-states, binding-state, tree-of-containers )

name: String \cup { * }

compartment: String \cup { * }

list-of-states: state1::state2::...::statem

binding-state: Boolean \cup { * }

tree: Tree of ( Containers \cup { * } )


[ container-selector = New-Container-Selector ( name, compartment, state1::state2::...::statem, binding-state, tree ) , σ ] = [ { container-selector: Container-Selector = < name, compartment, state1::state2::...::statem, binding-state, tree > } , σ ]



.

[edit]

container.Match ( container-selector)

container-selector: Container-Selector = < name, compartment, list-of-states, binding-state, tree, bond1::bond2::...::bondn >

container : Container = < name', compartment', list-of-states', binding-state', tree' >

tree-match = tree.match ( tree' )

name-match = name.match ( name' )

compartment-match = compartment.match ( compartment' )

list-of-states' = list-of-states :: Extra-state-list

bondi = ( componenti1, componenti2 )

Global-Bond-List := bond1::bond2::...::bondn::ExtraBondList

binding-state-match = binding-state. match ( binding-state' )

tree-match != NULL & name-match  != NULL & compartment-match  != NULL & state-match  != NULL & binding-state-match  != NULL

[ container.match( container-selector ) , σ ] --> [ { container-match : container-match = < tree-match, name-match, compartment-match, state-match, binding-state-match > } , σ ]



.


str: String

str': String

str = str'

[ str'.match (str) , σ ] = [ { string-match : string-match = < str, str' > } , σ ]




str: String

str': *

[ str'.match (str) , σ ] = [ { string-match : string-match = < str, * > } , σ ]




.


str: String

str': String

str != str'

[ str'.match (str) , σ ] = [ { string-match : string-match = NULL }, σ ]



.



tree  : Tree = < root, tree1 :: tree2 :: ... :: treen >

tree' : Tree = < root', [] >

root' = *

[ tree'.match (tree) , σ ] = [ { tree-match : tree-match = { <root,root'> } } , σ ]



.


tree  : Tree = < root, tree1 :: tree2 :: ... :: treen >

tree' : Tree = < root', tree'1 :: tree'2 :: ... :: tree'm >

root' = *

m <= n


( (match1 := tree'1.match(tree1)) != NULL) & ( (match2 := tree'2.match(tree2)) != NULL) .... & ( (matchm := tree'm.match(treem)) != NULL)

[ tree'.match (tree) , σ ] = [ { tree-match : tree-match = { <root,root'> } \cup \bigcup {match1, ....., matchm} > } } , σ ]


(The above assumes that there are rules available that allow reordering of lists)



.


tree  : Tree = < root, tree1 :: tree2 :: ... :: treen >

tree' : Tree = < root', tree'1 :: tree'2 :: ... :: tree'm >

root' = *

m <= n


\bigwedge_{\pi} \bigvee_{i} tree'π (i).match(treei) == NULL

[ tree'.match (tree) , σ ] = [ { tree-match : tree-match = NULL } , σ ]


tree  : Tree = < root, tree1 :: tree2 :: ... :: treen >

tree' : Tree = < root', tree'1 :: tree'2 :: ... :: tree'm >

root' != *

m > n

[ tree'.match (tree) , σ ] = [ { tree-match : tree-match = NULL } , σ ]


.


tree  : Tree = < root, tree1 :: tree2 :: ... :: treen >

tree' : Tree = < root', tree'1 :: tree'2 :: ... :: tree'm >

root' != *

n == m

root != root'

[ tree'.match (tree) , σ ] = [ { tree-match : tree-match = NULL } , σ ]



.

tree  : Tree = < root, tree1 :: tree2 :: ... :: treen >

tree' : Tree = < root', tree'1 :: tree'2 :: ... :: tree'm >

root' != *

m <= n

root == root'

(match1= tree'1.match(tree1) != NULL) & (match2= tree'2.match(tree2) != NULL) .... & (matchm= tree'm.match(treem) != NULL)

[ tree'.match (tree) , σ ] = [ { tree-match : tree-match = { <root,root'> } \cup \bigcup {match1, ....., matchm} > } , σ ]


(The above assumes that there are rules available that allow reordering of lists)



.



tree  : Tree = < root, tree1 :: tree2 :: ... :: treen >

tree' : Tree = < root', tree'1 :: tree'2 :: ... :: tree'm >

root' != *

m <= n

root == root'

\bigwedge_{\pi} \bigvee_{i} tree'π (i).match(treei) == NULL

[ tree'.match (tree) , σ ] = [ { tree-match : tree-match = NULL } , σ ]



.

[edit]

container-match.getMatch (selector-element)

container-match = < tree-match, name-match, compartment-match, state-match, binding-state-match >

tree-match = { <selector-element1, container-element1> , <selector-element2, container-element2> ..... <selector-elementn, container-elementn> }

selector-element = selector-elementi

[ container-match.getMatch (selector-element) , σ ] = [ { container-elementi } , σ ]



.


[edit]

Add-Bond (container1, container2)

Global-Bond-List = < bond1::bond2::...::bondn >

new-bond := (container1,container2)

[ AddBond (container1, container2) , σ ] = [ { Global-Bond-List = < bond1::bond2::...::bondn::new-bond >}, σ ]


.

[edit]

Delete-Bond (container1, container2)

Global-Bond-List = < bond1::bond2::...::bondn >

bond1 := (container1,container2)


[ Delete-Bond (container1, container2) , σ ] = [ { Global-Bond-List = < bond2::bond3::...::bondn > } , σ ]



.

[edit]

container.Change-State (state-name, new-state-value)

container = < name, compartment, state1::state2::...::staten, binding-state, tree >

state1 = ( name, value )

name = state-name


[ container.Change-State (state-name, new-state) , σ ] = [ { container = < name, compartment, ( state-name, new-state-value )::state2::...::staten, binding-state, tree > }, σ ]



[edit]

container.clone()

container : Container = < name, compartment, list-of-states, binding-state, tree >

[ container.clone() , σ ] --> [ { new-container : Container = < name, compartment, list-of-states, binding-state, tree > } , σ ]

Retrieved from "http://bionetgen.org/index.php/BNGSOS"