diff --git a/Benchmarks/PRISM/Polling/Polling_N_12/polling_T_10_N_12.csl b/Benchmarks/PRISM/Polling/Polling_N_12/polling_T_10_N_12.csl deleted file mode 100644 index dd1d41c..0000000 --- a/Benchmarks/PRISM/Polling/Polling_N_12/polling_T_10_N_12.csl +++ /dev/null @@ -1,2 +0,0 @@ -// once a station becomes full, probability it will be polled within T time units is ... -P=?[ true U<=10 (s=1 & a=0) ] \ No newline at end of file diff --git a/Benchmarks/PRISM/Polling/Polling_N_12/polling_T_10_N_12.prism b/Benchmarks/PRISM/Polling/Polling_N_12/polling_T_10_N_12.prism deleted file mode 100644 index d1db524..0000000 --- a/Benchmarks/PRISM/Polling/Polling_N_12/polling_T_10_N_12.prism +++ /dev/null @@ -1,90 +0,0 @@ -// polling example [IT90] -// gxn/dxp 26/01/00 - -ctmc - -const int N = 12; - -const double mu = 1; -const double gamma = 200; -const double lambda = mu/N; - -module server - - s : [1..N]; // station - a : [0..1]; // action: 0=polling, 1=serving - - [loop1a] (s=1)&(a=0) -> gamma : (s'=s+1); - [loop1b] (s=1)&(a=0) -> gamma : (a'=1); - [serve1] (s=1)&(a=1) -> mu : (s'=s+1)&(a'=0); - - [loop2a] (s=2)&(a=0) -> gamma : (s'=s+1); - [loop2b] (s=2)&(a=0) -> gamma : (a'=1); - [serve2] (s=2)&(a=1) -> mu : (s'=s+1)&(a'=0); - - [loop3a] (s=3)&(a=0) -> gamma : (s'=s+1); - [loop3b] (s=3)&(a=0) -> gamma : (a'=1); - [serve3] (s=3)&(a=1) -> mu : (s'=s+1)&(a'=0); - - [loop4a] (s=4)&(a=0) -> gamma : (s'=s+1); - [loop4b] (s=4)&(a=0) -> gamma : (a'=1); - [serve4] (s=4)&(a=1) -> mu : (s'=s+1)&(a'=0); - - [loop5a] (s=5)&(a=0) -> gamma : (s'=s+1); - [loop5b] (s=5)&(a=0) -> gamma : (a'=1); - [serve5] (s=5)&(a=1) -> mu : (s'=s+1)&(a'=0); - - [loop6a] (s=6)&(a=0) -> gamma : (s'=s+1); - [loop6b] (s=6)&(a=0) -> gamma : (a'=1); - [serve6] (s=6)&(a=1) -> mu : (s'=s+1)&(a'=0); - - [loop7a] (s=7)&(a=0) -> gamma : (s'=s+1); - [loop7b] (s=7)&(a=0) -> gamma : (a'=1); - [serve7] (s=7)&(a=1) -> mu : (s'=s+1)&(a'=0); - - [loop8a] (s=8)&(a=0) -> gamma : (s'=s+1); - [loop8b] (s=8)&(a=0) -> gamma : (a'=1); - [serve8] (s=8)&(a=1) -> mu : (s'=s+1)&(a'=0); - - [loop9a] (s=9)&(a=0) -> gamma : (s'=s+1); - [loop9b] (s=9)&(a=0) -> gamma : (a'=1); - [serve9] (s=9)&(a=1) -> mu : (s'=s+1)&(a'=0); - - [loop10a] (s=10)&(a=0) -> gamma : (s'=s+1); - [loop10b] (s=10)&(a=0) -> gamma : (a'=1); - [serve10] (s=10)&(a=1) -> mu : (s'=s+1)&(a'=0); - - [loop11a] (s=11)&(a=0) -> gamma : (s'=s+1); - [loop11b] (s=11)&(a=0) -> gamma : (a'=1); - [serve11] (s=11)&(a=1) -> mu : (s'=s+1)&(a'=0); - - [loop12a] (s=12)&(a=0) -> gamma : (s'=1); - [loop12b] (s=12)&(a=0) -> gamma : (a'=1); - [serve12] (s=12)&(a=1) -> mu : (s'=1)&(a'=0); - -endmodule - -module station1 - - s1 : [0..1]; // state of station: 0=empty, 1=full - - [loop1a] (s1=0) -> 1 : (s1'=0); - [] (s1=0) -> lambda : (s1'=1); - [loop1b] (s1=1) -> 1 : (s1'=1); - [serve1] (s1=1) -> 1 : (s1'=0); - -endmodule - -// construct further stations through renaming - -module station2 = station1 [ s1=s2, loop1a=loop2a, loop1b=loop2b, serve1=serve2 ] endmodule -module station3 = station1 [ s1=s3, loop1a=loop3a, loop1b=loop3b, serve1=serve3 ] endmodule -module station4 = station1 [ s1=s4, loop1a=loop4a, loop1b=loop4b, serve1=serve4 ] endmodule -module station5 = station1 [ s1=s5, loop1a=loop5a, loop1b=loop5b, serve1=serve5 ] endmodule -module station6 = station1 [ s1=s6, loop1a=loop6a, loop1b=loop6b, serve1=serve6 ] endmodule -module station7 = station1 [ s1=s7, loop1a=loop7a, loop1b=loop7b, serve1=serve7 ] endmodule -module station8 = station1 [ s1=s8, loop1a=loop8a, loop1b=loop8b, serve1=serve8 ] endmodule -module station9 = station1 [ s1=s9, loop1a=loop9a, loop1b=loop9b, serve1=serve9 ] endmodule -module station10 = station1 [ s1=s10, loop1a=loop10a, loop1b=loop10b, serve1=serve10 ] endmodule -module station11 = station1 [ s1=s11, loop1a=loop11a, loop1b=loop11b, serve1=serve11 ] endmodule -module station12 = station1 [ s1=s12, loop1a=loop12a, loop1b=loop12b, serve1=serve12 ] endmodule diff --git a/Benchmarks/PRISM/Polling/Polling_N_16/polling_T_10_N_16.csl b/Benchmarks/PRISM/Polling/Polling_N_16/polling_T_10_N_16.csl deleted file mode 100644 index dd1d41c..0000000 --- a/Benchmarks/PRISM/Polling/Polling_N_16/polling_T_10_N_16.csl +++ /dev/null @@ -1,2 +0,0 @@ -// once a station becomes full, probability it will be polled within T time units is ... -P=?[ true U<=10 (s=1 & a=0) ] \ No newline at end of file diff --git a/Benchmarks/PRISM/Polling/Polling_N_16/polling_T_10_N_16.prism b/Benchmarks/PRISM/Polling/Polling_N_16/polling_T_10_N_16.prism deleted file mode 100644 index 7abe195..0000000 --- a/Benchmarks/PRISM/Polling/Polling_N_16/polling_T_10_N_16.prism +++ /dev/null @@ -1,110 +0,0 @@ -// polling example [IT90] -// gxn/dxp 26/01/00 - -ctmc - -const int N = 16; - -const double mu = 1; -const double gamma = 200; -const double lambda = mu/N; - -module server - - s : [1..N]; // station - a : [0..1]; // action: 0=polling, 1=serving - - [loop1a] (s=1)&(a=0) -> gamma : (s'=s+1); - [loop1b] (s=1)&(a=0) -> gamma : (a'=1); - [serve1] (s=1)&(a=1) -> mu : (s'=s+1)&(a'=0); - - [loop2a] (s=2)&(a=0) -> gamma : (s'=s+1); - [loop2b] (s=2)&(a=0) -> gamma : (a'=1); - [serve2] (s=2)&(a=1) -> mu : (s'=s+1)&(a'=0); - - [loop3a] (s=3)&(a=0) -> gamma : (s'=s+1); - [loop3b] (s=3)&(a=0) -> gamma : (a'=1); - [serve3] (s=3)&(a=1) -> mu : (s'=s+1)&(a'=0); - - [loop4a] (s=4)&(a=0) -> gamma : (s'=s+1); - [loop4b] (s=4)&(a=0) -> gamma : (a'=1); - [serve4] (s=4)&(a=1) -> mu : (s'=s+1)&(a'=0); - - [loop5a] (s=5)&(a=0) -> gamma : (s'=s+1); - [loop5b] (s=5)&(a=0) -> gamma : (a'=1); - [serve5] (s=5)&(a=1) -> mu : (s'=s+1)&(a'=0); - - [loop6a] (s=6)&(a=0) -> gamma : (s'=s+1); - [loop6b] (s=6)&(a=0) -> gamma : (a'=1); - [serve6] (s=6)&(a=1) -> mu : (s'=s+1)&(a'=0); - - [loop7a] (s=7)&(a=0) -> gamma : (s'=s+1); - [loop7b] (s=7)&(a=0) -> gamma : (a'=1); - [serve7] (s=7)&(a=1) -> mu : (s'=s+1)&(a'=0); - - [loop8a] (s=8)&(a=0) -> gamma : (s'=s+1); - [loop8b] (s=8)&(a=0) -> gamma : (a'=1); - [serve8] (s=8)&(a=1) -> mu : (s'=s+1)&(a'=0); - - [loop9a] (s=9)&(a=0) -> gamma : (s'=s+1); - [loop9b] (s=9)&(a=0) -> gamma : (a'=1); - [serve9] (s=9)&(a=1) -> mu : (s'=s+1)&(a'=0); - - [loop10a] (s=10)&(a=0) -> gamma : (s'=s+1); - [loop10b] (s=10)&(a=0) -> gamma : (a'=1); - [serve10] (s=10)&(a=1) -> mu : (s'=s+1)&(a'=0); - - [loop11a] (s=11)&(a=0) -> gamma : (s'=s+1); - [loop11b] (s=11)&(a=0) -> gamma : (a'=1); - [serve11] (s=11)&(a=1) -> mu : (s'=s+1)&(a'=0); - - [loop12a] (s=12)&(a=0) -> gamma : (s'=s+1); - [loop12b] (s=12)&(a=0) -> gamma : (a'=1); - [serve12] (s=12)&(a=1) -> mu : (s'=s+1)&(a'=0); - - [loop13a] (s=13)&(a=0) -> gamma : (s'=s+1); - [loop13b] (s=13)&(a=0) -> gamma : (a'=1); - [serve13] (s=13)&(a=1) -> mu : (s'=s+1)&(a'=0); - - [loop14a] (s=14)&(a=0) -> gamma : (s'=s+1); - [loop14b] (s=14)&(a=0) -> gamma : (a'=1); - [serve14] (s=14)&(a=1) -> mu : (s'=s+1)&(a'=0); - - [loop15a] (s=15)&(a=0) -> gamma : (s'=s+1); - [loop15b] (s=15)&(a=0) -> gamma : (a'=1); - [serve15] (s=15)&(a=1) -> mu : (s'=s+1)&(a'=0); - - [loop16a] (s=16)&(a=0) -> gamma : (s'=1); - [loop16b] (s=16)&(a=0) -> gamma : (a'=1); - [serve16] (s=16)&(a=1) -> mu : (s'=1)&(a'=0); - -endmodule - -module station1 - - s1 : [0..1]; // state of station: 0=empty, 1=full - - [loop1a] (s1=0) -> 1 : (s1'=0); - [] (s1=0) -> lambda : (s1'=1); - [loop1b] (s1=1) -> 1 : (s1'=1); - [serve1] (s1=1) -> 1 : (s1'=0); - -endmodule - -// construct further stations through renaming - -module station2 = station1 [ s1=s2, loop1a=loop2a, loop1b=loop2b, serve1=serve2 ] endmodule -module station3 = station1 [ s1=s3, loop1a=loop3a, loop1b=loop3b, serve1=serve3 ] endmodule -module station4 = station1 [ s1=s4, loop1a=loop4a, loop1b=loop4b, serve1=serve4 ] endmodule -module station5 = station1 [ s1=s5, loop1a=loop5a, loop1b=loop5b, serve1=serve5 ] endmodule -module station6 = station1 [ s1=s6, loop1a=loop6a, loop1b=loop6b, serve1=serve6 ] endmodule -module station7 = station1 [ s1=s7, loop1a=loop7a, loop1b=loop7b, serve1=serve7 ] endmodule -module station8 = station1 [ s1=s8, loop1a=loop8a, loop1b=loop8b, serve1=serve8 ] endmodule -module station9 = station1 [ s1=s9, loop1a=loop9a, loop1b=loop9b, serve1=serve9 ] endmodule -module station10 = station1 [ s1=s10, loop1a=loop10a, loop1b=loop10b, serve1=serve10 ] endmodule -module station11 = station1 [ s1=s11, loop1a=loop11a, loop1b=loop11b, serve1=serve11 ] endmodule -module station12 = station1 [ s1=s12, loop1a=loop12a, loop1b=loop12b, serve1=serve12 ] endmodule -module station13 = station1 [ s1=s13, loop1a=loop13a, loop1b=loop13b, serve1=serve13 ] endmodule -module station14 = station1 [ s1=s14, loop1a=loop14a, loop1b=loop14b, serve1=serve14 ] endmodule -module station15 = station1 [ s1=s15, loop1a=loop15a, loop1b=loop15b, serve1=serve15 ] endmodule -module station16 = station1 [ s1=s16, loop1a=loop16a, loop1b=loop16b, serve1=serve16 ] endmodule diff --git a/Benchmarks/PRISM/Polling/Polling_N_20/polling_T_10_N_20.csl b/Benchmarks/PRISM/Polling/Polling_N_20/polling_T_10_N_20.csl deleted file mode 100644 index dd1d41c..0000000 --- a/Benchmarks/PRISM/Polling/Polling_N_20/polling_T_10_N_20.csl +++ /dev/null @@ -1,2 +0,0 @@ -// once a station becomes full, probability it will be polled within T time units is ... -P=?[ true U<=10 (s=1 & a=0) ] \ No newline at end of file diff --git a/Benchmarks/PRISM/Polling/Polling_N_20/polling_T_10_N_20.prism b/Benchmarks/PRISM/Polling/Polling_N_20/polling_T_10_N_20.prism deleted file mode 100644 index bee0591..0000000 --- a/Benchmarks/PRISM/Polling/Polling_N_20/polling_T_10_N_20.prism +++ /dev/null @@ -1,130 +0,0 @@ -// polling example [IT90] -// gxn/dxp 26/01/00 - -ctmc - -const int N = 20; - -const double mu = 1; -const double gamma = 200; -const double lambda = mu/N; - -module server - - s : [1..N]; // station - a : [0..1]; // action: 0=polling, 1=serving - - [loop1a] (s=1)&(a=0) -> gamma : (s'=s+1); - [loop1b] (s=1)&(a=0) -> gamma : (a'=1); - [serve1] (s=1)&(a=1) -> mu : (s'=s+1)&(a'=0); - - [loop2a] (s=2)&(a=0) -> gamma : (s'=s+1); - [loop2b] (s=2)&(a=0) -> gamma : (a'=1); - [serve2] (s=2)&(a=1) -> mu : (s'=s+1)&(a'=0); - - [loop3a] (s=3)&(a=0) -> gamma : (s'=s+1); - [loop3b] (s=3)&(a=0) -> gamma : (a'=1); - [serve3] (s=3)&(a=1) -> mu : (s'=s+1)&(a'=0); - - [loop4a] (s=4)&(a=0) -> gamma : (s'=s+1); - [loop4b] (s=4)&(a=0) -> gamma : (a'=1); - [serve4] (s=4)&(a=1) -> mu : (s'=s+1)&(a'=0); - - [loop5a] (s=5)&(a=0) -> gamma : (s'=s+1); - [loop5b] (s=5)&(a=0) -> gamma : (a'=1); - [serve5] (s=5)&(a=1) -> mu : (s'=s+1)&(a'=0); - - [loop6a] (s=6)&(a=0) -> gamma : (s'=s+1); - [loop6b] (s=6)&(a=0) -> gamma : (a'=1); - [serve6] (s=6)&(a=1) -> mu : (s'=s+1)&(a'=0); - - [loop7a] (s=7)&(a=0) -> gamma : (s'=s+1); - [loop7b] (s=7)&(a=0) -> gamma : (a'=1); - [serve7] (s=7)&(a=1) -> mu : (s'=s+1)&(a'=0); - - [loop8a] (s=8)&(a=0) -> gamma : (s'=s+1); - [loop8b] (s=8)&(a=0) -> gamma : (a'=1); - [serve8] (s=8)&(a=1) -> mu : (s'=s+1)&(a'=0); - - [loop9a] (s=9)&(a=0) -> gamma : (s'=s+1); - [loop9b] (s=9)&(a=0) -> gamma : (a'=1); - [serve9] (s=9)&(a=1) -> mu : (s'=s+1)&(a'=0); - - [loop10a] (s=10)&(a=0) -> gamma : (s'=s+1); - [loop10b] (s=10)&(a=0) -> gamma : (a'=1); - [serve10] (s=10)&(a=1) -> mu : (s'=s+1)&(a'=0); - - [loop11a] (s=11)&(a=0) -> gamma : (s'=s+1); - [loop11b] (s=11)&(a=0) -> gamma : (a'=1); - [serve11] (s=11)&(a=1) -> mu : (s'=s+1)&(a'=0); - - [loop12a] (s=12)&(a=0) -> gamma : (s'=s+1); - [loop12b] (s=12)&(a=0) -> gamma : (a'=1); - [serve12] (s=12)&(a=1) -> mu : (s'=s+1)&(a'=0); - - [loop13a] (s=13)&(a=0) -> gamma : (s'=s+1); - [loop13b] (s=13)&(a=0) -> gamma : (a'=1); - [serve13] (s=13)&(a=1) -> mu : (s'=s+1)&(a'=0); - - [loop14a] (s=14)&(a=0) -> gamma : (s'=s+1); - [loop14b] (s=14)&(a=0) -> gamma : (a'=1); - [serve14] (s=14)&(a=1) -> mu : (s'=s+1)&(a'=0); - - [loop15a] (s=15)&(a=0) -> gamma : (s'=s+1); - [loop15b] (s=15)&(a=0) -> gamma : (a'=1); - [serve15] (s=15)&(a=1) -> mu : (s'=s+1)&(a'=0); - - [loop16a] (s=16)&(a=0) -> gamma : (s'=s+1); - [loop16b] (s=16)&(a=0) -> gamma : (a'=1); - [serve16] (s=16)&(a=1) -> mu : (s'=s+1)&(a'=0); - - [loop17a] (s=17)&(a=0) -> gamma : (s'=s+1); - [loop17b] (s=17)&(a=0) -> gamma : (a'=1); - [serve17] (s=17)&(a=1) -> mu : (s'=s+1)&(a'=0); - - [loop18a] (s=18)&(a=0) -> gamma : (s'=s+1); - [loop18b] (s=18)&(a=0) -> gamma : (a'=1); - [serve18] (s=18)&(a=1) -> mu : (s'=s+1)&(a'=0); - - [loop19a] (s=19)&(a=0) -> gamma : (s'=s+1); - [loop19b] (s=19)&(a=0) -> gamma : (a'=1); - [serve19] (s=19)&(a=1) -> mu : (s'=s+1)&(a'=0); - - [loop20a] (s=20)&(a=0) -> gamma : (s'=1); - [loop20b] (s=20)&(a=0) -> gamma : (a'=1); - [serve20] (s=20)&(a=1) -> mu : (s'=1)&(a'=0); - -endmodule - -module station1 - - s1 : [0..1]; // state of station: 0=empty, 1=full - - [loop1a] (s1=0) -> 1 : (s1'=0); - [] (s1=0) -> lambda : (s1'=1); - [loop1b] (s1=1) -> 1 : (s1'=1); - [serve1] (s1=1) -> 1 : (s1'=0); - -endmodule - -// construct further stations through renaming - -module station2 = station1 [ s1=s2, loop1a=loop2a, loop1b=loop2b, serve1=serve2 ] endmodule -module station3 = station1 [ s1=s3, loop1a=loop3a, loop1b=loop3b, serve1=serve3 ] endmodule -module station4 = station1 [ s1=s4, loop1a=loop4a, loop1b=loop4b, serve1=serve4 ] endmodule -module station5 = station1 [ s1=s5, loop1a=loop5a, loop1b=loop5b, serve1=serve5 ] endmodule -module station6 = station1 [ s1=s6, loop1a=loop6a, loop1b=loop6b, serve1=serve6 ] endmodule -module station7 = station1 [ s1=s7, loop1a=loop7a, loop1b=loop7b, serve1=serve7 ] endmodule -module station8 = station1 [ s1=s8, loop1a=loop8a, loop1b=loop8b, serve1=serve8 ] endmodule -module station9 = station1 [ s1=s9, loop1a=loop9a, loop1b=loop9b, serve1=serve9 ] endmodule -module station10 = station1 [ s1=s10, loop1a=loop10a, loop1b=loop10b, serve1=serve10 ] endmodule -module station11 = station1 [ s1=s11, loop1a=loop11a, loop1b=loop11b, serve1=serve11 ] endmodule -module station12 = station1 [ s1=s12, loop1a=loop12a, loop1b=loop12b, serve1=serve12 ] endmodule -module station13 = station1 [ s1=s13, loop1a=loop13a, loop1b=loop13b, serve1=serve13 ] endmodule -module station14 = station1 [ s1=s14, loop1a=loop14a, loop1b=loop14b, serve1=serve14 ] endmodule -module station15 = station1 [ s1=s15, loop1a=loop15a, loop1b=loop15b, serve1=serve15 ] endmodule -module station16 = station1 [ s1=s16, loop1a=loop16a, loop1b=loop16b, serve1=serve16 ] endmodule -module station17 = station1 [ s1=s17, loop1a=loop17a, loop1b=loop17b, serve1=serve17 ] endmodule -module station18 = station1 [ s1=s18, loop1a=loop18a, loop1b=loop18b, serve1=serve18 ] endmodule -module station19 = station1 [ s1=s19, loop1a=loop19a, loop1b=loop19b, serve1=serve19 ] endmodule -module station20 = station1 [ s1=s20, loop1a=loop20a, loop1b=loop20b, serve1=serve20 ] endmodule diff --git a/Benchmarks/PRISM/README.md b/Benchmarks/PRISM/README.md deleted file mode 100644 index 9c1f3e3..0000000 --- a/Benchmarks/PRISM/README.md +++ /dev/null @@ -1,20 +0,0 @@ -# PRISM Benchmarks - -Some benchmarks here were taken from those provided by [PRISM](https://prismmodelchecker.org). The upstream URL is [https://github.com/prismmodelchecker/prism-benchmarks](https://github.com/prismmodelchecker/prism-benchmarks). - -## Jackson - -TODO: Steal description from PRISM folks - -## Polling - -TODO: Steal description from PRISM folks - -## Robot World - -TODO: Steal description from PRISM folks - -## Tandem Queue - -TODO: Steal description from PRISM folks - diff --git a/Benchmarks/README.md b/Benchmarks/README.md index 48c0292..d8c438f 100644 --- a/Benchmarks/README.md +++ b/Benchmarks/README.md @@ -2,18 +2,9 @@ The first benchmark suite is adapted from the systems biology markup language (SBML) [1,2] stochastic test suite [3] accessible at https://github.com/sbmlteam/sbml-test-suite/tree/release/cases/stochastic. SBML is an XML-based data format encoding models of biological systems. The test suite is designed for testing software for analyzing SBML models and has been converted into the PRISM language to also allow the testing of software for stochastic model checking. From the 100 cases provided by the SBML test suite, three were not included since the SBML-to-PRISM converter currently does not support rules or events. -## PRISM Benchmark Suite -In addition to the SBML benchmark models, we have included the PRISM benchmark suite [4]. This suite has several models including game models and ``toy'' simulations. The PRISM benchmark suite is licensed under the GPLv2 license, a prominent open-source license that allows for redistribution and modification as long as the license under which any copies (modified or not) remain unchanged. As a result of this freedom, PRISM benchmarks are also accessible in our repository. These models are used to test STAMINA [5,6], an infinite model-checking tool which supports the PRISM format. - ## References [1] Keating, Sarah M., Dagmar Waltemath, Matthias König, Fengkai Zhang, Andreas Dräger, Claudine Chaouiya, Frank T. Bergmann et al. "SBML Level 3: an extensible format for the exchange and reuse of biological models." Molecular systems biology 16, no. 8 (2020): e9110. [2] Hucka, Michael, Andrew Finney, Herbert M. Sauro, Hamid Bolouri, John C. Doyle, Hiroaki Kitano, Adam P. Arkin et al. "The systems biology markup language (SBML): a medium for representation and exchange of biochemical network models." Bioinformatics 19, no. 4 (2003): 524-531. [3] Evans, Thomas W., Colin S. Gillespie, and Darren J. Wilkinson. "The SBML discrete stochastic models test suite." Bioinformatics 24, no. 2 (2008): 285-286. - -[4] Kwiatkowska, Marta, Gethin Norman, and David Parker. "PRISM 4.0: Verification of probabilistic real-time systems." In Computer Aided Verification: 23rd International Conference, CAV 2011, Snowbird, UT, USA, July 14-20, 2011. Proceedings 23, pp. 585-591. Springer Berlin Heidelberg, 2011. - -[5] Neupane, Thakur, Chris J. Myers, Curtis Madsen, Hao Zheng, and Zhen Zhang. "Stamina: Stochastic approximate model-checker for infinite-state analysis." In Computer Aided Verification: 31st International Conference, CAV 2019, New York City, NY, USA, July 15-18, 2019, Proceedings, Part I 31, pp. 540-549. Springer International Publishing, 2019. - -[6] Roberts, Riley, Thakur Neupane, Lukas Buecherl, Chris J. Myers, and Zhen Zhang. "STAMINA 2.0: Improving scalability of infinite-state stochastic model checking." In Verification, Model Checking, and Abstract Interpretation: 23rd International Conference, VMCAI 2022, Philadelphia, PA, USA, January 16–18, 2022, Proceedings, pp. 319-331. Cham: Springer International Publishing, 2022. diff --git a/FaultTolerance/README.md b/FaultTolerance/README.md deleted file mode 100644 index db151fc..0000000 --- a/FaultTolerance/README.md +++ /dev/null @@ -1,76 +0,0 @@ -# Fault Tolerance Computing and Electronics - -This directory contains models in the fault tolerance domain. - -At present there are two subdirectories containing -specialized models: - -``` -|-- Redundancy -| |-- RFB -| `-- TMR -`-- StochasticComputing - |-- divide_by_two - `-- divider -``` - -An overview of each subcategory and the specific models is -provided in the text below. All of the provided cases are -designed to model transient noise or "soft" upsets, as opposed -to permanent hardware defects. - - -# Redundancy Models - -Fault tolerant systems usually have redundant modules and/or signals -so that the system's correct function can be recovered, even in the -event of an error. - -## TMR: Triple Modular Redundancy - -This model represents a classic "majority vote" redundancy technique -that has been deployed in critical systems since the 1960s. The TMR -model has a low state complexity and is provided mainly as a benchmark -for judging the RFB model. - -## RFB: Restorative Feedback - -This model is an updated form of TMR designed to suppress transient -faults. RFB is also suitable for fault tolerance with non-binary -discrete signals as might be encountered in a data communication bus -or high-density Flash memory. Due to its feedback dynamics and -non-binary signals, RFB can have a large or infinite state complexity. - -Two PRISM models are provided: - -* `rfb.pm` -- a binary-valued model with low state complexity. -* `rfb_inf.pm` -- a multiple-valued model with infinite state complexity. - - -# Stochastic Computing Models - -Fault tolerant systems sometimes employ "approximate" computing strategies -for masking or detecting errors in arithmetic or signal processing -circuits. Stochastic computing circuits operate by filtering pseudo- -random bit-streams (PRBS) wherein the computation depends on the overall -average value rather than any particular bit. These circuits are therefore -insensitive to a small number of transient upsets. - -## Divide-By-Two Circuit - -The stochastic divide-by-two function is based on the toggle flip-flop, -which provides a uniform output probability (i.e. average) independent -of the input probability. By using a simple feedback arrangement, this -property can be used to divide a PRBS value by 2. - - -## Divider - -The divider circuit uses a counter to estimate a PRBS probability and -"re-emit" an independent PRBS with the same average value. The re- -emitted stream is then used in feedback to obtain the ratio of two -PRBS averages. Two models are provided: - -* `divider.pm` -- a finite-state model with a fixed counter precision. -* `divider_inf.pm` -- an infinite-state model with a variable counter precision. - diff --git a/FaultTolerance/Redundancy/RestorativeFeedback/README.md b/FaultTolerance/Redundancy/RestorativeFeedback/README.md deleted file mode 100644 index 895b310..0000000 --- a/FaultTolerance/Redundancy/RestorativeFeedback/README.md +++ /dev/null @@ -1,242 +0,0 @@ -# Restorative Feedback (RFB) Model - -This case example models a restorative feedback (RFB) circuit -for in-situ transient error correction in logic circuits and -systems. RFB can be classified as a type of Triple Modular -Redundancy (TMR) wherein logic functions and signals are -instantiated in triplicate. Classical TMR systems use majority -vote to correct a single error, but cannot detect or correct -muliple errors. The RFB circuit is designed to correct momentary -upsets with better reliability than Majority TMR. RFB is able -to suppress multiple momentary faults when the feedback is -active. - -There are two RFB models provided: - -* `rfb.pm` -- a PRISM model for a binary-valued RFB circuit with finite state complexity. - Properties are given in `rfb.props`. -* `rfb_inf.pm` -- a PRISM model for a multiple-valued RFB circuit with infinite state complexity. - Properties are given in `rfb_inf.props`. - - -## Description of the Binary RFB Circuit - -The RFB circuit is based on a modified Muller C-element gate. -The classical C-element is a binary-valued latch with behavior -described as - -``` -if (A==B) - C = A; -``` - -When `A!=B` there is no change in `C`. - -In the RFB circuit, the modified C-element has two modes depending -on an external clock. When the clock is low, the C-element is initialized -to the value of an extra input `I`. When the clock is high, the C-element -behaves as usual: - -``` -if (clk) begin - if (A==B) - C = A; -end else - C = I; -``` - -![Modified Celement with initialization input.](../../../Media/ModifiedCElement.png) - -The RFB circuit shown below presumes that a logic system is replicated for a total -of three instances. Three logic signals x0, x1, and x2 represent instances -the same logic value. Any of the signals may momentarily "flip" to an -erroneous value due to interference or noise. When the clock signal (not shown) -is low, the outputs y0, y1, and y2 are initialized to values sampled from -x1, x2, and x0, respectively. When the clock is high, the C-element outputs -are passed in a feedback cycle which corrects errors and suppresses further upsets. - -![RFB circuit.](../../../Media/RFBCircuit.png) - -To see how a single error is corrected, suppose x0 is initially in error, -so the input values are (x0,x1,x2)=(1,0,0). During the initialization, -the output values are set to (y0,y1,y2)=(x3,x1,x2)=(0,1,0). When the -clock swings high, the three C-elements see respective inputs (1,0), -(0,0) and (0,1). Since C2 sees inputs (0,0), its output is changed to -y2=0, so the outputs finally become (0,0,0) and the error is corrected. - -Reference: - -* Chris Winstead, Yi Luo, Eduardo Monzon, and Abiezer Tejeda, - "An Error Correction Method for Binary and Multiple-Valued Logic", - *IEEE International Symposium on Multiple-Valued Logic*, 2011. -* Chris Winstead, Yi Luo, Eduardo Monzon, and Abiezer Tejeda, - "Error Correction via Restorative Feedback in M-ary Logic Circuits", - *J. of Multiple Valued Logic and Soft Computing*, Vol. 23, pp. 337, 2014. - - -### PRISM Model for the Binary RFB Circuit - -The PRISM model for this circuit is provided in -`rfb.pm`. The input signals are assumed to be 0 (when correct), -so a value of `1` indicates an error. The momentary upset rate -is specified via constant `epsilon`, and the signal recovery rate -is `Rc`. There is also a latch upset rate `alpha` which affects -the C-element memory. - -For a C-element with inputs `A` and `B`, upsets are modeled as -follows: - -* When `A=B`: not susceptible to state upsets. -* When `A!=B`: susceptible to upset with rate `alpha`. - -The initial states are constrained by the integer -constant named `initialErrors`, which indicates how -many signal errors occur when the clock transitions from -low to high. The PRISM model represents behavior during -the correction phase, where the speed and ultimate error -probability are determined by the circuit's feedback -dynamics. - -Two example properties are given in `rfb.props`: - -* `P=? [ F[T,T] y1+y2+y3>1 ]` evaluates the probability -that a non-correctable error state exists at time `T`. The -constant `T` is a `double` indicating the elapsed time in -the circuit's correction phase. -* `S=? [ y1+y2+y3>1 ]` evaluates the steady-state probability -that a non-correctable error state exists in the circuit's -output. - - -### Example results: - -The results given here are informative in comparison to the classical -TMR model located in `../TMR`, demonstrating that RFB is more -reliable for a system with the indicated parameters. - - -#### `T=0`, `initialErrors=1` - -This case models the initial error probability before activating -restorative feedback. Since there is initially only one error, -we expect the timed property to be zero. - -``` -prism -const T=0 -const initialErrors=1 rfb.pm rfb.props -``` - -For the first property (at `T=0`) PRISM returns: - -``` -Result: [0.0,0.0] -``` - -For the second property (steady state) PRISM returns: - -``` -Result: [1.272254163993728E-6,1.272254163993728E-6] -``` - -#### `T=1.0`, `initialErrors=1` - -This case models the error probability 1.0 time units after -activating restorative feedback. This case provides -information about the circuit's transient reliability. - -``` -prism -const T=1.0 -const initialErrors=1 rfb.pm rfb.props -``` - -For the first property (at `T=0`) PRISM returns: - -``` -Result: [4.3735439267849973E-4,4.3735439267849984E-4] -``` - -For the second property (steady state) PRISM returns: - -``` -Result: [1.272254163993728E-6,1.272254163993728E-6] -``` - - -## Description of the Multiple-Valued RFB Circuit - -One of the motivations for the RFB method is to apply TMR -to systems with non-binary signals. Classical TMR relies on -Majority logic that requires two of the three signals be -equal. In systems with multiple-valued signals, all three -signals may differ, so there is no majority. In that situation, -the C-element's latching behavior provides a solution. - -The multiple-valued C-Element and RFB circuit have the same -design as the binary case, except that the signals are allowed -to be arbitrary discrete levels. The upset processes are now -also multiple-valued, requiring more complex models. - - -### PRISM Model for the Multiple-Valued RFB Circuit - -The PRISM model for this circuit is provided in -`rfb_inf.pm`. The input signals are assumed to be 0 (when correct). -The momentary upset rate is specified via constant `epsilon`, and -the signal recovery rate is `Rc`. Since the signal values are non-binary, -the upset amplitude is modeled by a "noise" signal with rate `Rn`. -The noise amplitude distribution is: - -* n=1 with rate `Rn` -* n=2 with rate `Rn/2` -* n=3 with rate `Rn/4` -* n=4 with rate `Rn/8` - -This example noise process is not based on any specific physical model, -but is similar to "random telegraph noise" known to affect various FET -and memristor devices. - -There is also a latch upset rate `alpha` which affects the C-element memory. -Here the latch upset is identical to the binary-valued circuit. Latch upsets -always have amplitude 1, i.e. the C-element output drifts to an adjacent -signal level. - -Initial values for this model are given explicitly via integer constants -`i1`, `i2`, and `i3`, so a single initial state is specified (the binary- -valued circuit allowed specifying an ensemble of initial states, but that -is not possible here). - -Property definitions are more challenging for the multiple-valued circuit -compared to the binary case. Steady-state properties are not available -due to the model's unbounded state complexity. One property is provided -in `rfb_inf.props`: - -* `P=? [ F[T,T] y1+y2+y3!=0 ]` - -This evaluates the probability that the output signals are error-free at -time `T`. - -### Example Results for the Multiple-Valued Circuit - -#### `i1=0`, `i2=3`, `i3=1`, `T=20` - -``` -prism -sim -const i1=0 -const i2=3 -const i3=1 -const T=20 rfb_inf.pm rfb_inf.props -``` - -The result reported by PRISM is - -``` -Result: 0.051 (+/- 0.017928853962181267 with probability 0.99; rel err 0.3515461561212013) -``` - - -#### `i1=0`, `i2=0`, `i3=1`, `T=20` - -``` -prism -sim -const i1=0 -const i2=0 -const i3=1 -const T=20 rfb_inf.pm rfb_inf.props -``` - -The result reported by PRISM is - -``` -Result: 0.024 (+/- 0.012472826037899055 with probability 0.99; rel err 0.5197010849124606) -``` - diff --git a/FaultTolerance/Redundancy/RestorativeFeedback/RestorativeFeedback.pm b/FaultTolerance/Redundancy/RestorativeFeedback/RestorativeFeedback.pm deleted file mode 100644 index a421d29..0000000 --- a/FaultTolerance/Redundancy/RestorativeFeedback/RestorativeFeedback.pm +++ /dev/null @@ -1,49 +0,0 @@ -// rfb.pm -// Restorative Feedback model -// A type of Triple Modular Redundancy (TMR) -ctmc - -const double Rc = 10; // signal transition rate of logic gates -const double Rn = 2; // noise process rate -const double epsilon = 1; // transient upset rate -const double alpha = .1; // state upset rate -const double T; -const int i1; -const int i2; -const int i3; - - -// Noise sources -module noise1 - n1: int init 0; - - [] (true) -> Rn:(n1'=1)+(Rn/2):(n1'=2)+(Rn/4):(n1'=3)+(Rn/8):(n1'=4); -endmodule -module noise2 = noise1 [ n1=n2 ] endmodule -module noise3 = noise1 [ n1=n3 ] endmodule - - -// Signal Source -module source1 - x1 : int init i1; - - [] (x1 > 0) -> (epsilon/2):(x1'=x1+n1) + (epsilon/2):(x1'=x1-n1) + Rc:(x1'=x1-1); - [] (x1 = 0) -> (epsilon/2):(x1'=x1+n1) + (epsilon/2):(x1'=x1-n1); - [] (x1 < 0) -> (epsilon/2):(x1'=x1+n1) + (epsilon/2):(x1'=x1-n1) + Rc:(x1'=x1+1); -endmodule - -module source2 = source1 [ x1=x2, i1=i2, n1=n2 ] endmodule -module source3 = source1 [ x1=x3, i1=i3, n1=n3 ] endmodule - - -// Modified Muller C-element -module Cem1 - y1 : int init i3; - - [] (x1 = y3) -> (Rc):(y1' = y3); - [] (x1 != y3) -> (alpha/2):(y1'=y1+1)+(alpha/2):(y1'=y1-1); -endmodule - -module Cem2 = Cem1 [ x1=x2, y1=y2, y3=y1, i3 = i1 ] endmodule -module Cem3 = Cem1 [ x1=x3, y1=y3, y3=y2, i3 = i2 ] endmodule - diff --git a/FaultTolerance/Redundancy/RestorativeFeedback/RestorativeFeedback.props b/FaultTolerance/Redundancy/RestorativeFeedback/RestorativeFeedback.props deleted file mode 100644 index 7228516..0000000 --- a/FaultTolerance/Redundancy/RestorativeFeedback/RestorativeFeedback.props +++ /dev/null @@ -1 +0,0 @@ -P=? [ F[T,T] y1+y2+y3!=0 ] diff --git a/FaultTolerance/Redundancy/RestorativeFeedback/RestorativeFeedback_bound.pm b/FaultTolerance/Redundancy/RestorativeFeedback/RestorativeFeedback_bound.pm deleted file mode 100644 index 34858c1..0000000 --- a/FaultTolerance/Redundancy/RestorativeFeedback/RestorativeFeedback_bound.pm +++ /dev/null @@ -1,35 +0,0 @@ -// rfb.pm -// Restorative Feedback model -// A type of Triple Modular Redundancy (TMR) -ctmc - -const double Rc =100; // signal transition rate of logic gates -const double epsilon =1; // transient upset rate -const double alpha =0.01; // state upset rate -const double T; -const int initialErrors; - -// Signal Source -module source1 - x1 : [0..1]; - - [] (true) -> epsilon:(x1'=1) + Rc:(x1'=0); -endmodule - -module source2 = source1 [x1=x2] endmodule -module source3 = source1 [x1=x3] endmodule - - -// Modified Muller C-element -module Cem1 - y1 : [0..1]; - - [] (x1 = y3) -> (Rc):(y1' = y3); - [] (x1 != y3) -> (alpha):(y1'=1-y1); -endmodule - -module Cem2 = Cem1 [y1=y2, x1=x2, y3=y1] endmodule -module Cem3 = Cem1 [y1=y3, x1=x3, y3=y2] endmodule - - -init ((x1+x2+x3=initialErrors) & ((y1=x3)&(y2=x1)&(y3=x2))) endinit diff --git a/FaultTolerance/Redundancy/RestorativeFeedback/RestorativeFeedback_bound.props b/FaultTolerance/Redundancy/RestorativeFeedback/RestorativeFeedback_bound.props deleted file mode 100644 index c72acba..0000000 --- a/FaultTolerance/Redundancy/RestorativeFeedback/RestorativeFeedback_bound.props +++ /dev/null @@ -1,2 +0,0 @@ -P=? [ F[T,T] y1+y2+y3>1 ] -S=? [ y1+y2+y3>1 ] \ No newline at end of file diff --git a/FaultTolerance/Redundancy/TripleModularRedundancy/README.md b/FaultTolerance/Redundancy/TripleModularRedundancy/README.md deleted file mode 100644 index 4184f47..0000000 --- a/FaultTolerance/Redundancy/TripleModularRedundancy/README.md +++ /dev/null @@ -1,100 +0,0 @@ -# Triple Modular Redundancy (TMR) Model - -This case example models a Triple Modular Redundancy (TMR) circuit -wherein logic functions and signals are instantiated in triplicate. -Logic states are corrected using majority vote modules, so that a -single error can be corrected. In this model we assume that all signals -are susceptible to momentary upsets, including the majority outputs. - - -## Description of the Circuit - - -The TMR circuit shown below presumes that a logic system is replicated for a total -of three instances. Three logic signals x0, x1, and x2 represent instances -the same logic value. Any of the signals may momentarily "flip" to an -erroneous value due to interference or noise. The majority gates labeled `M` -output the majority decision among the three input signals. Since the majority -gates may also be susceptible to upsets, there are three independent majority -gates so that there is never a single point of failure. - -![Majority TMR circuit.](../../../Media/MajorityTMR.png) - -Reference: - -* R. E. Lyons and W. Vanderkulk, "The use of triple-modular redundancy to improve -computer reliability." *IBM Journal of Research and Development*, 6(2):200, 1962. - -## PRISM Model - -The PRISM model for this circuit is provided in -`tmr.pm`. The input signals are assumed to be 0 (when correct), -so a value of `1` indicates an error. The momentary upset rate -is specified via constant `epsilon`, and the signal recovery rate -is `Rc`. - -The initial states are constrained by the integer -constant named `initialErrors`, which indicates how -many signal errors are present in the initial state. - -Two example properties are given in `tmr.props`: - -* `P=? [ F[T,T] y1+y2+y3>1 ]` evaluates the probability -that a non-correctable error state exists at time `T`. The -constant `T` is a `double` indicating the elapsed time. -* `S=? [ y1+y2+y3>1 ]` evaluates the steady-state probability -that a non-correctable error state exists in the circuit's -output. - -The TMR's output error probability is not strongly dependent on -time, so these two properties should usually be close to each other. - - -## Example results: - - -### `T=0`, `initialErrors=1` - -This case models the initial error probability. Since the majority -gates have undefined (or unconstrained) initial output values, -the instantaneous error probability is indeteminate. - -``` -prism -const T=0 -const initialErrors=1 tmr.pm tmr.props -``` - -For the first property (at `T=0`) PRISM returns: - -``` -Result: [0.0,1.0] -``` - -For the second property (steady state) PRISM returns: - -``` -Result: [4.94427886688858E-4,4.94427886688858E-4] -``` - -### `T=1.0`, `initialErrors=1` - -This case models the error probability after 1.0 time units. -Since this is well beyond the mean signal recovery time `1/Rc`, -the transient error probability should be nearly equal to the steady -state. - -``` -prism -const T=1.0 -const initialErrors=1 tmr.pm tmr.props -``` - -For the first property (at `T=0`) PRISM returns: - -``` -Result: [4.944279220969286E-4,4.94427973657968E-4] -``` - -For the second property (steady state) PRISM returns: - -``` -Result: [4.94427886688858E-4,4.94427886688858E-4] -``` - diff --git a/FaultTolerance/Redundancy/TripleModularRedundancy/TripleModularRedundancy.pm b/FaultTolerance/Redundancy/TripleModularRedundancy/TripleModularRedundancy.pm deleted file mode 100644 index 69b9e8e..0000000 --- a/FaultTolerance/Redundancy/TripleModularRedundancy/TripleModularRedundancy.pm +++ /dev/null @@ -1,35 +0,0 @@ -// tmr.pm -// Triple Modular Reduncancy model -// using majority logic -ctmc - -const double Rc=100; // signal transition rate of logic gates -const double epsilon=1; // transient upset rate -const double T; -const int initialErrors; - -// Signal Source -module source1 - x1 : [0..1]; - - [] (true) -> epsilon:(x1'=1) + Rc:(x1'=0); -endmodule - -module source2 = source1 [x1=x2] endmodule -module source3 = source1 [x1=x3] endmodule - - -// Majority Gates -module Maj1 - y1 : [0..1]; - - [] (x1 + x2 + x3 > 1) -> (Rc):(y1' = 1) + epsilon:(y1'=0); - [] (x1 + x2 + x3 < 2) -> (Rc):(y1' = 0) + epsilon:(y1'=1); - -endmodule - -module Maj2 = Maj1 [y1=y2] endmodule -module Maj3 = Maj1 [y1=y3] endmodule - - -init (x1+x2+x3=initialErrors) endinit diff --git a/FaultTolerance/Redundancy/TripleModularRedundancy/TripleModularRedundancy.props b/FaultTolerance/Redundancy/TripleModularRedundancy/TripleModularRedundancy.props deleted file mode 100644 index c72acba..0000000 --- a/FaultTolerance/Redundancy/TripleModularRedundancy/TripleModularRedundancy.props +++ /dev/null @@ -1,2 +0,0 @@ -P=? [ F[T,T] y1+y2+y3>1 ] -S=? [ y1+y2+y3>1 ] \ No newline at end of file diff --git a/FaultTolerance/StochasticComputing/divide_by_two/README.md b/FaultTolerance/StochasticComputing/divide_by_two/README.md deleted file mode 100644 index 0107305..0000000 --- a/FaultTolerance/StochasticComputing/divide_by_two/README.md +++ /dev/null @@ -1,76 +0,0 @@ -# Unipolar Stochastic Divide-By-Two Model - -This case example models a stochastic divide-by-two circuit -using the unipolar stochastic numerical format. In the -unipolar format, a signal $x$ is a real number between -0 and 1, encoded probabilistically in a binary signal -$X(t)$. At any time $t$, the signal $X(t)=1$ with -probability $x$, and $X(t)=0$ with probability $1-x$. - -## Description of the Circuit - -The divide-by-two circuit schematic is shown below. It accepts -one stochastic input, $A(t)$, and produces a single output $Q(t)$. -Ideally $Q$ should arrive at a steady-state probability $q=a/2$. - -![Unary divide-by-two schematic](../../../Media/StochasticDivideByTwo.png) - -The principle of operation is as follows. The toggle flip-flop -emits a bitstream $B(t)$ with steady-state probability $b=1/2$, -independent of the input stream probability. The AND gate acts as -a probability multiplier, so it emits a bitstream with probability -$q=ab=q/2$. - -Reference: - -* C. Winstead, "Tutorial on Stochastic Computation," - Chapter 2 in *Stochastic Computing: Techniques and Applications*, - ed. Gaudet and Gross, Springer, 2019. - - -## PRISM Model - -The PRISM model for this circuit is provided in -`divide_by_two.pm`. The input probability is given -via the constant `a`. Internally, the stochastic -input signal is `inA`, and the output signal is `Q`. - -Three example properties are given in `divide_by_two.props`: - -* `P=? [ F[T,T] Q = 1 ]` evaluates the probability -that Q=1 (i.e. the numerical output $q$) at `T` clock cycles, -which relates to the circuit's response time. The constant `T` -is an integer. -* `S=? [ Q = 1 ]` evaluates the steady-state probability -that Q=1. -* `P=? [ F[T,T] Q = 1 ] - S=? [ Q = 1 ]` evaluates the transient -absolute error in output probability at clock cycle `T`. - -## Example results: - -### `a=0.1` and `T=100` - -The expected output is $q=0.05$. - -``` -prism --const a=0.1 --const T=100 divide_by_two.pm divide_by_two.props -``` - -For the first property (at 100 clock cycles) PRISM returns: - -``` -Result: 0.049999999984085816 (exact floating point) -``` - -For the second property (steady state) PRISM returns: - -``` -Result: 0.04999998765587841 -``` - -For the third property (transient error) PRISM returns: - -``` -Result: 1.2328207406320235E-8 -``` - diff --git a/FaultTolerance/StochasticComputing/divide_by_two/divide_by_two.pm b/FaultTolerance/StochasticComputing/divide_by_two/divide_by_two.pm deleted file mode 100644 index 03164a2..0000000 --- a/FaultTolerance/StochasticComputing/divide_by_two/divide_by_two.pm +++ /dev/null @@ -1,39 +0,0 @@ -// divide_by_two.pm -// Unipolar Stochastic Divide-By-2 -// Based on Toggle Flip-Flop - -dtmc - -const double a; // input value between 0 and 1 -const int T; // clock cycle count - -//------------------ -// Signal Sources -//------------------ -module Source0 - inA : [0..1] init 0; - - [event] (true) -> a:(inA'=1) + (1-a):(inA'=0); -endmodule - -//------------------------ -// Toggle Flip-Flop (TFF) -//------------------------ -module TFF - B : [0..1] init 0; - - [event] (inA=0) -> (B' = B); - [event] (inA=1) -> (B' = 1-B); -endmodule - - -//------------------ -// AND gate -//------------------ -module AND0 - - Q : [0..1] init 0; - - [event] (inA=1 & B=1) -> (Q'=1); - [event] (inA=0 | B=0) -> (Q'=0); -endmodule diff --git a/FaultTolerance/StochasticComputing/divide_by_two/divide_by_two.props b/FaultTolerance/StochasticComputing/divide_by_two/divide_by_two.props deleted file mode 100644 index cf2de91..0000000 --- a/FaultTolerance/StochasticComputing/divide_by_two/divide_by_two.props +++ /dev/null @@ -1,5 +0,0 @@ -P=? [ F[T,T] Q=1 ] - -S=? [ Q=1 ] - -(P=? [ F[T,T] Q=1 ]) - (S=? [ Q=1 ]) diff --git a/FaultTolerance/StochasticComputing/divider/README.md b/FaultTolerance/StochasticComputing/divider/README.md deleted file mode 100644 index 5fd2591..0000000 --- a/FaultTolerance/StochasticComputing/divider/README.md +++ /dev/null @@ -1,126 +0,0 @@ -# Unipolar Stochastic Divider Model - -This case example models a stochastic divider using -the unipolar stochastic numerical format. In the -unipolar format, a signal $x$ is a real number between -0 and 1, encoded probabilistically in a binary signal -$X(t)$. At any time $t$, the signal $X(t)=1$ with -probability $x$, and $X(t)=0$ with probability $1-x$. - -Two models are provided: - -* `divider.pm` is a finite-state model. -* `divider_inf.pm` is an intinite-state model. - -Both models rely on a finite up-down counter to -estimate the average probability of a unary stochastic -bitstream. The finite counter saturates at `MAX_COUNT`, -which is a fixed constant in the model. - -In the infinite-state model, the counter's limit is -variable, initially +/-1 and increasing logarithmically -with respect to the elapsed clock cycles. This approach -improves accuracy for calculations with small probabilities, -e.g. below 0.01, however the state complexity becomes -unbounded in this model. - - -## Description of the Circuit - -The divider circuit shematic is shown below. It accepts -two stochastic inputs, $A(t)$ and $B(t)$, and produces a -single output $Q(t)$. Ideally $Q$ should arrive at a -steady-state probability $Q(t)=q=a/b$. - -![Unary divider schematic](../../../Media/StochasticUnaryDivider.png) - -The principle of operation is as follows. The signed up/down -counter (UDC) reaches equilibrium when its inputs have equal -probability. The module R emits a bit stream with probability -equal to the counter value C, scaled to the range (0,1). -The AND gate acts as a probability multiplier, so it emits bits -with probability $qb$. Due to the feedback connection, at -steady state we expect $qb=a$ and therefore $q=a/b$. - -Reference: - -* C. Winstead, "Tutorial on Stochastic Computation," - Chapter 2 in *Stochastic Computing: Techniques and Applications*, - ed. Gaudet and Gross, Springer, 2019. - - -## PRISM Model - -The input probabilities are given via constants `a` and `b`. Internally, -the stochastic input signals are `inA` and `inB`, and the output -signal is `Q`. - -Two example properties are given in `divider.props`: - -* `P=? [ F[T,T] Q = 1 ]` evaluates the probability -that Q=1 (i.e. the numerical output $q$) at `T` clock cycles, -which relates to the circuit's response time. The constant `T` -is an integer. -* `S=? [ Q = 1 ]` evaluates the steady-state probability -that Q=1. - -## Example results (finite state model): - -### `a=0.1`, `b=0.3`, and `T=100` - -The expected output is $q=1/3$. - -``` -prism --const a=0.1 --const b=0.3 --const T=100 divider.pm divider.props -``` - -For the first property (at 100 clock cycles) PRISM returns: - -``` -Result: 0.4665562152140168 (exact floating point) -``` - -For the second property (steady state) PRISM returns: - -``` -Result: 0.33333443639168 -``` - - -### `a=0.7`, `b=0.3`, and `T=100` - -In this case the ratio $a/b$ is greather than one, so the expected output -is saturated close to $q=1$. - -``` -prism --const a=0.1 --const b=0.3 --const T=100 divider.pm divider.props -``` - -For the first property (at 100 clock cycles) PRISM returns: - -``` -Result: 0.8790749994268042 (exact floating point) -``` - -For the second property (steady state) PRISM returns: - -``` -Result: 0.9881554646304057 -``` - - -## Example results (infinite state model): - -### `a=0.001`, `b=0.1` - -In this case PRISM is best used to simulate a path with -10,000 clock cycles. The output bitstream `Q` is reported in -column 9 of the output trace. - -``` -prism -simpath time=10000 data -const a=0.001 -const b=0.1 -const T=1000 divider_inf.pm -``` - -In this model PRISM is unable to provide the requested path length, -so it is not possible to compute the long-term transient behavior -or the steady-state output probability using PRISM. diff --git a/FaultTolerance/StochasticComputing/divider/divider.pm b/FaultTolerance/StochasticComputing/divider/divider.pm deleted file mode 100644 index fde5be1..0000000 --- a/FaultTolerance/StochasticComputing/divider/divider.pm +++ /dev/null @@ -1,49 +0,0 @@ -// Unipolar stochastic divider circuit -dtmc - -const double a; -const double b; -const int T; - -// Saturation level for up-down counter -const int MAXCOUNT=63; - -//------------------ -// Signal Sources -//------------------ -module Source0 - inA : [0..1] init 0; - - [event] (inA=0 | inA=1) -> a:(inA'=1) + (1-a):(inA'=0); -endmodule - -// Second signal source: -module Source1 = Source0 [ inA=inB, a=b ] endmodule - - -// AND gate -module AND0 - QB : [0..1] init 0; - - [event] (inB=1)&(Q=1) -> (QB' = 1); - [event] !(inB=1 & Q=1) -> (QB' = 0); -endmodule - - -// Up-Down Counter -module UDC0 - c0: [-MAXCOUNT..MAXCOUNT] init 0; - - [event] (c0 > -MAXCOUNT) & (c0 < MAXCOUNT) -> 1:(c0' = c0 + inA - QB); - [event] (c0 = -MAXCOUNT) -> 1:(c0' = c0 + inA); - [event] (c0 = MAXCOUNT) -> 1:(c0' = c0 - QB); -endmodule - -// Output and Feedback -formula q=(c0+MAXCOUNT+1)/(2*(MAXCOUNT+1)); -module FB0 - Q: [0..1] init 0; - - [event] (c0 >= -MAXCOUNT) & (c0 <= MAXCOUNT) -> q:(Q' = 1) + (1-q):(Q'=0); -endmodule - diff --git a/FaultTolerance/StochasticComputing/divider/divider.props b/FaultTolerance/StochasticComputing/divider/divider.props deleted file mode 100644 index 7ab1358..0000000 --- a/FaultTolerance/StochasticComputing/divider/divider.props +++ /dev/null @@ -1,4 +0,0 @@ -P=? [ F[T,T] Q = 1 ] - -S=? [ Q = 1 ] - diff --git a/FaultTolerance/StochasticComputing/divider/divider_inf.pm b/FaultTolerance/StochasticComputing/divider/divider_inf.pm deleted file mode 100644 index 40b24bd..0000000 --- a/FaultTolerance/StochasticComputing/divider/divider_inf.pm +++ /dev/null @@ -1,54 +0,0 @@ -// Unipolar stochastic divider circuit -dtmc - -const double a; -const double b; -const int T; - -//------------------ -// Signal Sources -//------------------ -module Source0 - inA : [0..1] init 0; - - [event] (inA=0 | inA=1) -> a:(inA'=1) + (1-a):(inA'=0); -endmodule - -// Second signal source: -module Source1 = Source0 [ inA=inB, a=b ] endmodule - - -// AND gate -module AND0 - QB : [0..1] init 0; - - [event] (inB=1)&(Q=1) -> (QB' = 1); - [event] !(inB=1 & Q=1) -> (QB' = 0); -endmodule - - -// Up-Down Counter -module UDC0 - c0: int init 0; - - [event] (true) -> 1:(c0' = c0 + inA - QB); -endmodule - -// Clock Timer -module clockTimer - N: int init 1; - M: int init 1; - - [event] (true) -> 1:(N'=N+1)&(M'=1+round(log(N,2))); -endmodule - - -// Output and Feedback -formula q=(c0+M+1)/(2*(M+1)); -module FB0 - Q: [0..1] init 0; - - [event] (c0 >= -M) & (c0 <= M) -> q:(Q' = 1) + (1-q):(Q'=0); - -endmodule - diff --git a/GeneticCircuits/Circuit0x8E/Circuit0x8E_000to011_G1/Circuit0x8E_000to011.csl b/GeneticCircuits/Circuit0x8E/Circuit0x8E_000to011_G1/Circuit0x8E_000to011.props similarity index 100% rename from GeneticCircuits/Circuit0x8E/Circuit0x8E_000to011_G1/Circuit0x8E_000to011.csl rename to GeneticCircuits/Circuit0x8E/Circuit0x8E_000to011_G1/Circuit0x8E_000to011.props diff --git a/GeneticCircuits/Circuit0x8E/Circuit0x8E_000to011_G1_10_10/Circuit0x8E_G1.csl b/GeneticCircuits/Circuit0x8E/Circuit0x8E_000to011_G1_10_10/Circuit0x8E_G1.props similarity index 100% rename from GeneticCircuits/Circuit0x8E/Circuit0x8E_000to011_G1_10_10/Circuit0x8E_G1.csl rename to GeneticCircuits/Circuit0x8E/Circuit0x8E_000to011_G1_10_10/Circuit0x8E_G1.props diff --git a/GeneticCircuits/Circuit0x8E/Circuit0x8E_000to011_G1_10_10_RBA/Circuit0x8E_G1_RBA.csl b/GeneticCircuits/Circuit0x8E/Circuit0x8E_000to011_G1_10_10_RBA/Circuit0x8E_G1_RBA.props similarity index 100% rename from GeneticCircuits/Circuit0x8E/Circuit0x8E_000to011_G1_10_10_RBA/Circuit0x8E_G1_RBA.csl rename to GeneticCircuits/Circuit0x8E/Circuit0x8E_000to011_G1_10_10_RBA/Circuit0x8E_G1_RBA.props diff --git a/GeneticCircuits/Circuit0x8E/Circuit0x8E_000to101_G1/Circuit0x8E_000to101.csl b/GeneticCircuits/Circuit0x8E/Circuit0x8E_000to101_G1/Circuit0x8E_000to101.props similarity index 100% rename from GeneticCircuits/Circuit0x8E/Circuit0x8E_000to101_G1/Circuit0x8E_000to101.csl rename to GeneticCircuits/Circuit0x8E/Circuit0x8E_000to101_G1/Circuit0x8E_000to101.props diff --git a/GeneticCircuits/Circuit0x8E/Circuit0x8E_000to101_G1_10_10/Circuit0x8E_G1.csl b/GeneticCircuits/Circuit0x8E/Circuit0x8E_000to101_G1_10_10/Circuit0x8E_G1.props similarity index 100% rename from GeneticCircuits/Circuit0x8E/Circuit0x8E_000to101_G1_10_10/Circuit0x8E_G1.csl rename to GeneticCircuits/Circuit0x8E/Circuit0x8E_000to101_G1_10_10/Circuit0x8E_G1.props diff --git a/GeneticCircuits/Circuit0x8E/Circuit0x8E_000to101_G1_10_10_RBA/Circuit0x8E_G1_RBA.csl b/GeneticCircuits/Circuit0x8E/Circuit0x8E_000to101_G1_10_10_RBA/Circuit0x8E_G1_RBA.props similarity index 100% rename from GeneticCircuits/Circuit0x8E/Circuit0x8E_000to101_G1_10_10_RBA/Circuit0x8E_G1_RBA.csl rename to GeneticCircuits/Circuit0x8E/Circuit0x8E_000to101_G1_10_10_RBA/Circuit0x8E_G1_RBA.props diff --git a/GeneticCircuits/Circuit0x8E/Circuit0x8E_010to100_G0/Circuit0x8E_010to100.csl b/GeneticCircuits/Circuit0x8E/Circuit0x8E_010to100_G0/Circuit0x8E_010to100.props similarity index 100% rename from GeneticCircuits/Circuit0x8E/Circuit0x8E_010to100_G0/Circuit0x8E_010to100.csl rename to GeneticCircuits/Circuit0x8E/Circuit0x8E_010to100_G0/Circuit0x8E_010to100.props diff --git a/GeneticCircuits/Circuit0x8E/Circuit0x8E_010to100_G0_10_10/Circuit0x8E_G0.csl b/GeneticCircuits/Circuit0x8E/Circuit0x8E_010to100_G0_10_10/Circuit0x8E_G0.props similarity index 100% rename from GeneticCircuits/Circuit0x8E/Circuit0x8E_010to100_G0_10_10/Circuit0x8E_G0.csl rename to GeneticCircuits/Circuit0x8E/Circuit0x8E_010to100_G0_10_10/Circuit0x8E_G0.props diff --git a/GeneticCircuits/Circuit0x8E/Circuit0x8E_010to100_G0_10_10_RBA/Circuit0x8E_G0_RBA.csl b/GeneticCircuits/Circuit0x8E/Circuit0x8E_010to100_G0_10_10_RBA/Circuit0x8E_G0_RBA.props similarity index 100% rename from GeneticCircuits/Circuit0x8E/Circuit0x8E_010to100_G0_10_10_RBA/Circuit0x8E_G0_RBA.csl rename to GeneticCircuits/Circuit0x8E/Circuit0x8E_010to100_G0_10_10_RBA/Circuit0x8E_G0_RBA.props diff --git a/GeneticCircuits/Circuit0x8E/Circuit0x8E_010to111_G0/Circuit0x8E_010to111.csl b/GeneticCircuits/Circuit0x8E/Circuit0x8E_010to111_G0/Circuit0x8E_010to111.props similarity index 100% rename from GeneticCircuits/Circuit0x8E/Circuit0x8E_010to111_G0/Circuit0x8E_010to111.csl rename to GeneticCircuits/Circuit0x8E/Circuit0x8E_010to111_G0/Circuit0x8E_010to111.props diff --git a/GeneticCircuits/Circuit0x8E/Circuit0x8E_010to111_G0_10_10/Circuit0x8E_G0.csl b/GeneticCircuits/Circuit0x8E/Circuit0x8E_010to111_G0_10_10/Circuit0x8E_G0.props similarity index 100% rename from GeneticCircuits/Circuit0x8E/Circuit0x8E_010to111_G0_10_10/Circuit0x8E_G0.csl rename to GeneticCircuits/Circuit0x8E/Circuit0x8E_010to111_G0_10_10/Circuit0x8E_G0.props diff --git a/GeneticCircuits/Circuit0x8E/Circuit0x8E_010to111_G0_10_10_RBA/Circuit0x8E_G0_RBA.csl b/GeneticCircuits/Circuit0x8E/Circuit0x8E_010to111_G0_10_10_RBA/Circuit0x8E_G0_RBA.props similarity index 100% rename from GeneticCircuits/Circuit0x8E/Circuit0x8E_010to111_G0_10_10_RBA/Circuit0x8E_G0_RBA.csl rename to GeneticCircuits/Circuit0x8E/Circuit0x8E_010to111_G0_10_10_RBA/Circuit0x8E_G0_RBA.props diff --git a/GeneticCircuits/Circuit0x8E/Circuit0x8E_011to000_G1/Circuit0x8E_011to000.csl b/GeneticCircuits/Circuit0x8E/Circuit0x8E_011to000_G1/Circuit0x8E_011to000.props similarity index 100% rename from GeneticCircuits/Circuit0x8E/Circuit0x8E_011to000_G1/Circuit0x8E_011to000.csl rename to GeneticCircuits/Circuit0x8E/Circuit0x8E_011to000_G1/Circuit0x8E_011to000.props diff --git a/GeneticCircuits/Circuit0x8E/Circuit0x8E_011to000_G1_10_10/Circuit0x8E_G1.csl b/GeneticCircuits/Circuit0x8E/Circuit0x8E_011to000_G1_10_10/Circuit0x8E_G1.props similarity index 100% rename from GeneticCircuits/Circuit0x8E/Circuit0x8E_011to000_G1_10_10/Circuit0x8E_G1.csl rename to GeneticCircuits/Circuit0x8E/Circuit0x8E_011to000_G1_10_10/Circuit0x8E_G1.props diff --git a/GeneticCircuits/Circuit0x8E/Circuit0x8E_011to000_G1_10_10_RBA/Circuit0x8E_G1_RBA.csl b/GeneticCircuits/Circuit0x8E/Circuit0x8E_011to000_G1_10_10_RBA/Circuit0x8E_G1_RBA.props similarity index 100% rename from GeneticCircuits/Circuit0x8E/Circuit0x8E_011to000_G1_10_10_RBA/Circuit0x8E_G1_RBA.csl rename to GeneticCircuits/Circuit0x8E/Circuit0x8E_011to000_G1_10_10_RBA/Circuit0x8E_G1_RBA.props diff --git a/GeneticCircuits/Circuit0x8E/Circuit0x8E_011to101_G1/Circuit0x8E_011to101.csl b/GeneticCircuits/Circuit0x8E/Circuit0x8E_011to101_G1/Circuit0x8E_011to101.props similarity index 100% rename from GeneticCircuits/Circuit0x8E/Circuit0x8E_011to101_G1/Circuit0x8E_011to101.csl rename to GeneticCircuits/Circuit0x8E/Circuit0x8E_011to101_G1/Circuit0x8E_011to101.props diff --git a/GeneticCircuits/Circuit0x8E/Circuit0x8E_011to101_G1_10_10/Circuit0x8E_G1.csl b/GeneticCircuits/Circuit0x8E/Circuit0x8E_011to101_G1_10_10/Circuit0x8E_G1.props similarity index 100% rename from GeneticCircuits/Circuit0x8E/Circuit0x8E_011to101_G1_10_10/Circuit0x8E_G1.csl rename to GeneticCircuits/Circuit0x8E/Circuit0x8E_011to101_G1_10_10/Circuit0x8E_G1.props diff --git a/GeneticCircuits/Circuit0x8E/Circuit0x8E_011to101_G1_10_10_RBA/Circuit0x8E_G1_RBA.csl b/GeneticCircuits/Circuit0x8E/Circuit0x8E_011to101_G1_10_10_RBA/Circuit0x8E_G1_RBA.props similarity index 100% rename from GeneticCircuits/Circuit0x8E/Circuit0x8E_011to101_G1_10_10_RBA/Circuit0x8E_G1_RBA.csl rename to GeneticCircuits/Circuit0x8E/Circuit0x8E_011to101_G1_10_10_RBA/Circuit0x8E_G1_RBA.props diff --git a/GeneticCircuits/Circuit0x8E/Circuit0x8E_100to010_G0/Circuit0x8E_100to010.csl b/GeneticCircuits/Circuit0x8E/Circuit0x8E_100to010_G0/Circuit0x8E_100to010.props similarity index 100% rename from GeneticCircuits/Circuit0x8E/Circuit0x8E_100to010_G0/Circuit0x8E_100to010.csl rename to GeneticCircuits/Circuit0x8E/Circuit0x8E_100to010_G0/Circuit0x8E_100to010.props diff --git a/GeneticCircuits/Circuit0x8E/Circuit0x8E_100to010_G0_10_10/Circuit0x8E_G0.csl b/GeneticCircuits/Circuit0x8E/Circuit0x8E_100to010_G0_10_10/Circuit0x8E_G0.props similarity index 100% rename from GeneticCircuits/Circuit0x8E/Circuit0x8E_100to010_G0_10_10/Circuit0x8E_G0.csl rename to GeneticCircuits/Circuit0x8E/Circuit0x8E_100to010_G0_10_10/Circuit0x8E_G0.props diff --git a/GeneticCircuits/Circuit0x8E/Circuit0x8E_100to010_G0_10_10_RBA/Circuit0x8E_G0_RBA.csl b/GeneticCircuits/Circuit0x8E/Circuit0x8E_100to010_G0_10_10_RBA/Circuit0x8E_G0_RBA.props similarity index 100% rename from GeneticCircuits/Circuit0x8E/Circuit0x8E_100to010_G0_10_10_RBA/Circuit0x8E_G0_RBA.csl rename to GeneticCircuits/Circuit0x8E/Circuit0x8E_100to010_G0_10_10_RBA/Circuit0x8E_G0_RBA.props diff --git a/GeneticCircuits/Circuit0x8E/Circuit0x8E_100to111_G0/Circuit0x8E_100to111.csl b/GeneticCircuits/Circuit0x8E/Circuit0x8E_100to111_G0/Circuit0x8E_100to111.props similarity index 100% rename from GeneticCircuits/Circuit0x8E/Circuit0x8E_100to111_G0/Circuit0x8E_100to111.csl rename to GeneticCircuits/Circuit0x8E/Circuit0x8E_100to111_G0/Circuit0x8E_100to111.props diff --git a/GeneticCircuits/Circuit0x8E/Circuit0x8E_100to111_G0_10_10/Circuit0x8E_G0.csl b/GeneticCircuits/Circuit0x8E/Circuit0x8E_100to111_G0_10_10/Circuit0x8E_G0.props similarity index 100% rename from GeneticCircuits/Circuit0x8E/Circuit0x8E_100to111_G0_10_10/Circuit0x8E_G0.csl rename to GeneticCircuits/Circuit0x8E/Circuit0x8E_100to111_G0_10_10/Circuit0x8E_G0.props diff --git a/GeneticCircuits/Circuit0x8E/Circuit0x8E_100to111_G0_10_10_RBA/Circuit0x8E_G0_RBA.csl b/GeneticCircuits/Circuit0x8E/Circuit0x8E_100to111_G0_10_10_RBA/Circuit0x8E_G0_RBA.props similarity index 100% rename from GeneticCircuits/Circuit0x8E/Circuit0x8E_100to111_G0_10_10_RBA/Circuit0x8E_G0_RBA.csl rename to GeneticCircuits/Circuit0x8E/Circuit0x8E_100to111_G0_10_10_RBA/Circuit0x8E_G0_RBA.props diff --git a/GeneticCircuits/Circuit0x8E/Circuit0x8E_101to000_G1/Circuit0x8E_101to000.csl b/GeneticCircuits/Circuit0x8E/Circuit0x8E_101to000_G1/Circuit0x8E_101to000.props similarity index 100% rename from GeneticCircuits/Circuit0x8E/Circuit0x8E_101to000_G1/Circuit0x8E_101to000.csl rename to GeneticCircuits/Circuit0x8E/Circuit0x8E_101to000_G1/Circuit0x8E_101to000.props diff --git a/GeneticCircuits/Circuit0x8E/Circuit0x8E_101to000_G1_10_10/Circuit0x8E_G1.csl b/GeneticCircuits/Circuit0x8E/Circuit0x8E_101to000_G1_10_10/Circuit0x8E_G1.props similarity index 100% rename from GeneticCircuits/Circuit0x8E/Circuit0x8E_101to000_G1_10_10/Circuit0x8E_G1.csl rename to GeneticCircuits/Circuit0x8E/Circuit0x8E_101to000_G1_10_10/Circuit0x8E_G1.props diff --git a/GeneticCircuits/Circuit0x8E/Circuit0x8E_101to000_G1_10_10_RBA/Circuit0x8E_G1_RBA.csl b/GeneticCircuits/Circuit0x8E/Circuit0x8E_101to000_G1_10_10_RBA/Circuit0x8E_G1_RBA.props similarity index 100% rename from GeneticCircuits/Circuit0x8E/Circuit0x8E_101to000_G1_10_10_RBA/Circuit0x8E_G1_RBA.csl rename to GeneticCircuits/Circuit0x8E/Circuit0x8E_101to000_G1_10_10_RBA/Circuit0x8E_G1_RBA.props diff --git a/GeneticCircuits/Circuit0x8E/Circuit0x8E_101to011_G1/Circuit0x8E_101to011.csl b/GeneticCircuits/Circuit0x8E/Circuit0x8E_101to011_G1/Circuit0x8E_101to011.props similarity index 100% rename from GeneticCircuits/Circuit0x8E/Circuit0x8E_101to011_G1/Circuit0x8E_101to011.csl rename to GeneticCircuits/Circuit0x8E/Circuit0x8E_101to011_G1/Circuit0x8E_101to011.props diff --git a/GeneticCircuits/Circuit0x8E/Circuit0x8E_101to011_G1_10_10/Circuit0x8E_G1.csl b/GeneticCircuits/Circuit0x8E/Circuit0x8E_101to011_G1_10_10/Circuit0x8E_G1.props similarity index 100% rename from GeneticCircuits/Circuit0x8E/Circuit0x8E_101to011_G1_10_10/Circuit0x8E_G1.csl rename to GeneticCircuits/Circuit0x8E/Circuit0x8E_101to011_G1_10_10/Circuit0x8E_G1.props diff --git a/GeneticCircuits/Circuit0x8E/Circuit0x8E_101to011_G1_10_10_RBA/Circuit0x8E_G1_RBA.csl b/GeneticCircuits/Circuit0x8E/Circuit0x8E_101to011_G1_10_10_RBA/Circuit0x8E_G1_RBA.props similarity index 100% rename from GeneticCircuits/Circuit0x8E/Circuit0x8E_101to011_G1_10_10_RBA/Circuit0x8E_G1_RBA.csl rename to GeneticCircuits/Circuit0x8E/Circuit0x8E_101to011_G1_10_10_RBA/Circuit0x8E_G1_RBA.props diff --git a/GeneticCircuits/Circuit0x8E/Circuit0x8E_111to010_G0/Circuit0x8E_111to010.csl b/GeneticCircuits/Circuit0x8E/Circuit0x8E_111to010_G0/Circuit0x8E_111to010.props similarity index 100% rename from GeneticCircuits/Circuit0x8E/Circuit0x8E_111to010_G0/Circuit0x8E_111to010.csl rename to GeneticCircuits/Circuit0x8E/Circuit0x8E_111to010_G0/Circuit0x8E_111to010.props diff --git a/GeneticCircuits/Circuit0x8E/Circuit0x8E_111to010_G0_10_10/Circuit0x8E_G0.csl b/GeneticCircuits/Circuit0x8E/Circuit0x8E_111to010_G0_10_10/Circuit0x8E_G0.props similarity index 100% rename from GeneticCircuits/Circuit0x8E/Circuit0x8E_111to010_G0_10_10/Circuit0x8E_G0.csl rename to GeneticCircuits/Circuit0x8E/Circuit0x8E_111to010_G0_10_10/Circuit0x8E_G0.props diff --git a/GeneticCircuits/Circuit0x8E/Circuit0x8E_111to010_G0_10_10_RBA/Circuit0x8E_G0_RBA.csl b/GeneticCircuits/Circuit0x8E/Circuit0x8E_111to010_G0_10_10_RBA/Circuit0x8E_G0_RBA.props similarity index 100% rename from GeneticCircuits/Circuit0x8E/Circuit0x8E_111to010_G0_10_10_RBA/Circuit0x8E_G0_RBA.csl rename to GeneticCircuits/Circuit0x8E/Circuit0x8E_111to010_G0_10_10_RBA/Circuit0x8E_G0_RBA.props diff --git a/GeneticCircuits/Circuit0x8E/Circuit0x8E_111to100_G0/Circuit0x8E_111to100.csl b/GeneticCircuits/Circuit0x8E/Circuit0x8E_111to100_G0/Circuit0x8E_111to100.props similarity index 100% rename from GeneticCircuits/Circuit0x8E/Circuit0x8E_111to100_G0/Circuit0x8E_111to100.csl rename to GeneticCircuits/Circuit0x8E/Circuit0x8E_111to100_G0/Circuit0x8E_111to100.props diff --git a/GeneticCircuits/Circuit0x8E/Circuit0x8E_111to100_G0_10_10/Circuit0x8E_G0.csl b/GeneticCircuits/Circuit0x8E/Circuit0x8E_111to100_G0_10_10/Circuit0x8E_G0.props similarity index 100% rename from GeneticCircuits/Circuit0x8E/Circuit0x8E_111to100_G0_10_10/Circuit0x8E_G0.csl rename to GeneticCircuits/Circuit0x8E/Circuit0x8E_111to100_G0_10_10/Circuit0x8E_G0.props diff --git a/GeneticCircuits/Circuit0x8E/Circuit0x8E_111to100_G0_10_10_RBA/Circuit0x8E_G0_RBA.csl b/GeneticCircuits/Circuit0x8E/Circuit0x8E_111to100_G0_10_10_RBA/Circuit0x8E_G0_RBA.props similarity index 100% rename from GeneticCircuits/Circuit0x8E/Circuit0x8E_111to100_G0_10_10_RBA/Circuit0x8E_G0_RBA.csl rename to GeneticCircuits/Circuit0x8E/Circuit0x8E_111to100_G0_10_10_RBA/Circuit0x8E_G0_RBA.props diff --git a/GeneticCircuits/Circuit0x8E/Circuit0x8E_LHF_000to011_G1/Circuit0x8E_LHF_000to011.csl b/GeneticCircuits/Circuit0x8E/Circuit0x8E_LHF_000to011_G1/Circuit0x8E_LHF_000to011.props similarity index 100% rename from GeneticCircuits/Circuit0x8E/Circuit0x8E_LHF_000to011_G1/Circuit0x8E_LHF_000to011.csl rename to GeneticCircuits/Circuit0x8E/Circuit0x8E_LHF_000to011_G1/Circuit0x8E_LHF_000to011.props diff --git a/GeneticCircuits/Circuit0x8E/Circuit0x8E_LHF_000to011_G1_10_10/Circuit0x8E_LHF_G1.csl b/GeneticCircuits/Circuit0x8E/Circuit0x8E_LHF_000to011_G1_10_10/Circuit0x8E_LHF_G1.props similarity index 100% rename from GeneticCircuits/Circuit0x8E/Circuit0x8E_LHF_000to011_G1_10_10/Circuit0x8E_LHF_G1.csl rename to GeneticCircuits/Circuit0x8E/Circuit0x8E_LHF_000to011_G1_10_10/Circuit0x8E_LHF_G1.props diff --git a/GeneticCircuits/Circuit0x8E/Circuit0x8E_LHF_000to101_G1/Circuit0x8E_LHF_000to101.sm.csl b/GeneticCircuits/Circuit0x8E/Circuit0x8E_LHF_000to101_G1/Circuit0x8E_LHF_000to101.sm.props similarity index 100% rename from GeneticCircuits/Circuit0x8E/Circuit0x8E_LHF_000to101_G1/Circuit0x8E_LHF_000to101.sm.csl rename to GeneticCircuits/Circuit0x8E/Circuit0x8E_LHF_000to101_G1/Circuit0x8E_LHF_000to101.sm.props diff --git a/GeneticCircuits/Circuit0x8E/Circuit0x8E_LHF_000to101_G1_10_10/Circuit0x8E_LHF_G1.csl b/GeneticCircuits/Circuit0x8E/Circuit0x8E_LHF_000to101_G1_10_10/Circuit0x8E_LHF_G1.props similarity index 100% rename from GeneticCircuits/Circuit0x8E/Circuit0x8E_LHF_000to101_G1_10_10/Circuit0x8E_LHF_G1.csl rename to GeneticCircuits/Circuit0x8E/Circuit0x8E_LHF_000to101_G1_10_10/Circuit0x8E_LHF_G1.props diff --git a/GeneticCircuits/Circuit0x8E/Circuit0x8E_LHF_010to100_G0/Circuit0x8E_LHF_010to100.csl b/GeneticCircuits/Circuit0x8E/Circuit0x8E_LHF_010to100_G0/Circuit0x8E_LHF_010to100.props similarity index 100% rename from GeneticCircuits/Circuit0x8E/Circuit0x8E_LHF_010to100_G0/Circuit0x8E_LHF_010to100.csl rename to GeneticCircuits/Circuit0x8E/Circuit0x8E_LHF_010to100_G0/Circuit0x8E_LHF_010to100.props diff --git a/GeneticCircuits/Circuit0x8E/Circuit0x8E_LHF_010to100_G0_10_10/Circuit0x8E_LHF_G0.csl b/GeneticCircuits/Circuit0x8E/Circuit0x8E_LHF_010to100_G0_10_10/Circuit0x8E_LHF_G0.props similarity index 100% rename from GeneticCircuits/Circuit0x8E/Circuit0x8E_LHF_010to100_G0_10_10/Circuit0x8E_LHF_G0.csl rename to GeneticCircuits/Circuit0x8E/Circuit0x8E_LHF_010to100_G0_10_10/Circuit0x8E_LHF_G0.props diff --git a/GeneticCircuits/Circuit0x8E/Circuit0x8E_LHF_010to111_G0/Circuit0x8E_LHF_010to111.csl b/GeneticCircuits/Circuit0x8E/Circuit0x8E_LHF_010to111_G0/Circuit0x8E_LHF_010to111.props similarity index 100% rename from GeneticCircuits/Circuit0x8E/Circuit0x8E_LHF_010to111_G0/Circuit0x8E_LHF_010to111.csl rename to GeneticCircuits/Circuit0x8E/Circuit0x8E_LHF_010to111_G0/Circuit0x8E_LHF_010to111.props diff --git a/GeneticCircuits/Circuit0x8E/Circuit0x8E_LHF_010to111_G0_10_10/Circuit0x8E_LHF_G0.csl b/GeneticCircuits/Circuit0x8E/Circuit0x8E_LHF_010to111_G0_10_10/Circuit0x8E_LHF_G0.props similarity index 100% rename from GeneticCircuits/Circuit0x8E/Circuit0x8E_LHF_010to111_G0_10_10/Circuit0x8E_LHF_G0.csl rename to GeneticCircuits/Circuit0x8E/Circuit0x8E_LHF_010to111_G0_10_10/Circuit0x8E_LHF_G0.props diff --git a/GeneticCircuits/Circuit0x8E/Circuit0x8E_LHF_011to000_G1/Circuit0x8E_LHF_011to000.csl b/GeneticCircuits/Circuit0x8E/Circuit0x8E_LHF_011to000_G1/Circuit0x8E_LHF_011to000.props similarity index 100% rename from GeneticCircuits/Circuit0x8E/Circuit0x8E_LHF_011to000_G1/Circuit0x8E_LHF_011to000.csl rename to GeneticCircuits/Circuit0x8E/Circuit0x8E_LHF_011to000_G1/Circuit0x8E_LHF_011to000.props diff --git a/GeneticCircuits/Circuit0x8E/Circuit0x8E_LHF_011to000_G1_10_10/Circuit0x8E_LHF_G1.csl b/GeneticCircuits/Circuit0x8E/Circuit0x8E_LHF_011to000_G1_10_10/Circuit0x8E_LHF_G1.props similarity index 100% rename from GeneticCircuits/Circuit0x8E/Circuit0x8E_LHF_011to000_G1_10_10/Circuit0x8E_LHF_G1.csl rename to GeneticCircuits/Circuit0x8E/Circuit0x8E_LHF_011to000_G1_10_10/Circuit0x8E_LHF_G1.props diff --git a/GeneticCircuits/Circuit0x8E/Circuit0x8E_LHF_011to101_G1/Circuit0x8E_LHF_011to101.csl b/GeneticCircuits/Circuit0x8E/Circuit0x8E_LHF_011to101_G1/Circuit0x8E_LHF_011to101.props similarity index 100% rename from GeneticCircuits/Circuit0x8E/Circuit0x8E_LHF_011to101_G1/Circuit0x8E_LHF_011to101.csl rename to GeneticCircuits/Circuit0x8E/Circuit0x8E_LHF_011to101_G1/Circuit0x8E_LHF_011to101.props diff --git a/GeneticCircuits/Circuit0x8E/Circuit0x8E_LHF_011to101_G1_10_10/Circuit0x8E_LHF_G1.csl b/GeneticCircuits/Circuit0x8E/Circuit0x8E_LHF_011to101_G1_10_10/Circuit0x8E_LHF_G1.props similarity index 100% rename from GeneticCircuits/Circuit0x8E/Circuit0x8E_LHF_011to101_G1_10_10/Circuit0x8E_LHF_G1.csl rename to GeneticCircuits/Circuit0x8E/Circuit0x8E_LHF_011to101_G1_10_10/Circuit0x8E_LHF_G1.props diff --git a/GeneticCircuits/Circuit0x8E/Circuit0x8E_LHF_100to010_G0/Circuit0x8E_LHF_100to010.csl b/GeneticCircuits/Circuit0x8E/Circuit0x8E_LHF_100to010_G0/Circuit0x8E_LHF_100to010.props similarity index 100% rename from GeneticCircuits/Circuit0x8E/Circuit0x8E_LHF_100to010_G0/Circuit0x8E_LHF_100to010.csl rename to GeneticCircuits/Circuit0x8E/Circuit0x8E_LHF_100to010_G0/Circuit0x8E_LHF_100to010.props diff --git a/GeneticCircuits/Circuit0x8E/Circuit0x8E_LHF_100to010_G0_10_10/Circuit0x8E_LHF_G0.csl b/GeneticCircuits/Circuit0x8E/Circuit0x8E_LHF_100to010_G0_10_10/Circuit0x8E_LHF_G0.props similarity index 100% rename from GeneticCircuits/Circuit0x8E/Circuit0x8E_LHF_100to010_G0_10_10/Circuit0x8E_LHF_G0.csl rename to GeneticCircuits/Circuit0x8E/Circuit0x8E_LHF_100to010_G0_10_10/Circuit0x8E_LHF_G0.props diff --git a/GeneticCircuits/Circuit0x8E/Circuit0x8E_LHF_100to111_G0/Circuit0x8E_LHF_100to111.csl b/GeneticCircuits/Circuit0x8E/Circuit0x8E_LHF_100to111_G0/Circuit0x8E_LHF_100to111.props similarity index 100% rename from GeneticCircuits/Circuit0x8E/Circuit0x8E_LHF_100to111_G0/Circuit0x8E_LHF_100to111.csl rename to GeneticCircuits/Circuit0x8E/Circuit0x8E_LHF_100to111_G0/Circuit0x8E_LHF_100to111.props diff --git a/GeneticCircuits/Circuit0x8E/Circuit0x8E_LHF_100to111_G0_10_10/Circuit0x8E_LHF_G0.csl b/GeneticCircuits/Circuit0x8E/Circuit0x8E_LHF_100to111_G0_10_10/Circuit0x8E_LHF_G0.props similarity index 100% rename from GeneticCircuits/Circuit0x8E/Circuit0x8E_LHF_100to111_G0_10_10/Circuit0x8E_LHF_G0.csl rename to GeneticCircuits/Circuit0x8E/Circuit0x8E_LHF_100to111_G0_10_10/Circuit0x8E_LHF_G0.props diff --git a/GeneticCircuits/Circuit0x8E/Circuit0x8E_LHF_101to000_G1/Circuit0x8E_LHF_101to000.csl b/GeneticCircuits/Circuit0x8E/Circuit0x8E_LHF_101to000_G1/Circuit0x8E_LHF_101to000.props similarity index 100% rename from GeneticCircuits/Circuit0x8E/Circuit0x8E_LHF_101to000_G1/Circuit0x8E_LHF_101to000.csl rename to GeneticCircuits/Circuit0x8E/Circuit0x8E_LHF_101to000_G1/Circuit0x8E_LHF_101to000.props diff --git a/GeneticCircuits/Circuit0x8E/Circuit0x8E_LHF_101to000_G1_10_10/Circuit0x8E_LHF_G1.csl b/GeneticCircuits/Circuit0x8E/Circuit0x8E_LHF_101to000_G1_10_10/Circuit0x8E_LHF_G1.props similarity index 100% rename from GeneticCircuits/Circuit0x8E/Circuit0x8E_LHF_101to000_G1_10_10/Circuit0x8E_LHF_G1.csl rename to GeneticCircuits/Circuit0x8E/Circuit0x8E_LHF_101to000_G1_10_10/Circuit0x8E_LHF_G1.props diff --git a/GeneticCircuits/Circuit0x8E/Circuit0x8E_LHF_101to011_G1/Circuit0x8E_LHF_101to011.csl b/GeneticCircuits/Circuit0x8E/Circuit0x8E_LHF_101to011_G1/Circuit0x8E_LHF_101to011.props similarity index 100% rename from GeneticCircuits/Circuit0x8E/Circuit0x8E_LHF_101to011_G1/Circuit0x8E_LHF_101to011.csl rename to GeneticCircuits/Circuit0x8E/Circuit0x8E_LHF_101to011_G1/Circuit0x8E_LHF_101to011.props diff --git a/GeneticCircuits/Circuit0x8E/Circuit0x8E_LHF_101to011_G1_10_10/Circuit0x8E_LHF_G1.csl b/GeneticCircuits/Circuit0x8E/Circuit0x8E_LHF_101to011_G1_10_10/Circuit0x8E_LHF_G1.props similarity index 100% rename from GeneticCircuits/Circuit0x8E/Circuit0x8E_LHF_101to011_G1_10_10/Circuit0x8E_LHF_G1.csl rename to GeneticCircuits/Circuit0x8E/Circuit0x8E_LHF_101to011_G1_10_10/Circuit0x8E_LHF_G1.props diff --git a/GeneticCircuits/Circuit0x8E/Circuit0x8E_LHF_111to010_G0/Circuit0x8E_LHF_111to010.csl b/GeneticCircuits/Circuit0x8E/Circuit0x8E_LHF_111to010_G0/Circuit0x8E_LHF_111to010.props similarity index 100% rename from GeneticCircuits/Circuit0x8E/Circuit0x8E_LHF_111to010_G0/Circuit0x8E_LHF_111to010.csl rename to GeneticCircuits/Circuit0x8E/Circuit0x8E_LHF_111to010_G0/Circuit0x8E_LHF_111to010.props diff --git a/GeneticCircuits/Circuit0x8E/Circuit0x8E_LHF_111to010_G0_10_10/Circuit0x8E_LHF_G0.csl b/GeneticCircuits/Circuit0x8E/Circuit0x8E_LHF_111to010_G0_10_10/Circuit0x8E_LHF_G0.props similarity index 100% rename from GeneticCircuits/Circuit0x8E/Circuit0x8E_LHF_111to010_G0_10_10/Circuit0x8E_LHF_G0.csl rename to GeneticCircuits/Circuit0x8E/Circuit0x8E_LHF_111to010_G0_10_10/Circuit0x8E_LHF_G0.props diff --git a/GeneticCircuits/Circuit0x8E/Circuit0x8E_LHF_111to100_G0/Circuit0x8E_LHF_111to100.csl b/GeneticCircuits/Circuit0x8E/Circuit0x8E_LHF_111to100_G0/Circuit0x8E_LHF_111to100.props similarity index 100% rename from GeneticCircuits/Circuit0x8E/Circuit0x8E_LHF_111to100_G0/Circuit0x8E_LHF_111to100.csl rename to GeneticCircuits/Circuit0x8E/Circuit0x8E_LHF_111to100_G0/Circuit0x8E_LHF_111to100.props diff --git a/GeneticCircuits/Circuit0x8E/Circuit0x8E_LHF_111to100_G0_10_10/Circuit0x8E_LHF_G0.csl b/GeneticCircuits/Circuit0x8E/Circuit0x8E_LHF_111to100_G0_10_10/Circuit0x8E_LHF_G0.props similarity index 100% rename from GeneticCircuits/Circuit0x8E/Circuit0x8E_LHF_111to100_G0_10_10/Circuit0x8E_LHF_G0.csl rename to GeneticCircuits/Circuit0x8E/Circuit0x8E_LHF_111to100_G0_10_10/Circuit0x8E_LHF_G0.props diff --git a/GeneticCircuits/Circuit0x8E/Circuit0x8E_TI_000to011_G1/Circuit0x8E_TI_000to011.csl b/GeneticCircuits/Circuit0x8E/Circuit0x8E_TI_000to011_G1/Circuit0x8E_TI_000to011.props similarity index 100% rename from GeneticCircuits/Circuit0x8E/Circuit0x8E_TI_000to011_G1/Circuit0x8E_TI_000to011.csl rename to GeneticCircuits/Circuit0x8E/Circuit0x8E_TI_000to011_G1/Circuit0x8E_TI_000to011.props diff --git a/GeneticCircuits/Circuit0x8E/Circuit0x8E_TI_000to011_G1_10_10/Circuit0x8E_TI_G1.csl b/GeneticCircuits/Circuit0x8E/Circuit0x8E_TI_000to011_G1_10_10/Circuit0x8E_TI_G1.props similarity index 100% rename from GeneticCircuits/Circuit0x8E/Circuit0x8E_TI_000to011_G1_10_10/Circuit0x8E_TI_G1.csl rename to GeneticCircuits/Circuit0x8E/Circuit0x8E_TI_000to011_G1_10_10/Circuit0x8E_TI_G1.props diff --git a/GeneticCircuits/Circuit0x8E/Circuit0x8E_TI_000to101_G1/Circuit0x8E_TI_000to101.csl b/GeneticCircuits/Circuit0x8E/Circuit0x8E_TI_000to101_G1/Circuit0x8E_TI_000to101.props similarity index 100% rename from GeneticCircuits/Circuit0x8E/Circuit0x8E_TI_000to101_G1/Circuit0x8E_TI_000to101.csl rename to GeneticCircuits/Circuit0x8E/Circuit0x8E_TI_000to101_G1/Circuit0x8E_TI_000to101.props diff --git a/GeneticCircuits/Circuit0x8E/Circuit0x8E_TI_000to101_G1_10_10/Circuit0x8E_TI_G1.csl b/GeneticCircuits/Circuit0x8E/Circuit0x8E_TI_000to101_G1_10_10/Circuit0x8E_TI_G1.props similarity index 100% rename from GeneticCircuits/Circuit0x8E/Circuit0x8E_TI_000to101_G1_10_10/Circuit0x8E_TI_G1.csl rename to GeneticCircuits/Circuit0x8E/Circuit0x8E_TI_000to101_G1_10_10/Circuit0x8E_TI_G1.props diff --git a/GeneticCircuits/Circuit0x8E/Circuit0x8E_TI_010to000_G1/Circuit0x8E_TI_011to000.csl b/GeneticCircuits/Circuit0x8E/Circuit0x8E_TI_010to000_G1/Circuit0x8E_TI_011to000.props similarity index 100% rename from GeneticCircuits/Circuit0x8E/Circuit0x8E_TI_010to000_G1/Circuit0x8E_TI_011to000.csl rename to GeneticCircuits/Circuit0x8E/Circuit0x8E_TI_010to000_G1/Circuit0x8E_TI_011to000.props diff --git a/GeneticCircuits/Circuit0x8E/Circuit0x8E_TI_010to100_G0/Circuit0x8E_TI_010to100.csl b/GeneticCircuits/Circuit0x8E/Circuit0x8E_TI_010to100_G0/Circuit0x8E_TI_010to100.props similarity index 100% rename from GeneticCircuits/Circuit0x8E/Circuit0x8E_TI_010to100_G0/Circuit0x8E_TI_010to100.csl rename to GeneticCircuits/Circuit0x8E/Circuit0x8E_TI_010to100_G0/Circuit0x8E_TI_010to100.props diff --git a/GeneticCircuits/Circuit0x8E/Circuit0x8E_TI_010to100_G0_10_10/Circuit0x8E_TI_G0csl.csl b/GeneticCircuits/Circuit0x8E/Circuit0x8E_TI_010to100_G0_10_10/Circuit0x8E_TI_G0csl.props similarity index 100% rename from GeneticCircuits/Circuit0x8E/Circuit0x8E_TI_010to100_G0_10_10/Circuit0x8E_TI_G0csl.csl rename to GeneticCircuits/Circuit0x8E/Circuit0x8E_TI_010to100_G0_10_10/Circuit0x8E_TI_G0csl.props diff --git a/GeneticCircuits/Circuit0x8E/Circuit0x8E_TI_010to101_G1/Circuit0x8E_TI_011to101.csl b/GeneticCircuits/Circuit0x8E/Circuit0x8E_TI_010to101_G1/Circuit0x8E_TI_011to101.props similarity index 100% rename from GeneticCircuits/Circuit0x8E/Circuit0x8E_TI_010to101_G1/Circuit0x8E_TI_011to101.csl rename to GeneticCircuits/Circuit0x8E/Circuit0x8E_TI_010to101_G1/Circuit0x8E_TI_011to101.props diff --git a/GeneticCircuits/Circuit0x8E/Circuit0x8E_TI_010to111_G0/Circuit0x8E_TI_010to111.csl b/GeneticCircuits/Circuit0x8E/Circuit0x8E_TI_010to111_G0/Circuit0x8E_TI_010to111.props similarity index 100% rename from GeneticCircuits/Circuit0x8E/Circuit0x8E_TI_010to111_G0/Circuit0x8E_TI_010to111.csl rename to GeneticCircuits/Circuit0x8E/Circuit0x8E_TI_010to111_G0/Circuit0x8E_TI_010to111.props diff --git a/GeneticCircuits/Circuit0x8E/Circuit0x8E_TI_010to111_G0_10_10/Circuit0x8E_TI_G0csl.csl b/GeneticCircuits/Circuit0x8E/Circuit0x8E_TI_010to111_G0_10_10/Circuit0x8E_TI_G0csl.props similarity index 100% rename from GeneticCircuits/Circuit0x8E/Circuit0x8E_TI_010to111_G0_10_10/Circuit0x8E_TI_G0csl.csl rename to GeneticCircuits/Circuit0x8E/Circuit0x8E_TI_010to111_G0_10_10/Circuit0x8E_TI_G0csl.props diff --git a/GeneticCircuits/Circuit0x8E/Circuit0x8E_TI_011to000_G1_10_10/Circuit0x8E_TI_G1.csl b/GeneticCircuits/Circuit0x8E/Circuit0x8E_TI_011to000_G1_10_10/Circuit0x8E_TI_G1.props similarity index 100% rename from GeneticCircuits/Circuit0x8E/Circuit0x8E_TI_011to000_G1_10_10/Circuit0x8E_TI_G1.csl rename to GeneticCircuits/Circuit0x8E/Circuit0x8E_TI_011to000_G1_10_10/Circuit0x8E_TI_G1.props diff --git a/GeneticCircuits/Circuit0x8E/Circuit0x8E_TI_011to101_G1_10_10/Circuit0x8E_TI_G1.csl b/GeneticCircuits/Circuit0x8E/Circuit0x8E_TI_011to101_G1_10_10/Circuit0x8E_TI_G1.props similarity index 100% rename from GeneticCircuits/Circuit0x8E/Circuit0x8E_TI_011to101_G1_10_10/Circuit0x8E_TI_G1.csl rename to GeneticCircuits/Circuit0x8E/Circuit0x8E_TI_011to101_G1_10_10/Circuit0x8E_TI_G1.props diff --git a/GeneticCircuits/Circuit0x8E/Circuit0x8E_TI_100to010_G0/Circuit0x8E_TI_100to010.csl b/GeneticCircuits/Circuit0x8E/Circuit0x8E_TI_100to010_G0/Circuit0x8E_TI_100to010.props similarity index 100% rename from GeneticCircuits/Circuit0x8E/Circuit0x8E_TI_100to010_G0/Circuit0x8E_TI_100to010.csl rename to GeneticCircuits/Circuit0x8E/Circuit0x8E_TI_100to010_G0/Circuit0x8E_TI_100to010.props diff --git a/GeneticCircuits/Circuit0x8E/Circuit0x8E_TI_100to010_G0_10_10/Circuit0x8E_TI_G0csl.csl b/GeneticCircuits/Circuit0x8E/Circuit0x8E_TI_100to010_G0_10_10/Circuit0x8E_TI_G0csl.props similarity index 100% rename from GeneticCircuits/Circuit0x8E/Circuit0x8E_TI_100to010_G0_10_10/Circuit0x8E_TI_G0csl.csl rename to GeneticCircuits/Circuit0x8E/Circuit0x8E_TI_100to010_G0_10_10/Circuit0x8E_TI_G0csl.props diff --git a/GeneticCircuits/Circuit0x8E/Circuit0x8E_TI_100to111_G0/Circuit0x8E_TI_100to111.csl b/GeneticCircuits/Circuit0x8E/Circuit0x8E_TI_100to111_G0/Circuit0x8E_TI_100to111.props similarity index 100% rename from GeneticCircuits/Circuit0x8E/Circuit0x8E_TI_100to111_G0/Circuit0x8E_TI_100to111.csl rename to GeneticCircuits/Circuit0x8E/Circuit0x8E_TI_100to111_G0/Circuit0x8E_TI_100to111.props diff --git a/GeneticCircuits/Circuit0x8E/Circuit0x8E_TI_100to111_G0_10_10/Circuit0x8E_TI_G0csl.csl b/GeneticCircuits/Circuit0x8E/Circuit0x8E_TI_100to111_G0_10_10/Circuit0x8E_TI_G0csl.props similarity index 100% rename from GeneticCircuits/Circuit0x8E/Circuit0x8E_TI_100to111_G0_10_10/Circuit0x8E_TI_G0csl.csl rename to GeneticCircuits/Circuit0x8E/Circuit0x8E_TI_100to111_G0_10_10/Circuit0x8E_TI_G0csl.props diff --git a/GeneticCircuits/Circuit0x8E/Circuit0x8E_TI_101to000_G1/Circuit0x8E_TI_101to000.csl b/GeneticCircuits/Circuit0x8E/Circuit0x8E_TI_101to000_G1/Circuit0x8E_TI_101to000.props similarity index 100% rename from GeneticCircuits/Circuit0x8E/Circuit0x8E_TI_101to000_G1/Circuit0x8E_TI_101to000.csl rename to GeneticCircuits/Circuit0x8E/Circuit0x8E_TI_101to000_G1/Circuit0x8E_TI_101to000.props diff --git a/GeneticCircuits/Circuit0x8E/Circuit0x8E_TI_101to000_G1_10_10/Circuit0x8E_TI_101to000_G1_10_10.csl b/GeneticCircuits/Circuit0x8E/Circuit0x8E_TI_101to000_G1_10_10/Circuit0x8E_TI_101to000_G1_10_10.props similarity index 100% rename from GeneticCircuits/Circuit0x8E/Circuit0x8E_TI_101to000_G1_10_10/Circuit0x8E_TI_101to000_G1_10_10.csl rename to GeneticCircuits/Circuit0x8E/Circuit0x8E_TI_101to000_G1_10_10/Circuit0x8E_TI_101to000_G1_10_10.props diff --git a/GeneticCircuits/Circuit0x8E/Circuit0x8E_TI_101to011_G1/Circuit0x8E_TI_101to011.csl b/GeneticCircuits/Circuit0x8E/Circuit0x8E_TI_101to011_G1/Circuit0x8E_TI_101to011.props similarity index 100% rename from GeneticCircuits/Circuit0x8E/Circuit0x8E_TI_101to011_G1/Circuit0x8E_TI_101to011.csl rename to GeneticCircuits/Circuit0x8E/Circuit0x8E_TI_101to011_G1/Circuit0x8E_TI_101to011.props diff --git a/GeneticCircuits/Circuit0x8E/Circuit0x8E_TI_101to011_G1_10_10/Circuit0x8E_TI_101to011_G1_10_10.csl b/GeneticCircuits/Circuit0x8E/Circuit0x8E_TI_101to011_G1_10_10/Circuit0x8E_TI_101to011_G1_10_10.props similarity index 100% rename from GeneticCircuits/Circuit0x8E/Circuit0x8E_TI_101to011_G1_10_10/Circuit0x8E_TI_101to011_G1_10_10.csl rename to GeneticCircuits/Circuit0x8E/Circuit0x8E_TI_101to011_G1_10_10/Circuit0x8E_TI_101to011_G1_10_10.props diff --git a/GeneticCircuits/Circuit0x8E/Circuit0x8E_TI_111to010_G0/Circuit0x8E_TI_111to010.csl b/GeneticCircuits/Circuit0x8E/Circuit0x8E_TI_111to010_G0/Circuit0x8E_TI_111to010.props similarity index 100% rename from GeneticCircuits/Circuit0x8E/Circuit0x8E_TI_111to010_G0/Circuit0x8E_TI_111to010.csl rename to GeneticCircuits/Circuit0x8E/Circuit0x8E_TI_111to010_G0/Circuit0x8E_TI_111to010.props diff --git a/GeneticCircuits/Circuit0x8E/Circuit0x8E_TI_111to010_G0_10_10/Circuit0x8E_TI_G0csl.csl b/GeneticCircuits/Circuit0x8E/Circuit0x8E_TI_111to010_G0_10_10/Circuit0x8E_TI_G0csl.props similarity index 100% rename from GeneticCircuits/Circuit0x8E/Circuit0x8E_TI_111to010_G0_10_10/Circuit0x8E_TI_G0csl.csl rename to GeneticCircuits/Circuit0x8E/Circuit0x8E_TI_111to010_G0_10_10/Circuit0x8E_TI_G0csl.props diff --git a/GeneticCircuits/Circuit0x8E/Circuit0x8E_TI_111to100_G0/Circuit0x8E_TI_111to100.csl b/GeneticCircuits/Circuit0x8E/Circuit0x8E_TI_111to100_G0/Circuit0x8E_TI_111to100.props similarity index 100% rename from GeneticCircuits/Circuit0x8E/Circuit0x8E_TI_111to100_G0/Circuit0x8E_TI_111to100.csl rename to GeneticCircuits/Circuit0x8E/Circuit0x8E_TI_111to100_G0/Circuit0x8E_TI_111to100.props diff --git a/GeneticCircuits/Circuit0x8E/Circuit0x8E_TI_111to100_G0_10_10/Circuit0x8E_TI_G0csl.csl b/GeneticCircuits/Circuit0x8E/Circuit0x8E_TI_111to100_G0_10_10/Circuit0x8E_TI_G0csl.props similarity index 100% rename from GeneticCircuits/Circuit0x8E/Circuit0x8E_TI_111to100_G0_10_10/Circuit0x8E_TI_G0csl.csl rename to GeneticCircuits/Circuit0x8E/Circuit0x8E_TI_111to100_G0_10_10/Circuit0x8E_TI_G0csl.props diff --git a/GeneticCircuits/Dual_Feedback_Osscillator/Default/Dual_Feedback_Oscillator.sm b/GeneticCircuits/Dual_Feedback_Osscillator/Dual_Feedback_Oscillator.sm similarity index 100% rename from GeneticCircuits/Dual_Feedback_Osscillator/Default/Dual_Feedback_Oscillator.sm rename to GeneticCircuits/Dual_Feedback_Osscillator/Dual_Feedback_Oscillator.sm diff --git a/GeneticCircuits/Dual_Feedback_Osscillator/Default/Dual_Feedback_Oscillator.xml b/GeneticCircuits/Dual_Feedback_Osscillator/Dual_Feedback_Oscillator.xml similarity index 100% rename from GeneticCircuits/Dual_Feedback_Osscillator/Default/Dual_Feedback_Oscillator.xml rename to GeneticCircuits/Dual_Feedback_Osscillator/Dual_Feedback_Oscillator.xml diff --git a/GeneticCircuits/Repressilator/Default/Repressilator.sm b/GeneticCircuits/Repressilator/Repressilator.sm similarity index 100% rename from GeneticCircuits/Repressilator/Default/Repressilator.sm rename to GeneticCircuits/Repressilator/Repressilator.sm diff --git a/GeneticCircuits/Repressilator/Default/Repressilator.xml b/GeneticCircuits/Repressilator/Repressilator.xml similarity index 100% rename from GeneticCircuits/Repressilator/Default/Repressilator.xml rename to GeneticCircuits/Repressilator/Repressilator.xml diff --git a/GeneticCircuits/Toggle_Switch/Default/Toggle_Switch.props b/GeneticCircuits/Toggle_Switch/Default/Toggle_Switch.props deleted file mode 100644 index 87ad135..0000000 --- a/GeneticCircuits/Toggle_Switch/Default/Toggle_Switch.props +++ /dev/null @@ -1,4 +0,0 @@ -// File generated by SBML-to-PRISM converter -// Original file: Toggle_Switch.xml -// @GeneticLogicLab - diff --git a/GeneticCircuits/Toggle_Switch/Default/Toggle_Switch.sm b/GeneticCircuits/Toggle_Switch/Default/Toggle_Switch.sm deleted file mode 100644 index e913ff0..0000000 --- a/GeneticCircuits/Toggle_Switch/Default/Toggle_Switch.sm +++ /dev/null @@ -1,199 +0,0 @@ -// File generated by SBML-to-PRISM converter -// Original file: Toggle_Switch.xml -// @GeneticLogicLab - -ctmc - -// Compartment size -const double Cell = 1.0; - -// Model parameters -const double kd = 0.0075; // Degradation rate -const double kc_f = 0.05; // Forward complex formation rate -const double kc_r = 1.0; // Reverse complex formation rate -const double nc = 2.0; // Stoichiometry of binding -const double topModell_Part2_module_sub__kr_f = 0.5; // Forward repression binding rate -const double topModell_Part2_module_sub__kr_r = 1.0; // Reverse repression binding rate -const double topModell_Part2_module_sub__ka_f = 0.0033; // Forward activation binding rate -const double topModell_Part2_module_sub__ka_r = 1.0; // Reverse activation binding rate -const double topModell_Part2_module_sub__ko_f = 0.033; // Forward RNAP binding rate -const double topModell_Part2_module_sub__ko_r = 1.0; // Reverse RNAP binding rate -const double topModell_Part2_module_sub__kao_f = 1.0; // Forward activated RNAP binding rate -const double topModell_Part2_module_sub__kao_r = 1.0; // Reverse activated RNAP binding rate -const double topModell_Part2_module_sub__nc = 2.0; // Stoichiometry of binding -const double topModell_Part2_module_sub__nr = 30.0; // Initial RNAP count -const double topModell_Part2_module_sub__ko = 0.05; // Open complex production rate -const double topModell_Part2_module_sub__kb = 1.0E-4; // Basal production rate -const double topModell_Part2_module_sub__ng = 2.0; // Initial promoter count -const double topModell_Part2_module_sub__np = 10.0; // Stoichiometry of production -const double topModell_Part2_module_sub__ka = 0.25; // Activated production rate -const double topModell_Part1_module_sub__kr_f = 0.5; // Forward repression binding rate -const double topModell_Part1_module_sub__kr_r = 1.0; // Reverse repression binding rate -const double topModell_Part1_module_sub__ka_f = 0.0033; // Forward activation binding rate -const double topModell_Part1_module_sub__ka_r = 1.0; // Reverse activation binding rate -const double topModell_Part1_module_sub__ko_f = 0.033; // Forward RNAP binding rate -const double topModell_Part1_module_sub__ko_r = 1.0; // Reverse RNAP binding rate -const double topModell_Part1_module_sub__kao_f = 1.0; // Forward activated RNAP binding rate -const double topModell_Part1_module_sub__kao_r = 1.0; // Reverse activated RNAP binding rate -const double topModell_Part1_module_sub__nc = 2.0; // Stoichiometry of binding -const double topModell_Part1_module_sub__nr = 30.0; // Initial RNAP count -const double topModell_Part1_module_sub__ko = 0.05; // Open complex production rate -const double topModell_Part1_module_sub__kb = 1.0E-4; // Basal production rate -const double topModell_Part1_module_sub__ng = 2.0; // Initial promoter count -const double topModell_Part1_module_sub__np = 10.0; // Stoichiometry of production -const double topModell_Part1_module_sub__ka = 0.25; // Activated production rate - -// Species IPTG -module IPTG - - IPTG : int init 0; - - // Complex_IPTG_LacI_protein - [Complex_IPTG_LacI_protein] IPTG > 0 -> (IPTG' = IPTG - 2); - -endmodule - -// Species aTc -module aTc - - aTc : int init 0; - - // Complex_aTc_TetR_protein - [Complex_aTc_TetR_protein] aTc > 0 -> (aTc' = aTc - 2); - -endmodule - -// Species YFP_protein -module YFP_protein - - YFP_protein : int init 0; - - // Degradation_YFP_protein - [Degradation_YFP_protein] YFP_protein > 0 -> (YFP_protein' = YFP_protein - 1); - // R_abstracted_production_topModell_Part2_module_sub__Part2_fc - [R_abstracted_production_topModell_Part2_module_sub__Part2_fc] YFP_protein > 0 -> (YFP_protein' = YFP_protein + 10); - -endmodule - -// Species aTc_TetR_protein -module aTc_TetR_protein - - aTc_TetR_protein : int init 0; - - // Degradation_aTc_TetR_protein - [Degradation_aTc_TetR_protein] aTc_TetR_protein > 0 -> (aTc_TetR_protein' = aTc_TetR_protein - 1); - // Complex_aTc_TetR_protein - [Complex_aTc_TetR_protein] aTc_TetR_protein > 0 -> (aTc_TetR_protein' = aTc_TetR_protein + 1); - -endmodule - -// Species LacI_protein -module LacI_protein - - LacI_protein : int init 0; - - // Degradation_LacI_protein - [Degradation_LacI_protein] LacI_protein > 0 -> (LacI_protein' = LacI_protein - 1); - // R_abstracted_production_topModell_Part2_module_sub__Part2_fc - [R_abstracted_production_topModell_Part2_module_sub__Part2_fc] LacI_protein > 0 -> (LacI_protein' = LacI_protein + 10); - // Complex_IPTG_LacI_protein - [Complex_IPTG_LacI_protein] LacI_protein > 0 -> (LacI_protein' = LacI_protein - 2); - -endmodule - -// Species IPTG_LacI_protein -module IPTG_LacI_protein - - IPTG_LacI_protein : int init 0; - - // Degradation_IPTG_LacI_protein - [Degradation_IPTG_LacI_protein] IPTG_LacI_protein > 0 -> (IPTG_LacI_protein' = IPTG_LacI_protein - 1); - // Complex_IPTG_LacI_protein - [Complex_IPTG_LacI_protein] IPTG_LacI_protein > 0 -> (IPTG_LacI_protein' = IPTG_LacI_protein + 1); - -endmodule - -// Species TetR_protein -module TetR_protein - - TetR_protein : int init 60; - - // Degradation_TetR_protein - [Degradation_TetR_protein] TetR_protein > 0 -> (TetR_protein' = TetR_protein - 1); - // R_abstracted_production_topModell_Part1_module_sub__Part1_fc - [R_abstracted_production_topModell_Part1_module_sub__Part1_fc] TetR_protein > 0 -> (TetR_protein' = TetR_protein + 10); - // Complex_aTc_TetR_protein - [Complex_aTc_TetR_protein] TetR_protein > 0 -> (TetR_protein' = TetR_protein - 2); - -endmodule - -// Species topModell_Part2_module_sub__Part2_fc -module topModell_Part2_module_sub__Part2_fc - - topModell_Part2_module_sub__Part2_fc : int init 2; - - -endmodule - -// Species topModell_Part1_module_sub__Part1_fc -module topModell_Part1_module_sub__Part1_fc - - topModell_Part1_module_sub__Part1_fc : int init 2; - - -endmodule - -// Reaction rates -module reaction_rates - - // Degradation_aTc_TetR_protein: -> aTc_TetR_protein -> - [Degradation_aTc_TetR_protein] (kd * aTc_TetR_protein) > 0 -> (kd * aTc_TetR_protein) : true; - - // Degradation_YFP_protein: -> YFP_protein -> - [Degradation_YFP_protein] (kd * YFP_protein) > 0 -> (kd * YFP_protein) : true; - - // Degradation_LacI_protein: -> LacI_protein -> - [Degradation_LacI_protein] (kd * LacI_protein) > 0 -> (kd * LacI_protein) : true; - - // Degradation_IPTG_LacI_protein: -> IPTG_LacI_protein -> - [Degradation_IPTG_LacI_protein] (kd * IPTG_LacI_protein) > 0 -> (kd * IPTG_LacI_protein) : true; - - // Degradation_TetR_protein: -> TetR_protein -> - [Degradation_TetR_protein] (kd * TetR_protein) > 0 -> (kd * TetR_protein) : true; - - // R_abstracted_production_topModell_Part1_module_sub__Part1_fc: -> -> -TetR_protein - [R_abstracted_production_topModell_Part1_module_sub__Part1_fc] (((ko__topModell_Part1_module_sub__Part1_fc * ng__topModell_Part1_module_sub__Part1_fc) * (Ko__topModell_Part1_module_sub__Part1_fc * RNAP)) / ((1 + (Ko__topModell_Part1_module_sub__Part1_fc * RNAP)) + pow((Kr__LacI_protein_topModell_Part1_module_sub__Part1_fc * LacI_protein) , nc__LacI_protein_topModell_Part1_module_sub__Part1_fc))) > 0 -> (((ko__topModell_Part1_module_sub__Part1_fc * ng__topModell_Part1_module_sub__Part1_fc) * (Ko__topModell_Part1_module_sub__Part1_fc * RNAP)) / ((1 + (Ko__topModell_Part1_module_sub__Part1_fc * RNAP)) + pow((Kr__LacI_protein_topModell_Part1_module_sub__Part1_fc * LacI_protein) , nc__LacI_protein_topModell_Part1_module_sub__Part1_fc))) : true; - - // R_abstracted_production_topModell_Part2_module_sub__Part2_fc: -> -> -YFP_protein + -LacI_protein - [R_abstracted_production_topModell_Part2_module_sub__Part2_fc] (((ko__topModell_Part2_module_sub__Part2_fc * ng__topModell_Part2_module_sub__Part2_fc) * (Ko__topModell_Part2_module_sub__Part2_fc * RNAP)) / ((1 + (Ko__topModell_Part2_module_sub__Part2_fc * RNAP)) + pow((Kr__TetR_protein_topModell_Part2_module_sub__Part2_fc * TetR_protein) , nc__TetR_protein_topModell_Part2_module_sub__Part2_fc))) > 0 -> (((ko__topModell_Part2_module_sub__Part2_fc * ng__topModell_Part2_module_sub__Part2_fc) * (Ko__topModell_Part2_module_sub__Part2_fc * RNAP)) / ((1 + (Ko__topModell_Part2_module_sub__Part2_fc * RNAP)) + pow((Kr__TetR_protein_topModell_Part2_module_sub__Part2_fc * TetR_protein) , nc__TetR_protein_topModell_Part2_module_sub__Part2_fc))) : true; - - // Complex_aTc_TetR_protein: -> aTc + TetR_protein -> aTc_TetR_protein - [Complex_aTc_TetR_protein] ((((kf_c * pow(Kc , ((nc__aTc_aTc_TetR_protein + nc__TetR_protein_aTc_TetR_protein) - 2))) * pow(aTc , nc__aTc_aTc_TetR_protein)) * pow(TetR_protein , nc__TetR_protein_aTc_TetR_protein)) - (kr_c * aTc_TetR_protein)) > 0 -> ((((kf_c * pow(Kc , ((nc__aTc_aTc_TetR_protein + nc__TetR_protein_aTc_TetR_protein) - 2))) * pow(aTc , nc__aTc_aTc_TetR_protein)) * pow(TetR_protein , nc__TetR_protein_aTc_TetR_protein)) - (kr_c * aTc_TetR_protein)) : true; - - // Complex_IPTG_LacI_protein: -> IPTG + LacI_protein -> IPTG_LacI_protein - [Complex_IPTG_LacI_protein] ((((kf_c * pow(Kc , ((nc__IPTG_IPTG_LacI_protein + nc__LacI_protein_IPTG_LacI_protein) - 2))) * pow(IPTG , nc__IPTG_IPTG_LacI_protein)) * pow(LacI_protein , nc__LacI_protein_IPTG_LacI_protein)) - (kr_c * IPTG_LacI_protein)) > 0 -> ((((kf_c * pow(Kc , ((nc__IPTG_IPTG_LacI_protein + nc__LacI_protein_IPTG_LacI_protein) - 2))) * pow(IPTG , nc__IPTG_IPTG_LacI_protein)) * pow(LacI_protein , nc__LacI_protein_IPTG_LacI_protein)) - (kr_c * IPTG_LacI_protein)) : true; - -endmodule - -// Reward structures (one per species) -// Reward 1: IPTG -rewards "IPTG" true : IPTG; endrewards -// Reward 2: aTc -rewards "aTc" true : aTc; endrewards -// Reward 3: YFP_protein -rewards "YFP_protein" true : YFP_protein; endrewards -// Reward 4: aTc_TetR_protein -rewards "aTc_TetR_protein" true : aTc_TetR_protein; endrewards -// Reward 5: LacI_protein -rewards "LacI_protein" true : LacI_protein; endrewards -// Reward 6: IPTG_LacI_protein -rewards "IPTG_LacI_protein" true : IPTG_LacI_protein; endrewards -// Reward 7: TetR_protein -rewards "TetR_protein" true : TetR_protein; endrewards -// Reward 8: topModell_Part2_module_sub__Part2_fc -rewards "topModell_Part2_module_sub__Part2_fc" true : topModell_Part2_module_sub__Part2_fc; endrewards -// Reward 9: topModell_Part1_module_sub__Part1_fc -rewards "topModell_Part1_module_sub__Part1_fc" true : topModell_Part1_module_sub__Part1_fc; endrewards diff --git a/GeneticCircuits/Toggle_Switch/Default/Toggle_Switch.xml b/GeneticCircuits/Toggle_Switch/Default/Toggle_Switch.xml deleted file mode 100644 index 4b3cc68..0000000 --- a/GeneticCircuits/Toggle_Switch/Default/Toggle_Switch.xml +++ /dev/null @@ -1,1186 +0,0 @@ - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - + - - - - - - - - - - - - - - - - - - - - - + - - - - - - - - - - - - - - - - - - - - - + - - - - - - - - - - - - - - - - - - - - - + - - - - - - - - - - - - - - - - - - - - - + - - - - - - - - - - - - - - - - - - - - - + - - - - - - - - - - - - - - - - - - - - - + - - - - - - - - - - - - - - - - - - - - - - - - - - + - - - - - - - - - - - - - - - - - - - - - - - - - - + - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - kd - aTc_TetR_protein - - - - - - - - - - - - - - - - kd - YFP_protein - - - - - - - - - - - - - - - - kd - LacI_protein - - - - - - - - - - - - - - - - kd - IPTG_LacI_protein - - - - - - - - - - - - - - - - kd - TetR_protein - - - - - - - - - - - - - - - - - - - - - - - ko__topModell_Part1_module_sub__Part1_fc - ng__topModell_Part1_module_sub__Part1_fc - - - - Ko__topModell_Part1_module_sub__Part1_fc - RNAP - - - - - - - 1 - - - Ko__topModell_Part1_module_sub__Part1_fc - RNAP - - - - - - - Kr__LacI_protein_topModell_Part1_module_sub__Part1_fc - LacI_protein - - nc__LacI_protein_topModell_Part1_module_sub__Part1_fc - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - ko__topModell_Part2_module_sub__Part2_fc - ng__topModell_Part2_module_sub__Part2_fc - - - - Ko__topModell_Part2_module_sub__Part2_fc - RNAP - - - - - - - 1 - - - Ko__topModell_Part2_module_sub__Part2_fc - RNAP - - - - - - - Kr__TetR_protein_topModell_Part2_module_sub__Part2_fc - TetR_protein - - nc__TetR_protein_topModell_Part2_module_sub__Part2_fc - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - kf_c - - - Kc - - - - - nc__aTc_aTc_TetR_protein - nc__TetR_protein_aTc_TetR_protein - - 2 - - - - - - aTc - nc__aTc_aTc_TetR_protein - - - - - TetR_protein - nc__TetR_protein_aTc_TetR_protein - - - - - kr_c - aTc_TetR_protein - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - kf_c - - - Kc - - - - - nc__IPTG_IPTG_LacI_protein - nc__LacI_protein_IPTG_LacI_protein - - 2 - - - - - - IPTG - nc__IPTG_IPTG_LacI_protein - - - - - LacI_protein - nc__LacI_protein_IPTG_LacI_protein - - - - - kr_c - IPTG_LacI_protein - - - - - - - - - - - - - - - - - - - - - - - 2000 - - - - - - 60 - - - - - - - - - - - - - 4000 - - - - - - 0 - - - - - - - - - - - - - 6000 - - - - - - 60 - - - - - - - - - - - - - 8000 - - - - - - 0 - - - - - - - diff --git a/GeneticCircuits/Toggle_Switch/Default/jsbml.log b/GeneticCircuits/Toggle_Switch/Default/jsbml.log deleted file mode 100644 index d568ccc..0000000 --- a/GeneticCircuits/Toggle_Switch/Default/jsbml.log +++ /dev/null @@ -1,130 +0,0 @@ -2023-02-02 12:06:16,124 ERROR o.s.j.x.p.SBMLCoreParser [main] Property substanceUnits is not defined in model for Level 2 and Version 2. -2023-02-02 12:06:16,125 INFO o.s.j.x.p.SBMLCoreParser [main] Attribute = substanceUnits, value 'mole' , element name = model -2023-02-02 12:06:16,126 WARN o.s.j.x.p.SBMLCoreParser [main] Could not recognize the attribute 'substanceUnits' on the element model. Please check the specification for SBML. -2023-02-02 12:06:16,127 ERROR o.s.j.x.p.SBMLCoreParser [main] Property volumeUnits is not defined in model for Level 2 and Version 2. -2023-02-02 12:06:16,128 INFO o.s.j.x.p.SBMLCoreParser [main] Attribute = volumeUnits, value 'litre' , element name = model -2023-02-02 12:06:16,128 WARN o.s.j.x.p.SBMLCoreParser [main] Could not recognize the attribute 'volumeUnits' on the element model. Please check the specification for SBML. -2023-02-02 12:06:16,129 WARN o.s.j.x.p.XMLNodeReader [main] The type of String '' on the element 'annotation' is unknown! Some data might be lost -2023-02-02 12:06:16,171 WARN o.s.j.x.p.XMLNodeReader [main] The type of String '' on the element 'annotation' is unknown! Some data might be lost -2023-02-02 12:06:16,172 WARN o.s.j.x.p.XMLNodeReader [main] The type of String '' on the element 'annotation' is unknown! Some data might be lost -2023-02-02 12:06:16,173 WARN o.s.j.x.p.XMLNodeReader [main] The type of String '' on the element 'annotation' is unknown! Some data might be lost -2023-02-02 12:06:16,175 WARN o.s.j.x.p.XMLNodeReader [main] The type of String '' on the element 'annotation' is unknown! Some data might be lost -2023-02-02 12:06:16,176 WARN o.s.j.x.p.XMLNodeReader [main] The type of String '' on the element 'annotation' is unknown! Some data might be lost -2023-02-02 12:06:16,177 WARN o.s.j.x.p.XMLNodeReader [main] The type of String '' on the element 'annotation' is unknown! Some data might be lost -2023-02-02 12:06:16,178 WARN o.s.j.x.p.XMLNodeReader [main] The type of String '' on the element 'annotation' is unknown! Some data might be lost -2023-02-02 12:06:16,221 WARN o.s.j.x.p.XMLNodeReader [main] The type of String '' on the element 'annotation' is unknown! Some data might be lost -2023-02-02 12:06:16,222 WARN o.s.j.x.p.XMLNodeReader [main] The type of String '' on the element 'annotation' is unknown! Some data might be lost -2023-02-02 12:06:16,228 ERROR o.s.j.x.p.SBMLCoreParser [main] Property compartment is not defined in reaction for Level 2 and Version 2. -2023-02-02 12:06:16,229 INFO o.s.j.x.p.SBMLCoreParser [main] Attribute = compartment, value 'Cell' , element name = reaction -2023-02-02 12:06:16,229 WARN o.s.j.x.p.SBMLCoreParser [main] Could not recognize the attribute 'compartment' on the element reaction. Please check the specification for SBML. -2023-02-02 12:06:16,230 ERROR o.s.j.x.p.SBMLCoreParser [main] Property constant is not defined in speciesReference for Level 2 and Version 2. -2023-02-02 12:06:16,230 INFO o.s.j.x.p.SBMLCoreParser [main] Attribute = constant, value 'true' , element name = speciesReference -2023-02-02 12:06:16,231 WARN o.s.j.x.p.SBMLCoreParser [main] Could not recognize the attribute 'constant' on the element speciesReference. Please check the specification for SBML. -2023-02-02 12:06:16,235 WARN o.s.j.x.p.SBMLCoreParser [main] The element 'listOfLocalParameters' is not recognized. -2023-02-02 12:06:16,236 ERROR o.s.j.x.p.SBMLCoreParser [main] Property compartment is not defined in reaction for Level 2 and Version 2. -2023-02-02 12:06:16,236 INFO o.s.j.x.p.SBMLCoreParser [main] Attribute = compartment, value 'Cell' , element name = reaction -2023-02-02 12:06:16,236 WARN o.s.j.x.p.SBMLCoreParser [main] Could not recognize the attribute 'compartment' on the element reaction. Please check the specification for SBML. -2023-02-02 12:06:16,237 ERROR o.s.j.x.p.SBMLCoreParser [main] Property constant is not defined in speciesReference for Level 2 and Version 2. -2023-02-02 12:06:16,237 INFO o.s.j.x.p.SBMLCoreParser [main] Attribute = constant, value 'true' , element name = speciesReference -2023-02-02 12:06:16,237 WARN o.s.j.x.p.SBMLCoreParser [main] Could not recognize the attribute 'constant' on the element speciesReference. Please check the specification for SBML. -2023-02-02 12:06:16,238 WARN o.s.j.x.p.SBMLCoreParser [main] The element 'listOfLocalParameters' is not recognized. -2023-02-02 12:06:16,239 ERROR o.s.j.x.p.SBMLCoreParser [main] Property compartment is not defined in reaction for Level 2 and Version 2. -2023-02-02 12:06:16,239 INFO o.s.j.x.p.SBMLCoreParser [main] Attribute = compartment, value 'Cell' , element name = reaction -2023-02-02 12:06:16,240 WARN o.s.j.x.p.SBMLCoreParser [main] Could not recognize the attribute 'compartment' on the element reaction. Please check the specification for SBML. -2023-02-02 12:06:16,240 ERROR o.s.j.x.p.SBMLCoreParser [main] Property constant is not defined in speciesReference for Level 2 and Version 2. -2023-02-02 12:06:16,241 INFO o.s.j.x.p.SBMLCoreParser [main] Attribute = constant, value 'true' , element name = speciesReference -2023-02-02 12:06:16,241 WARN o.s.j.x.p.SBMLCoreParser [main] Could not recognize the attribute 'constant' on the element speciesReference. Please check the specification for SBML. -2023-02-02 12:06:16,241 WARN o.s.j.x.p.SBMLCoreParser [main] The element 'listOfLocalParameters' is not recognized. -2023-02-02 12:06:16,242 ERROR o.s.j.x.p.SBMLCoreParser [main] Property compartment is not defined in reaction for Level 2 and Version 2. -2023-02-02 12:06:16,242 INFO o.s.j.x.p.SBMLCoreParser [main] Attribute = compartment, value 'Cell' , element name = reaction -2023-02-02 12:06:16,242 WARN o.s.j.x.p.SBMLCoreParser [main] Could not recognize the attribute 'compartment' on the element reaction. Please check the specification for SBML. -2023-02-02 12:06:16,243 ERROR o.s.j.x.p.SBMLCoreParser [main] Property constant is not defined in speciesReference for Level 2 and Version 2. -2023-02-02 12:06:16,243 INFO o.s.j.x.p.SBMLCoreParser [main] Attribute = constant, value 'true' , element name = speciesReference -2023-02-02 12:06:16,243 WARN o.s.j.x.p.SBMLCoreParser [main] Could not recognize the attribute 'constant' on the element speciesReference. Please check the specification for SBML. -2023-02-02 12:06:16,244 WARN o.s.j.x.p.SBMLCoreParser [main] The element 'listOfLocalParameters' is not recognized. -2023-02-02 12:06:16,244 ERROR o.s.j.x.p.SBMLCoreParser [main] Property compartment is not defined in reaction for Level 2 and Version 2. -2023-02-02 12:06:16,244 INFO o.s.j.x.p.SBMLCoreParser [main] Attribute = compartment, value 'Cell' , element name = reaction -2023-02-02 12:06:16,244 WARN o.s.j.x.p.SBMLCoreParser [main] Could not recognize the attribute 'compartment' on the element reaction. Please check the specification for SBML. -2023-02-02 12:06:16,245 ERROR o.s.j.x.p.SBMLCoreParser [main] Property constant is not defined in speciesReference for Level 2 and Version 2. -2023-02-02 12:06:16,245 INFO o.s.j.x.p.SBMLCoreParser [main] Attribute = constant, value 'true' , element name = speciesReference -2023-02-02 12:06:16,245 WARN o.s.j.x.p.SBMLCoreParser [main] Could not recognize the attribute 'constant' on the element speciesReference. Please check the specification for SBML. -2023-02-02 12:06:16,246 WARN o.s.j.x.p.SBMLCoreParser [main] The element 'listOfLocalParameters' is not recognized. -2023-02-02 12:06:16,246 ERROR o.s.j.x.p.SBMLCoreParser [main] Property compartment is not defined in reaction for Level 2 and Version 2. -2023-02-02 12:06:16,246 INFO o.s.j.x.p.SBMLCoreParser [main] Attribute = compartment, value 'Cell' , element name = reaction -2023-02-02 12:06:16,246 WARN o.s.j.x.p.SBMLCoreParser [main] Could not recognize the attribute 'compartment' on the element reaction. Please check the specification for SBML. -2023-02-02 12:06:16,247 ERROR o.s.j.x.p.SBMLCoreParser [main] Property constant is not defined in speciesReference for Level 2 and Version 2. -2023-02-02 12:06:16,247 INFO o.s.j.x.p.SBMLCoreParser [main] Attribute = constant, value 'true' , element name = speciesReference -2023-02-02 12:06:16,247 WARN o.s.j.x.p.SBMLCoreParser [main] Could not recognize the attribute 'constant' on the element speciesReference. Please check the specification for SBML. -2023-02-02 12:06:16,249 WARN o.s.j.x.p.SBMLCoreParser [main] The element 'listOfLocalParameters' is not recognized. -2023-02-02 12:06:16,250 ERROR o.s.j.x.p.SBMLCoreParser [main] Property compartment is not defined in reaction for Level 2 and Version 2. -2023-02-02 12:06:16,250 INFO o.s.j.x.p.SBMLCoreParser [main] Attribute = compartment, value 'Cell' , element name = reaction -2023-02-02 12:06:16,250 WARN o.s.j.x.p.SBMLCoreParser [main] Could not recognize the attribute 'compartment' on the element reaction. Please check the specification for SBML. -2023-02-02 12:06:16,251 ERROR o.s.j.x.p.SBMLCoreParser [main] Property constant is not defined in speciesReference for Level 2 and Version 2. -2023-02-02 12:06:16,251 INFO o.s.j.x.p.SBMLCoreParser [main] Attribute = constant, value 'true' , element name = speciesReference -2023-02-02 12:06:16,251 WARN o.s.j.x.p.SBMLCoreParser [main] Could not recognize the attribute 'constant' on the element speciesReference. Please check the specification for SBML. -2023-02-02 12:06:16,252 ERROR o.s.j.x.p.SBMLCoreParser [main] Property constant is not defined in speciesReference for Level 2 and Version 2. -2023-02-02 12:06:16,252 INFO o.s.j.x.p.SBMLCoreParser [main] Attribute = constant, value 'true' , element name = speciesReference -2023-02-02 12:06:16,252 WARN o.s.j.x.p.SBMLCoreParser [main] Could not recognize the attribute 'constant' on the element speciesReference. Please check the specification for SBML. -2023-02-02 12:06:16,254 WARN o.s.j.x.p.SBMLCoreParser [main] The element 'listOfLocalParameters' is not recognized. -2023-02-02 12:06:16,255 ERROR o.s.j.x.p.SBMLCoreParser [main] Property compartment is not defined in reaction for Level 2 and Version 2. -2023-02-02 12:06:16,255 INFO o.s.j.x.p.SBMLCoreParser [main] Attribute = compartment, value 'Cell' , element name = reaction -2023-02-02 12:06:16,255 WARN o.s.j.x.p.SBMLCoreParser [main] Could not recognize the attribute 'compartment' on the element reaction. Please check the specification for SBML. -2023-02-02 12:06:16,255 ERROR o.s.j.x.p.SBMLCoreParser [main] Property constant is not defined in speciesReference for Level 2 and Version 2. -2023-02-02 12:06:16,256 INFO o.s.j.x.p.SBMLCoreParser [main] Attribute = constant, value 'true' , element name = speciesReference -2023-02-02 12:06:16,256 WARN o.s.j.x.p.SBMLCoreParser [main] Could not recognize the attribute 'constant' on the element speciesReference. Please check the specification for SBML. -2023-02-02 12:06:16,256 ERROR o.s.j.x.p.SBMLCoreParser [main] Property constant is not defined in speciesReference for Level 2 and Version 2. -2023-02-02 12:06:16,256 INFO o.s.j.x.p.SBMLCoreParser [main] Attribute = constant, value 'true' , element name = speciesReference -2023-02-02 12:06:16,256 WARN o.s.j.x.p.SBMLCoreParser [main] Could not recognize the attribute 'constant' on the element speciesReference. Please check the specification for SBML. -2023-02-02 12:06:16,257 ERROR o.s.j.x.p.SBMLCoreParser [main] Property constant is not defined in speciesReference for Level 2 and Version 2. -2023-02-02 12:06:16,257 INFO o.s.j.x.p.SBMLCoreParser [main] Attribute = constant, value 'true' , element name = speciesReference -2023-02-02 12:06:16,257 WARN o.s.j.x.p.SBMLCoreParser [main] Could not recognize the attribute 'constant' on the element speciesReference. Please check the specification for SBML. -2023-02-02 12:06:16,258 WARN o.s.j.x.p.SBMLCoreParser [main] The element 'listOfLocalParameters' is not recognized. -2023-02-02 12:06:16,259 ERROR o.s.j.x.p.SBMLCoreParser [main] Property compartment is not defined in reaction for Level 2 and Version 2. -2023-02-02 12:06:16,259 INFO o.s.j.x.p.SBMLCoreParser [main] Attribute = compartment, value 'Cell' , element name = reaction -2023-02-02 12:06:16,259 WARN o.s.j.x.p.SBMLCoreParser [main] Could not recognize the attribute 'compartment' on the element reaction. Please check the specification for SBML. -2023-02-02 12:06:16,259 ERROR o.s.j.x.p.SBMLCoreParser [main] Property constant is not defined in speciesReference for Level 2 and Version 2. -2023-02-02 12:06:16,259 INFO o.s.j.x.p.SBMLCoreParser [main] Attribute = constant, value 'true' , element name = speciesReference -2023-02-02 12:06:16,260 WARN o.s.j.x.p.SBMLCoreParser [main] Could not recognize the attribute 'constant' on the element speciesReference. Please check the specification for SBML. -2023-02-02 12:06:16,260 ERROR o.s.j.x.p.SBMLCoreParser [main] Property constant is not defined in speciesReference for Level 2 and Version 2. -2023-02-02 12:06:16,260 INFO o.s.j.x.p.SBMLCoreParser [main] Attribute = constant, value 'true' , element name = speciesReference -2023-02-02 12:06:16,260 WARN o.s.j.x.p.SBMLCoreParser [main] Could not recognize the attribute 'constant' on the element speciesReference. Please check the specification for SBML. -2023-02-02 12:06:16,261 ERROR o.s.j.x.p.SBMLCoreParser [main] Property constant is not defined in speciesReference for Level 2 and Version 2. -2023-02-02 12:06:16,261 INFO o.s.j.x.p.SBMLCoreParser [main] Attribute = constant, value 'true' , element name = speciesReference -2023-02-02 12:06:16,261 WARN o.s.j.x.p.SBMLCoreParser [main] Could not recognize the attribute 'constant' on the element speciesReference. Please check the specification for SBML. -2023-02-02 12:06:16,262 WARN o.s.j.x.p.SBMLCoreParser [main] The element 'listOfLocalParameters' is not recognized. -2023-02-02 12:06:16,263 ERROR o.s.j.x.p.SBMLCoreParser [main] Property useValuesFromTriggerTime is not defined in event for Level 2 and Version 2. -2023-02-02 12:06:16,263 INFO o.s.j.x.p.SBMLCoreParser [main] Attribute = useValuesFromTriggerTime, value 'false' , element name = event -2023-02-02 12:06:16,263 WARN o.s.j.x.p.SBMLCoreParser [main] Could not recognize the attribute 'useValuesFromTriggerTime' on the element event. Please check the specification for SBML. -2023-02-02 12:06:16,264 ERROR o.s.j.x.p.SBMLCoreParser [main] Property initialValue is not defined in trigger for Level 2 and Version 2. -2023-02-02 12:06:16,264 INFO o.s.j.x.p.SBMLCoreParser [main] Attribute = initialValue, value 'false' , element name = trigger -2023-02-02 12:06:16,264 WARN o.s.j.x.p.SBMLCoreParser [main] Could not recognize the attribute 'initialValue' on the element trigger. Please check the specification for SBML. -2023-02-02 12:06:16,265 ERROR o.s.j.x.p.SBMLCoreParser [main] Property persistent is not defined in trigger for Level 2 and Version 2. -2023-02-02 12:06:16,265 INFO o.s.j.x.p.SBMLCoreParser [main] Attribute = persistent, value 'false' , element name = trigger -2023-02-02 12:06:16,265 WARN o.s.j.x.p.SBMLCoreParser [main] Could not recognize the attribute 'persistent' on the element trigger. Please check the specification for SBML. -2023-02-02 12:06:16,266 ERROR o.s.j.x.p.SBMLCoreParser [main] Property useValuesFromTriggerTime is not defined in event for Level 2 and Version 2. -2023-02-02 12:06:16,266 INFO o.s.j.x.p.SBMLCoreParser [main] Attribute = useValuesFromTriggerTime, value 'false' , element name = event -2023-02-02 12:06:16,266 WARN o.s.j.x.p.SBMLCoreParser [main] Could not recognize the attribute 'useValuesFromTriggerTime' on the element event. Please check the specification for SBML. -2023-02-02 12:06:16,267 ERROR o.s.j.x.p.SBMLCoreParser [main] Property initialValue is not defined in trigger for Level 2 and Version 2. -2023-02-02 12:06:16,267 INFO o.s.j.x.p.SBMLCoreParser [main] Attribute = initialValue, value 'false' , element name = trigger -2023-02-02 12:06:16,267 WARN o.s.j.x.p.SBMLCoreParser [main] Could not recognize the attribute 'initialValue' on the element trigger. Please check the specification for SBML. -2023-02-02 12:06:16,267 ERROR o.s.j.x.p.SBMLCoreParser [main] Property persistent is not defined in trigger for Level 2 and Version 2. -2023-02-02 12:06:16,267 INFO o.s.j.x.p.SBMLCoreParser [main] Attribute = persistent, value 'false' , element name = trigger -2023-02-02 12:06:16,267 WARN o.s.j.x.p.SBMLCoreParser [main] Could not recognize the attribute 'persistent' on the element trigger. Please check the specification for SBML. -2023-02-02 12:06:16,268 ERROR o.s.j.x.p.SBMLCoreParser [main] Property useValuesFromTriggerTime is not defined in event for Level 2 and Version 2. -2023-02-02 12:06:16,268 INFO o.s.j.x.p.SBMLCoreParser [main] Attribute = useValuesFromTriggerTime, value 'false' , element name = event -2023-02-02 12:06:16,268 WARN o.s.j.x.p.SBMLCoreParser [main] Could not recognize the attribute 'useValuesFromTriggerTime' on the element event. Please check the specification for SBML. -2023-02-02 12:06:16,269 ERROR o.s.j.x.p.SBMLCoreParser [main] Property initialValue is not defined in trigger for Level 2 and Version 2. -2023-02-02 12:06:16,269 INFO o.s.j.x.p.SBMLCoreParser [main] Attribute = initialValue, value 'false' , element name = trigger -2023-02-02 12:06:16,269 WARN o.s.j.x.p.SBMLCoreParser [main] Could not recognize the attribute 'initialValue' on the element trigger. Please check the specification for SBML. -2023-02-02 12:06:16,269 ERROR o.s.j.x.p.SBMLCoreParser [main] Property persistent is not defined in trigger for Level 2 and Version 2. -2023-02-02 12:06:16,269 INFO o.s.j.x.p.SBMLCoreParser [main] Attribute = persistent, value 'false' , element name = trigger -2023-02-02 12:06:16,269 WARN o.s.j.x.p.SBMLCoreParser [main] Could not recognize the attribute 'persistent' on the element trigger. Please check the specification for SBML. -2023-02-02 12:06:16,270 ERROR o.s.j.x.p.SBMLCoreParser [main] Property useValuesFromTriggerTime is not defined in event for Level 2 and Version 2. -2023-02-02 12:06:16,270 INFO o.s.j.x.p.SBMLCoreParser [main] Attribute = useValuesFromTriggerTime, value 'false' , element name = event -2023-02-02 12:06:16,270 WARN o.s.j.x.p.SBMLCoreParser [main] Could not recognize the attribute 'useValuesFromTriggerTime' on the element event. Please check the specification for SBML. -2023-02-02 12:06:16,271 ERROR o.s.j.x.p.SBMLCoreParser [main] Property initialValue is not defined in trigger for Level 2 and Version 2. -2023-02-02 12:06:16,271 INFO o.s.j.x.p.SBMLCoreParser [main] Attribute = initialValue, value 'false' , element name = trigger -2023-02-02 12:06:16,271 WARN o.s.j.x.p.SBMLCoreParser [main] Could not recognize the attribute 'initialValue' on the element trigger. Please check the specification for SBML. -2023-02-02 12:06:16,271 ERROR o.s.j.x.p.SBMLCoreParser [main] Property persistent is not defined in trigger for Level 2 and Version 2. -2023-02-02 12:06:16,271 INFO o.s.j.x.p.SBMLCoreParser [main] Attribute = persistent, value 'false' , element name = trigger -2023-02-02 12:06:16,271 WARN o.s.j.x.p.SBMLCoreParser [main] Could not recognize the attribute 'persistent' on the element trigger. Please check the specification for SBML. diff --git a/GeneticCircuits/Toggle_Switch/RBA/Toggle_Switch_RBA.props b/GeneticCircuits/Toggle_Switch/RBA/Toggle_Switch_RBA.props deleted file mode 100644 index dab0e7a..0000000 --- a/GeneticCircuits/Toggle_Switch/RBA/Toggle_Switch_RBA.props +++ /dev/null @@ -1,4 +0,0 @@ -// File generated by SBML-to-PRISM converter -// Original file: Toggle_Switch_RBA.xml -// @GeneticLogicLab - diff --git a/GeneticCircuits/Toggle_Switch/RBA/Toggle_Switch_RBA.sm b/GeneticCircuits/Toggle_Switch/RBA/Toggle_Switch_RBA.sm deleted file mode 100644 index 2119e38..0000000 --- a/GeneticCircuits/Toggle_Switch/RBA/Toggle_Switch_RBA.sm +++ /dev/null @@ -1,183 +0,0 @@ -// File generated by SBML-to-PRISM converter -// Original file: Toggle_Switch_RBA.xml -// @GeneticLogicLab - -ctmc - -// Compartment size -const double Cell = 1.0; - -// Model parameters -const double kd = 0.0075; // Degradation rate -const double kc_f = 0.05; // Forward complex formation rate -const double kc_r = 1.0; // Reverse complex formation rate -const double nc = 2.0; // Stoichiometry of binding -const double kr_f = 0.5; // Forward repression binding rate -const double kr_r = 1.0; // Reverse repression binding rate -const double ka_f = 0.0033; // Forward activation binding rate -const double ka_r = 1.0; // Reverse activation binding rate -const double ko_f = 0.033; // Forward RNAP binding rate -const double ko_r = 1.0; // Reverse RNAP binding rate -const double kao_f = 1.0; // Forward activated RNAP binding rate -const double kao_r = 1.0; // Reverse activated RNAP binding rate -const double nr = 30.0; // Initial RNAP count -const double ko = 0.05; // Open complex production rate -const double kb = 1.0E-4; // Basal production rate -const double ng = 2.0; // Initial promoter count -const double np = 10.0; // Stoichiometry of production -const double ka = 0.25; // Activated production rate - -// Species P1 -module P1 - - P1 : int init 2; - - -endmodule - -// Species IPTG -module IPTG - - IPTG : int init 0; - - // Complex_C1 - [Complex_C1] IPTG > 0 -> (IPTG' = IPTG - 1); - -endmodule - -// Species aTc -module aTc - - aTc : int init 0; - - // Complex_C2 - [Complex_C2] aTc > 0 -> (aTc' = aTc - 1); - -endmodule - -// Species TetR -module TetR - - TetR : int init 0; - - // Degradation_TetR - [Degradation_TetR] TetR > 0 -> (TetR' = TetR - 1); - // Complex_C2 - [Complex_C2] TetR > 0 -> (TetR' = TetR - 1); - // Production_P1 - [Production_P1] TetR > 0 -> (TetR' = TetR + 10); - -endmodule - -// Species GFP -module GFP - - GFP : int init 0; - - // Degradation_GFP - [Degradation_GFP] GFP > 0 -> (GFP' = GFP - 1); - // Production_P1 - [Production_P1] GFP > 0 -> (GFP' = GFP + 10); - -endmodule - -// Species P2 -module P2 - - P2 : int init 2; - - -endmodule - -// Species C1 -module C1 - - C1 : int init 0; - - // Degradation_C1 - [Degradation_C1] C1 > 0 -> (C1' = C1 - 1); - // Complex_C1 - [Complex_C1] C1 > 0 -> (C1' = C1 + 1); - -endmodule - -// Species C2 -module C2 - - C2 : int init 0; - - // Degradation_C2 - [Degradation_C2] C2 > 0 -> (C2' = C2 - 1); - // Complex_C2 - [Complex_C2] C2 > 0 -> (C2' = C2 + 1); - -endmodule - -// Species LacI -module LacI - - LacI : int init 0; - - // Degradation_LacI - [Degradation_LacI] LacI > 0 -> (LacI' = LacI - 1); - // Complex_C1 - [Complex_C1] LacI > 0 -> (LacI' = LacI - 1); - // Production_P2 - [Production_P2] LacI > 0 -> (LacI' = LacI + 10); - -endmodule - -// Reaction rates -module reaction_rates - - // Degradation_TetR: -> TetR -> - [Degradation_TetR] (kd * TetR) > 0 -> (kd * TetR) : true; - - // Degradation_GFP: -> GFP -> - [Degradation_GFP] (kd * GFP) > 0 -> (kd * GFP) : true; - - // Degradation_C2: -> C2 -> - [Degradation_C2] (kd * C2) > 0 -> (kd * C2) : true; - - // Degradation_LacI: -> LacI -> - [Degradation_LacI] (kd * LacI) > 0 -> (kd * LacI) : true; - - // Degradation_C1: -> C1 -> - [Degradation_C1] (kd * C1) > 0 -> (kd * C1) : true; - - // Complex_C1: -> IPTG + LacI -> C1 - [Complex_C1] (((kc_f * pow(IPTG , nc_IPTG)) * pow(LacI , nc_LacI)) - (kc_r * C1)) > 0 -> (((kc_f * pow(IPTG , nc_IPTG)) * pow(LacI , nc_LacI)) - (kc_r * C1)) : true; - - // Complex_C2: -> aTc + TetR -> C2 - [Complex_C2] (((kc_f * pow(aTc , nc_aTc)) * pow(TetR , nc_TetR)) - (kc_r * C2)) > 0 -> (((kc_f * pow(aTc , nc_aTc)) * pow(TetR , nc_TetR)) - (kc_r * C2)) : true; - - // Production_P1: -> -> -GFP + -TetR - [Production_P1] (((((P1 * ko) * ko_f) / ko_r) * nr) / ((1 + ((ko_f / ko_r) * nr)) + pow(((kr_f / kr_r) * LacI) , nc))) > 0 -> (((((P1 * ko) * ko_f) / ko_r) * nr) / ((1 + ((ko_f / ko_r) * nr)) + pow(((kr_f / kr_r) * LacI) , nc))) : true; - - // Production_P2: -> -> -LacI - [Production_P2] (((((P2 * ko) * ko_f) / ko_r) * nr) / ((1 + ((ko_f / ko_r) * nr)) + pow(((kr_f / kr_r) * TetR) , nc))) > 0 -> (((((P2 * ko) * ko_f) / ko_r) * nr) / ((1 + ((ko_f / ko_r) * nr)) + pow(((kr_f / kr_r) * TetR) , nc))) : true; - -endmodule - -// Reward structures (one per species) -// Reward 1: P1 -rewards "P1" true : P1; endrewards -// Reward 2: IPTG -rewards "IPTG" true : IPTG; endrewards -// Reward 3: aTc -rewards "aTc" true : aTc; endrewards -// Reward 4: TetR -rewards "TetR" true : TetR; endrewards -// Reward 5: GFP -rewards "GFP" true : GFP; endrewards -// Reward 6: P2 -rewards "P2" true : P2; endrewards -// Reward 7: C1 -rewards "C1" true : C1; endrewards -// Reward 8: C2 -rewards "C2" true : C2; endrewards -// Reward 9: LacI -rewards "LacI" true : LacI; endrewards diff --git a/GeneticCircuits/Toggle_Switch/RBA/Toggle_Switch_RBA.xml b/GeneticCircuits/Toggle_Switch/RBA/Toggle_Switch_RBA.xml deleted file mode 100644 index 73a0998..0000000 --- a/GeneticCircuits/Toggle_Switch/RBA/Toggle_Switch_RBA.xml +++ /dev/null @@ -1,798 +0,0 @@ - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - kd - TetR - - - - - - - - - - - - - kd - GFP - - - - - - - - - - - - - kd - C2 - - - - - - - - - - - - - kd - LacI - - - - - - - - - - - - - kd - C1 - - - - - - - - - - - - - - - - - - - - - kc_f - - - IPTG - nc_IPTG - - - - - LacI - nc_LacI - - - - - kc_r - C1 - - - - - - - - - - - - - - - - - - - - - - - - - - kc_f - - - aTc - nc_aTc - - - - - TetR - nc_TetR - - - - - kc_r - C2 - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - P1 - ko - - ko_f - - ko_r - - nr - - - - - - 1 - - - - - ko_f - ko_r - - nr - - - - - - - - - kr_f - kr_r - - LacI - - nc - - - - - - - - - - - - - - - - - - - - - - - - - - - P2 - ko - - ko_f - - ko_r - - nr - - - - - - 1 - - - - - ko_f - ko_r - - nr - - - - - - - - - kr_f - kr_r - - TetR - - nc - - - - - - - - - - - - - - t - 500 - - - - - - - 60 - - - - - - - - - - t - 1500 - - - - - - - 0 - - - - - - - - - - t - 2000 - - - - - - - 60 - - - - - - - - - - t - 3000 - - - - - - - 0 - - - - - - - diff --git a/GeneticCircuits/Toggle_Switch/RBA/jsbml.log b/GeneticCircuits/Toggle_Switch/RBA/jsbml.log deleted file mode 100644 index 8bda126..0000000 --- a/GeneticCircuits/Toggle_Switch/RBA/jsbml.log +++ /dev/null @@ -1,107 +0,0 @@ -2023-02-02 12:08:21,958 ERROR o.s.j.x.p.SBMLCoreParser [main] Property compartment is not defined in reaction for Level 2 and Version 1. -2023-02-02 12:08:21,960 INFO o.s.j.x.p.SBMLCoreParser [main] Attribute = compartment, value 'Cell' , element name = reaction -2023-02-02 12:08:21,960 WARN o.s.j.x.p.SBMLCoreParser [main] Could not recognize the attribute 'compartment' on the element reaction. Please check the specification for SBML. -2023-02-02 12:08:21,962 ERROR o.s.j.x.p.SBMLCoreParser [main] Property constant is not defined in speciesReference for Level 2 and Version 1. -2023-02-02 12:08:21,963 INFO o.s.j.x.p.SBMLCoreParser [main] Attribute = constant, value 'true' , element name = speciesReference -2023-02-02 12:08:21,963 WARN o.s.j.x.p.SBMLCoreParser [main] Could not recognize the attribute 'constant' on the element speciesReference. Please check the specification for SBML. -2023-02-02 12:08:21,966 ERROR o.s.j.x.p.SBMLCoreParser [main] Property compartment is not defined in reaction for Level 2 and Version 1. -2023-02-02 12:08:21,966 INFO o.s.j.x.p.SBMLCoreParser [main] Attribute = compartment, value 'Cell' , element name = reaction -2023-02-02 12:08:21,966 WARN o.s.j.x.p.SBMLCoreParser [main] Could not recognize the attribute 'compartment' on the element reaction. Please check the specification for SBML. -2023-02-02 12:08:21,967 ERROR o.s.j.x.p.SBMLCoreParser [main] Property constant is not defined in speciesReference for Level 2 and Version 1. -2023-02-02 12:08:21,967 INFO o.s.j.x.p.SBMLCoreParser [main] Attribute = constant, value 'true' , element name = speciesReference -2023-02-02 12:08:21,967 WARN o.s.j.x.p.SBMLCoreParser [main] Could not recognize the attribute 'constant' on the element speciesReference. Please check the specification for SBML. -2023-02-02 12:08:21,968 ERROR o.s.j.x.p.SBMLCoreParser [main] Property compartment is not defined in reaction for Level 2 and Version 1. -2023-02-02 12:08:21,968 INFO o.s.j.x.p.SBMLCoreParser [main] Attribute = compartment, value 'Cell' , element name = reaction -2023-02-02 12:08:21,968 WARN o.s.j.x.p.SBMLCoreParser [main] Could not recognize the attribute 'compartment' on the element reaction. Please check the specification for SBML. -2023-02-02 12:08:21,969 ERROR o.s.j.x.p.SBMLCoreParser [main] Property constant is not defined in speciesReference for Level 2 and Version 1. -2023-02-02 12:08:21,969 INFO o.s.j.x.p.SBMLCoreParser [main] Attribute = constant, value 'true' , element name = speciesReference -2023-02-02 12:08:21,969 WARN o.s.j.x.p.SBMLCoreParser [main] Could not recognize the attribute 'constant' on the element speciesReference. Please check the specification for SBML. -2023-02-02 12:08:21,970 ERROR o.s.j.x.p.SBMLCoreParser [main] Property compartment is not defined in reaction for Level 2 and Version 1. -2023-02-02 12:08:21,970 INFO o.s.j.x.p.SBMLCoreParser [main] Attribute = compartment, value 'Cell' , element name = reaction -2023-02-02 12:08:21,970 WARN o.s.j.x.p.SBMLCoreParser [main] Could not recognize the attribute 'compartment' on the element reaction. Please check the specification for SBML. -2023-02-02 12:08:21,971 ERROR o.s.j.x.p.SBMLCoreParser [main] Property constant is not defined in speciesReference for Level 2 and Version 1. -2023-02-02 12:08:21,971 INFO o.s.j.x.p.SBMLCoreParser [main] Attribute = constant, value 'true' , element name = speciesReference -2023-02-02 12:08:21,971 WARN o.s.j.x.p.SBMLCoreParser [main] Could not recognize the attribute 'constant' on the element speciesReference. Please check the specification for SBML. -2023-02-02 12:08:21,972 ERROR o.s.j.x.p.SBMLCoreParser [main] Property compartment is not defined in reaction for Level 2 and Version 1. -2023-02-02 12:08:21,972 INFO o.s.j.x.p.SBMLCoreParser [main] Attribute = compartment, value 'Cell' , element name = reaction -2023-02-02 12:08:21,972 WARN o.s.j.x.p.SBMLCoreParser [main] Could not recognize the attribute 'compartment' on the element reaction. Please check the specification for SBML. -2023-02-02 12:08:21,973 ERROR o.s.j.x.p.SBMLCoreParser [main] Property constant is not defined in speciesReference for Level 2 and Version 1. -2023-02-02 12:08:21,973 INFO o.s.j.x.p.SBMLCoreParser [main] Attribute = constant, value 'true' , element name = speciesReference -2023-02-02 12:08:21,973 WARN o.s.j.x.p.SBMLCoreParser [main] Could not recognize the attribute 'constant' on the element speciesReference. Please check the specification for SBML. -2023-02-02 12:08:21,974 ERROR o.s.j.x.p.SBMLCoreParser [main] Property compartment is not defined in reaction for Level 2 and Version 1. -2023-02-02 12:08:21,974 INFO o.s.j.x.p.SBMLCoreParser [main] Attribute = compartment, value 'Cell' , element name = reaction -2023-02-02 12:08:21,974 WARN o.s.j.x.p.SBMLCoreParser [main] Could not recognize the attribute 'compartment' on the element reaction. Please check the specification for SBML. -2023-02-02 12:08:21,974 ERROR o.s.j.x.p.SBMLCoreParser [main] Property constant is not defined in speciesReference for Level 2 and Version 1. -2023-02-02 12:08:21,974 INFO o.s.j.x.p.SBMLCoreParser [main] Attribute = constant, value 'true' , element name = speciesReference -2023-02-02 12:08:21,975 WARN o.s.j.x.p.SBMLCoreParser [main] Could not recognize the attribute 'constant' on the element speciesReference. Please check the specification for SBML. -2023-02-02 12:08:21,975 ERROR o.s.j.x.p.SBMLCoreParser [main] Property constant is not defined in speciesReference for Level 2 and Version 1. -2023-02-02 12:08:21,975 INFO o.s.j.x.p.SBMLCoreParser [main] Attribute = constant, value 'true' , element name = speciesReference -2023-02-02 12:08:21,975 WARN o.s.j.x.p.SBMLCoreParser [main] Could not recognize the attribute 'constant' on the element speciesReference. Please check the specification for SBML. -2023-02-02 12:08:21,976 ERROR o.s.j.x.p.SBMLCoreParser [main] Property constant is not defined in speciesReference for Level 2 and Version 1. -2023-02-02 12:08:21,976 INFO o.s.j.x.p.SBMLCoreParser [main] Attribute = constant, value 'true' , element name = speciesReference -2023-02-02 12:08:21,976 WARN o.s.j.x.p.SBMLCoreParser [main] Could not recognize the attribute 'constant' on the element speciesReference. Please check the specification for SBML. -2023-02-02 12:08:21,977 WARN o.s.j.x.p.SBMLCoreParser [main] The element 'listOfLocalParameters' is not recognized. -2023-02-02 12:08:21,977 ERROR o.s.j.x.p.SBMLCoreParser [main] Property compartment is not defined in reaction for Level 2 and Version 1. -2023-02-02 12:08:21,977 INFO o.s.j.x.p.SBMLCoreParser [main] Attribute = compartment, value 'Cell' , element name = reaction -2023-02-02 12:08:21,978 WARN o.s.j.x.p.SBMLCoreParser [main] Could not recognize the attribute 'compartment' on the element reaction. Please check the specification for SBML. -2023-02-02 12:08:21,978 ERROR o.s.j.x.p.SBMLCoreParser [main] Property constant is not defined in speciesReference for Level 2 and Version 1. -2023-02-02 12:08:21,978 INFO o.s.j.x.p.SBMLCoreParser [main] Attribute = constant, value 'true' , element name = speciesReference -2023-02-02 12:08:21,978 WARN o.s.j.x.p.SBMLCoreParser [main] Could not recognize the attribute 'constant' on the element speciesReference. Please check the specification for SBML. -2023-02-02 12:08:21,979 ERROR o.s.j.x.p.SBMLCoreParser [main] Property constant is not defined in speciesReference for Level 2 and Version 1. -2023-02-02 12:08:21,979 INFO o.s.j.x.p.SBMLCoreParser [main] Attribute = constant, value 'true' , element name = speciesReference -2023-02-02 12:08:21,979 WARN o.s.j.x.p.SBMLCoreParser [main] Could not recognize the attribute 'constant' on the element speciesReference. Please check the specification for SBML. -2023-02-02 12:08:21,979 ERROR o.s.j.x.p.SBMLCoreParser [main] Property constant is not defined in speciesReference for Level 2 and Version 1. -2023-02-02 12:08:21,979 INFO o.s.j.x.p.SBMLCoreParser [main] Attribute = constant, value 'true' , element name = speciesReference -2023-02-02 12:08:21,980 WARN o.s.j.x.p.SBMLCoreParser [main] Could not recognize the attribute 'constant' on the element speciesReference. Please check the specification for SBML. -2023-02-02 12:08:21,981 WARN o.s.j.x.p.SBMLCoreParser [main] The element 'listOfLocalParameters' is not recognized. -2023-02-02 12:08:21,981 ERROR o.s.j.x.p.SBMLCoreParser [main] Property compartment is not defined in reaction for Level 2 and Version 1. -2023-02-02 12:08:21,981 INFO o.s.j.x.p.SBMLCoreParser [main] Attribute = compartment, value 'Cell' , element name = reaction -2023-02-02 12:08:21,981 WARN o.s.j.x.p.SBMLCoreParser [main] Could not recognize the attribute 'compartment' on the element reaction. Please check the specification for SBML. -2023-02-02 12:08:21,982 ERROR o.s.j.x.p.SBMLCoreParser [main] Property constant is not defined in speciesReference for Level 2 and Version 1. -2023-02-02 12:08:21,982 INFO o.s.j.x.p.SBMLCoreParser [main] Attribute = constant, value 'true' , element name = speciesReference -2023-02-02 12:08:21,982 WARN o.s.j.x.p.SBMLCoreParser [main] Could not recognize the attribute 'constant' on the element speciesReference. Please check the specification for SBML. -2023-02-02 12:08:21,983 ERROR o.s.j.x.p.SBMLCoreParser [main] Property constant is not defined in speciesReference for Level 2 and Version 1. -2023-02-02 12:08:21,983 INFO o.s.j.x.p.SBMLCoreParser [main] Attribute = constant, value 'true' , element name = speciesReference -2023-02-02 12:08:21,983 WARN o.s.j.x.p.SBMLCoreParser [main] Could not recognize the attribute 'constant' on the element speciesReference. Please check the specification for SBML. -2023-02-02 12:08:21,984 ERROR o.s.j.x.p.SBMLCoreParser [main] Property compartment is not defined in reaction for Level 2 and Version 1. -2023-02-02 12:08:21,985 INFO o.s.j.x.p.SBMLCoreParser [main] Attribute = compartment, value 'Cell' , element name = reaction -2023-02-02 12:08:21,985 WARN o.s.j.x.p.SBMLCoreParser [main] Could not recognize the attribute 'compartment' on the element reaction. Please check the specification for SBML. -2023-02-02 12:08:21,985 ERROR o.s.j.x.p.SBMLCoreParser [main] Property constant is not defined in speciesReference for Level 2 and Version 1. -2023-02-02 12:08:21,985 INFO o.s.j.x.p.SBMLCoreParser [main] Attribute = constant, value 'true' , element name = speciesReference -2023-02-02 12:08:21,985 WARN o.s.j.x.p.SBMLCoreParser [main] Could not recognize the attribute 'constant' on the element speciesReference. Please check the specification for SBML. -2023-02-02 12:08:21,987 ERROR o.s.j.x.p.SBMLCoreParser [main] Property useValuesFromTriggerTime is not defined in event for Level 2 and Version 1. -2023-02-02 12:08:21,987 INFO o.s.j.x.p.SBMLCoreParser [main] Attribute = useValuesFromTriggerTime, value 'false' , element name = event -2023-02-02 12:08:21,987 WARN o.s.j.x.p.SBMLCoreParser [main] Could not recognize the attribute 'useValuesFromTriggerTime' on the element event. Please check the specification for SBML. -2023-02-02 12:08:21,988 ERROR o.s.j.x.p.SBMLCoreParser [main] Property initialValue is not defined in trigger for Level 2 and Version 1. -2023-02-02 12:08:21,988 INFO o.s.j.x.p.SBMLCoreParser [main] Attribute = initialValue, value 'false' , element name = trigger -2023-02-02 12:08:21,988 WARN o.s.j.x.p.SBMLCoreParser [main] Could not recognize the attribute 'initialValue' on the element trigger. Please check the specification for SBML. -2023-02-02 12:08:21,988 ERROR o.s.j.x.p.SBMLCoreParser [main] Property persistent is not defined in trigger for Level 2 and Version 1. -2023-02-02 12:08:21,988 INFO o.s.j.x.p.SBMLCoreParser [main] Attribute = persistent, value 'false' , element name = trigger -2023-02-02 12:08:21,988 WARN o.s.j.x.p.SBMLCoreParser [main] Could not recognize the attribute 'persistent' on the element trigger. Please check the specification for SBML. -2023-02-02 12:08:21,989 ERROR o.s.j.x.p.SBMLCoreParser [main] Property useValuesFromTriggerTime is not defined in event for Level 2 and Version 1. -2023-02-02 12:08:21,989 INFO o.s.j.x.p.SBMLCoreParser [main] Attribute = useValuesFromTriggerTime, value 'false' , element name = event -2023-02-02 12:08:21,989 WARN o.s.j.x.p.SBMLCoreParser [main] Could not recognize the attribute 'useValuesFromTriggerTime' on the element event. Please check the specification for SBML. -2023-02-02 12:08:21,990 ERROR o.s.j.x.p.SBMLCoreParser [main] Property initialValue is not defined in trigger for Level 2 and Version 1. -2023-02-02 12:08:21,990 INFO o.s.j.x.p.SBMLCoreParser [main] Attribute = initialValue, value 'false' , element name = trigger -2023-02-02 12:08:21,990 WARN o.s.j.x.p.SBMLCoreParser [main] Could not recognize the attribute 'initialValue' on the element trigger. Please check the specification for SBML. -2023-02-02 12:08:21,990 ERROR o.s.j.x.p.SBMLCoreParser [main] Property persistent is not defined in trigger for Level 2 and Version 1. -2023-02-02 12:08:21,990 INFO o.s.j.x.p.SBMLCoreParser [main] Attribute = persistent, value 'false' , element name = trigger -2023-02-02 12:08:21,991 WARN o.s.j.x.p.SBMLCoreParser [main] Could not recognize the attribute 'persistent' on the element trigger. Please check the specification for SBML. -2023-02-02 12:08:21,991 ERROR o.s.j.x.p.SBMLCoreParser [main] Property useValuesFromTriggerTime is not defined in event for Level 2 and Version 1. -2023-02-02 12:08:21,991 INFO o.s.j.x.p.SBMLCoreParser [main] Attribute = useValuesFromTriggerTime, value 'false' , element name = event -2023-02-02 12:08:21,991 WARN o.s.j.x.p.SBMLCoreParser [main] Could not recognize the attribute 'useValuesFromTriggerTime' on the element event. Please check the specification for SBML. -2023-02-02 12:08:21,992 ERROR o.s.j.x.p.SBMLCoreParser [main] Property initialValue is not defined in trigger for Level 2 and Version 1. -2023-02-02 12:08:21,992 INFO o.s.j.x.p.SBMLCoreParser [main] Attribute = initialValue, value 'false' , element name = trigger -2023-02-02 12:08:21,992 WARN o.s.j.x.p.SBMLCoreParser [main] Could not recognize the attribute 'initialValue' on the element trigger. Please check the specification for SBML. -2023-02-02 12:08:21,992 ERROR o.s.j.x.p.SBMLCoreParser [main] Property persistent is not defined in trigger for Level 2 and Version 1. -2023-02-02 12:08:21,992 INFO o.s.j.x.p.SBMLCoreParser [main] Attribute = persistent, value 'false' , element name = trigger -2023-02-02 12:08:21,992 WARN o.s.j.x.p.SBMLCoreParser [main] Could not recognize the attribute 'persistent' on the element trigger. Please check the specification for SBML. -2023-02-02 12:08:21,993 ERROR o.s.j.x.p.SBMLCoreParser [main] Property useValuesFromTriggerTime is not defined in event for Level 2 and Version 1. -2023-02-02 12:08:21,993 INFO o.s.j.x.p.SBMLCoreParser [main] Attribute = useValuesFromTriggerTime, value 'false' , element name = event -2023-02-02 12:08:21,994 WARN o.s.j.x.p.SBMLCoreParser [main] Could not recognize the attribute 'useValuesFromTriggerTime' on the element event. Please check the specification for SBML. -2023-02-02 12:08:21,994 ERROR o.s.j.x.p.SBMLCoreParser [main] Property initialValue is not defined in trigger for Level 2 and Version 1. -2023-02-02 12:08:21,994 INFO o.s.j.x.p.SBMLCoreParser [main] Attribute = initialValue, value 'false' , element name = trigger -2023-02-02 12:08:21,994 WARN o.s.j.x.p.SBMLCoreParser [main] Could not recognize the attribute 'initialValue' on the element trigger. Please check the specification for SBML. -2023-02-02 12:08:21,995 ERROR o.s.j.x.p.SBMLCoreParser [main] Property persistent is not defined in trigger for Level 2 and Version 1. -2023-02-02 12:08:21,995 INFO o.s.j.x.p.SBMLCoreParser [main] Attribute = persistent, value 'false' , element name = trigger -2023-02-02 12:08:21,995 WARN o.s.j.x.p.SBMLCoreParser [main] Could not recognize the attribute 'persistent' on the element trigger. Please check the specification for SBML. diff --git a/GeneticCircuits/Toggle_Switch/README.md b/GeneticCircuits/Toggle_Switch/README.md deleted file mode 100644 index 294a1e4..0000000 --- a/GeneticCircuits/Toggle_Switch/README.md +++ /dev/null @@ -1,7 +0,0 @@ -### Toggle Switch - -The toggle switch is a state holding gate and consists of two promoters each followed by a coding sequence. Each promoter is repressed by the protein transcribed by the other promoter [1]. - -![Figure7](../../Media/ToggleSwitch.png) - -1. Gardner, T. S.; Cantor, C. R.; Collins, J. J. Construction of a Genetic Toggle Switch in Escherichia Coli. Nature 2000, 403 (6767), 339–342. https://doi.org/10.1038/35002131. diff --git a/README.md b/README.md index 889a631..5608de6 100644 --- a/README.md +++ b/README.md @@ -15,7 +15,3 @@ Chemical reaction networks are systems including some number of chemical species ### Genetic Circuits Genetic circuits are part of synthetic biology, a research field combining engineering principles with biology. Researchers build circuits out of defined biological parts adding desired functionalities to biological systems. Automation in the design process allows scientists to model and analyze their genetic circuits \emph{in silico} to test the system before implementation. Stochastic model checking has been used to analyze genetic circuits before, which have an infinite state space and therefore suit the case studies presented here. - -### Fault Computing - -Fault tolerant computing encompasses a wide variety of fault mechanisms and strategies to mitigate them. The case studies presented here focus on circuits that experience transient upsets modeled by Markov processes. Case studies in this field are given in two subcategories.