| |
---|
| | channel price_In { |
---|
| | out price(prev_price:Int, setPrice(cur_price)) == cur_price |
---|
| | } |
---|
| | channel siteA_Add { |
---|
| | out siteA(prev_products:List, addProduct(price:Int, capacity:Int)) == cons({"price": price, "capacity": capacity}, prev_products) |
---|
| | out siteA(prev_products:List, addProductToSiteA(price:Int, capacity:Int)) == cons({"price": price, "capacity": capacity}, prev_products) |
---|
| | } |
---|
| | channel capacity_Update { |
---|
| | in siteA(prev_products:List, updateList(cur_products, cur_capacity)) == cur_products |
---|
| | in capacity(prev_capacity:Int, updateList(cur_products, cur_capacity)) == cur_capacity |
---|
| |
---|
| | |
|