[SERVER-47503] Invalid batchtime setting on tla_plus task Created: 13/Apr/20  Updated: 29/Oct/23  Resolved: 20/Apr/20

Status: Closed
Project: Core Server
Component/s: Replication
Affects Version/s: None
Fix Version/s: 4.7.0

Type: Bug Priority: Minor - P4
Reporter: A. Jesse Jiryu Davis Assignee: A. Jesse Jiryu Davis
Resolution: Fixed Votes: 0
Labels: None
Remaining Estimate: Not Specified
Time Spent: Not Specified
Original Estimate: Not Specified

Issue Links:
Problem/Incident
is caused by SERVER-45416 TLA+ specs are not continuously tested Closed
Backwards Compatibility: Fully Compatible
Operating System: ALL
Sprint: Repl 2020-04-20, Repl 2020-05-04
Participants:

 Description   

I put "batchtime" in the wrong place in SERVER-45416:

https://github.com/mongodb/mongo/commit/6018c34bd232d565d18ba8ee5b97509b374ac3ed#diff-71ccc9b828b2d68dab47c8be07ab6f96R7696

batchtime is only a setting on build variants and not on individual tasks.



 Comments   
Comment by Githook User [ 20/Apr/20 ]

Author:

{'name': 'A. Jesse Jiryu Davis', 'email': 'jesse@mongodb.com', 'username': 'ajdavis'}

Message: SERVER-47503 Run TLA+ tests daily
Branch: master
https://github.com/mongodb/mongo/commit/61f5d6cf5087d656ebc4bbd2bf75a0a5eacb9cad

Comment by A. Jesse Jiryu Davis [ 17/Apr/20 ]

Besides fixing where batchtime is declared, I'll change it from 1 week to 1 day, since TLA+ model-checking is quicker than I originally expected.

Generated at Thu Feb 08 05:14:22 UTC 2024 using Jira 9.7.1#970001-sha1:2222b88b221c4928ef0de3161136cc90c8356a66.