11use crate :: {
22 model:: {
3- query:: { Create , Insert , Predicate , Query , Select } ,
3+ query:: { Create , Delete , Insert , Predicate , Query , Select } ,
44 table:: Value ,
55 } ,
66 runner:: env:: SimulatorEnv ,
@@ -35,7 +35,7 @@ pub(crate) enum Property {
3535 /// The insert query
3636 insert : Insert ,
3737 /// Additional interactions in the middle of the property
38- interactions : Vec < Query > ,
38+ queries : Vec < Query > ,
3939 /// The select query
4040 select : Select ,
4141 } ,
@@ -55,7 +55,7 @@ pub(crate) enum Property {
5555 /// The create query
5656 create : Create ,
5757 /// Additional interactions in the middle of the property
58- interactions : Vec < Query > ,
58+ queries : Vec < Query > ,
5959 } ,
6060}
6161
@@ -70,7 +70,7 @@ impl Property {
7070 match self {
7171 Property :: InsertSelect {
7272 insert,
73- interactions : _ , // todo: add extensional interactions
73+ queries ,
7474 select,
7575 } => {
7676 // Check that the row is there
@@ -106,21 +106,34 @@ impl Property {
106106 } ) ,
107107 } ) ;
108108
109- vec ! [
110- assumption,
111- Interaction :: Query ( Query :: Insert ( insert. clone( ) ) ) ,
112- Interaction :: Query ( Query :: Select ( select. clone( ) ) ) ,
113- assertion,
114- ]
109+ let mut interactions = Vec :: new ( ) ;
110+ interactions. push ( assumption) ;
111+ interactions. push ( Interaction :: Query ( Query :: Insert ( insert. clone ( ) ) ) ) ;
112+ interactions. extend ( queries. clone ( ) . into_iter ( ) . map ( Interaction :: Query ) ) ;
113+ interactions. push ( Interaction :: Query ( Query :: Select ( select. clone ( ) ) ) ) ;
114+ interactions. push ( assertion) ;
115+
116+ interactions
115117 }
116118 Property :: DoubleCreateFailure {
117119 create,
118- interactions : _ , // todo: add extensional interactions
120+ queries ,
119121 } => {
120122 let table_name = create. table . name . clone ( ) ;
123+
124+ let assumption = Interaction :: Assumption ( Assertion {
125+ message : "Double-Create-Failure should not be called on an existing table"
126+ . to_string ( ) ,
127+ func : Box :: new ( move |_: & Vec < ResultSet > , env : & SimulatorEnv | {
128+ !env. tables . iter ( ) . any ( |t| t. name == table_name)
129+ } ) ,
130+ } ) ;
131+
121132 let cq1 = Interaction :: Query ( Query :: Create ( create. clone ( ) ) ) ;
122133 let cq2 = Interaction :: Query ( Query :: Create ( create. clone ( ) ) ) ;
123134
135+ let table_name = create. table . name . clone ( ) ;
136+
124137 let assertion = Interaction :: Assertion ( Assertion {
125138 message :
126139 "creating two tables with the name should result in a failure for the second query"
@@ -136,13 +149,26 @@ impl Property {
136149 } ) ,
137150 } ) ;
138151
139- vec ! [ cq1, cq2, assertion]
152+ let mut interactions = Vec :: new ( ) ;
153+ interactions. push ( assumption) ;
154+ interactions. push ( cq1) ;
155+ interactions. extend ( queries. clone ( ) . into_iter ( ) . map ( Interaction :: Query ) ) ;
156+ interactions. push ( cq2) ;
157+ interactions. push ( assertion) ;
158+
159+ interactions
140160 }
141161 }
142162 }
143163}
144164
145- fn remaining ( env : & SimulatorEnv , stats : & InteractionStats ) -> ( f64 , f64 , f64 ) {
165+ pub ( crate ) struct Remaining {
166+ pub ( crate ) read : f64 ,
167+ pub ( crate ) write : f64 ,
168+ pub ( crate ) create : f64 ,
169+ }
170+
171+ fn remaining ( env : & SimulatorEnv , stats : & InteractionStats ) -> Remaining {
146172 let remaining_read = ( ( env. opts . max_interactions as f64 * env. opts . read_percent / 100.0 )
147173 - ( stats. read_count as f64 ) )
148174 . max ( 0.0 ) ;
@@ -153,10 +179,14 @@ fn remaining(env: &SimulatorEnv, stats: &InteractionStats) -> (f64, f64, f64) {
153179 - ( stats. create_count as f64 ) )
154180 . max ( 0.0 ) ;
155181
156- ( remaining_read, remaining_write, remaining_create)
182+ Remaining {
183+ read : remaining_read,
184+ write : remaining_write,
185+ create : remaining_create,
186+ }
157187}
158188
159- fn property_insert_select < R : rand:: Rng > ( rng : & mut R , env : & SimulatorEnv ) -> Property {
189+ fn property_insert_select < R : rand:: Rng > ( rng : & mut R , env : & SimulatorEnv , remaining : & Remaining ) -> Property {
160190 // Get a random table
161191 let table = pick ( & env. tables , rng) ;
162192 // Pick a random column
@@ -181,6 +211,36 @@ fn property_insert_select<R: rand::Rng>(rng: &mut R, env: &SimulatorEnv) -> Prop
181211 values : vec ! [ row. clone( ) ] ,
182212 } ;
183213
214+ // Create random queries respecting the constraints
215+ let mut queries = Vec :: new ( ) ;
216+ // - [x] There will be no errors in the middle interactions. (this constraint is impossible to check, so this is just best effort)
217+ // - [x] The inserted row will not be deleted.
218+ // - [ ] The inserted row will not be updated. (todo: add this constraint once UPDATE is implemented)
219+ // - [ ] The table `t` will not be renamed, dropped, or altered. (todo: add this constraint once ALTER or DROP is implemented)
220+ for _ in 0 ..rng. gen_range ( 0 ..3 ) {
221+ let query = Query :: arbitrary_from ( rng, & ( table, remaining) ) ;
222+ match & query {
223+ Query :: Delete ( Delete {
224+ table : t,
225+ predicate,
226+ } ) => {
227+ // The inserted row will not be deleted.
228+ if t == & table. name && predicate. test ( & row, & table) {
229+ continue ;
230+ }
231+ }
232+ Query :: Create ( Create { table : t } ) => {
233+ // There will be no errors in the middle interactions.
234+ // - Creating the same table is an error
235+ if t. name == table. name {
236+ continue ;
237+ }
238+ }
239+ _ => ( ) ,
240+ }
241+ queries. push ( query) ;
242+ }
243+
184244 // Select the row
185245 let select_query = Select {
186246 table : table. name . clone ( ) ,
@@ -189,40 +249,62 @@ fn property_insert_select<R: rand::Rng>(rng: &mut R, env: &SimulatorEnv) -> Prop
189249
190250 Property :: InsertSelect {
191251 insert : insert_query,
192- interactions : Vec :: new ( ) ,
252+ queries ,
193253 select : select_query,
194254 }
195255}
196256
197- fn property_double_create_failure < R : rand:: Rng > ( rng : & mut R , env : & SimulatorEnv ) -> Property {
257+ fn property_double_create_failure < R : rand:: Rng > ( rng : & mut R , env : & SimulatorEnv , remaining : & Remaining ) -> Property {
198258 // Get a random table
199259 let table = pick ( & env. tables , rng) ;
200260 // Create the table
201261 let create_query = Create {
202262 table : table. clone ( ) ,
203263 } ;
204264
265+ // Create random queries respecting the constraints
266+ let mut queries = Vec :: new ( ) ;
267+ // The interactions in the middle has the following constraints;
268+ // - [x] There will be no errors in the middle interactions.(best effort)
269+ // - [ ] Table `t` will not be renamed or dropped.(todo: add this constraint once ALTER or DROP is implemented)
270+ for _ in 0 ..rng. gen_range ( 0 ..3 ) {
271+ let query = Query :: arbitrary_from ( rng, & ( table, remaining) ) ;
272+ match & query {
273+ Query :: Create ( Create { table : t } ) => {
274+ // There will be no errors in the middle interactions.
275+ // - Creating the same table is an error
276+ if t. name == table. name {
277+ continue ;
278+ }
279+ }
280+ _ => ( ) ,
281+ }
282+ queries. push ( query) ;
283+ }
284+
205285 Property :: DoubleCreateFailure {
206286 create : create_query,
207- interactions : Vec :: new ( ) ,
287+ queries ,
208288 }
209289}
210290
291+
292+
211293impl ArbitraryFrom < ( & SimulatorEnv , & InteractionStats ) > for Property {
212294 fn arbitrary_from < R : rand:: Rng > (
213295 rng : & mut R ,
214296 ( env, stats) : & ( & SimulatorEnv , & InteractionStats ) ,
215297 ) -> Self {
216- let ( remaining_read , remaining_write , remaining_create ) = remaining ( env, stats) ;
298+ let remaining_ = remaining ( env, stats) ;
217299 frequency (
218300 vec ! [
219301 (
220- f64 :: min( remaining_read , remaining_write ) ,
221- Box :: new( |rng: & mut R | property_insert_select( rng, env) ) ,
302+ f64 :: min( remaining_ . read , remaining_ . write ) ,
303+ Box :: new( |rng: & mut R | property_insert_select( rng, env, & remaining_ ) ) ,
222304 ) ,
223305 (
224- remaining_create / 2.0 ,
225- Box :: new( |rng: & mut R | property_double_create_failure( rng, env) ) ,
306+ remaining_ . create / 2.0 ,
307+ Box :: new( |rng: & mut R | property_double_create_failure( rng, env, & remaining_ ) ) ,
226308 ) ,
227309 ] ,
228310 rng,
0 commit comments