wo / tpg

Tree Proof Generator
GNU General Public License v3.0
151 stars 20 forks source link

Proofs take significantly more time on Chrome than on Firefox #3

Closed mr-frying-pan closed 4 years ago

mr-frying-pan commented 4 years ago

For certain formulas finding proofs and counterexamples takes significantly more time on Google Chrome than on Mozilla Firefox. I do not have exact timings but Firefox finishes in a fraction of a second and Chrome takes several minutes at least.

Example: (((∀x(Mx→(◇Px∧◇¬Px))∧∃xMx)∧(∀x(Sx→(◇Mx∧◇¬Mx))∧∃xSx))→(∀x(Sx→(◇Px∧◇¬Px))∧∃xSx)) with reflexivity, transitivity and euclidity%E2%88%A7%E2%88%83xMx)%E2%88%A7(%E2%88%80x(Sx%E2%86%92(%E2%97%87Mx%E2%88%A7%E2%97%87%C2%ACMx))%E2%88%A7%E2%88%83xSx))%E2%86%92(%E2%88%80x(Sx%E2%86%92(%E2%97%87Px%E2%88%A7%E2%97%87%C2%ACPx))%E2%88%A7%E2%88%83xSx))||reflexivity|transitivity|euclidity)

Basically this is due to different implementations of Array.sort() function in Firefox and Chrome. According to MDN callback provided to sort should return a number (positive (a > b) , negative (a < b) or zero (a = b)). Right now those callbacks return a boolean which gets converted into 1 when true and 0 when false. When receiving 0, sort should preserve order of the elements however Firefox does not do that, which results in sorted arrays. Chrome, on the other hand, does and that results in unsorted arrays.

A fix for this would be to make sure that all functions given to Array.sort return a number.

wo commented 4 years ago

Oh, thanks for spotting this, and for figuring out the cause! I should get in the habit of running the tests with Chrome.