{"action":"created","issue":{"url":"https://api.github.com/repos/newca12/gapt/issues/264","labels_url":"https://api.github.com/repos/newca12/gapt/issues/264/labels{/name}","comments_url":"https://api.github.com/repos/newca12/gapt/issues/264/comments","events_url":"https://api.github.com/repos/newca12/gapt/issues/264/events","html_url":"https://github.com/newca12/gapt/issues/264","id":55608466,"number":264,"title":"non-deterministic bug, apparently in cleanStructuralRules","user":{"login":"newca12","id":543542,"avatar_url":"https://avatars.githubusercontent.com/u/543542?v=3","gravatar_id":"","url":"https://api.github.com/users/newca12","html_url":"https://github.com/newca12","followers_url":"https://api.github.com/users/newca12/followers","following_url":"https://api.github.com/users/newca12/following{/other_user}","gists_url":"https://api.github.com/users/newca12/gists{/gist_id}","starred_url":"https://api.github.com/users/newca12/starred{/owner}{/repo}","subscriptions_url":"https://api.github.com/users/newca12/subscriptions","organizations_url":"https://api.github.com/users/newca12/orgs","repos_url":"https://api.github.com/users/newca12/repos","events_url":"https://api.github.com/users/newca12/events{/privacy}","received_events_url":"https://api.github.com/users/newca12/received_events","type":"User","site_admin":false},"labels":[{"url":"https://api.github.com/repos/newca12/gapt/labels/1%20star","name":"1 star","color":"FFFFFF"},{"url":"https://api.github.com/repos/newca12/gapt/labels/bug","name":"bug","color":"FFFFFF"},{"url":"https://api.github.com/repos/newca12/gapt/labels/imported","name":"imported","color":"FFFFFF"},{"url":"https://api.github.com/repos/newca12/gapt/labels/Priority-High","name":"Priority-High","color":"FFFFFF"}],"state":"open","locked":false,"assignee":null,"milestone":null,"comments":3,"created_at":"2015-01-27T11:52:57Z","updated_at":"2015-01-27T11:53:09Z","closed_at":null,"body":"_From [stefan.hetzl](https://code.google.com/u/stefan.hetzl/) on April 04, 2014 17:42:17_\n\nI have been experiencing the following strange behaviour. During 'mvn install', a test failed as below. I tried running this test again several times using 'mvn -pl integration_tests/misc_test install' and sometimes this problem did occur, and sometimes it did not (i.e. all tests passed successfully). In fact, after around 15 tries, the test seems to fail with a probability of only 20-25&#37;.\r\n\r\nThis looks to me like a bug in cleanStructuralRules which is sometimes exposed (and sometimes not) depending on the proof produced by reading back an expansion tree.\r\n\r\nThe bug should be fixed, even if it appears only sometimes.\r\n\r\nIndependently of that it would be nice to understand the cause of this non-deterministic behaviour. Bernhard, any thoughts on that?\r\n\r\n\\-------------------------------------------------------\r\n T E S T S\r\n\\-------------------------------------------------------\r\nRunning at.logic.integration_tests.MiscTest\r\nUsing OneVariableDelta.\r\n\r\nEnd sequent: P(0), ∀x.(P(x)⊃P(s(x))) :- P(s(s(s(s(0)))))\r\nSize of term set: 4\r\ninitializing generalized delta-table (set-based)\r\n\r\nNumber of grammars: 2\r\nSmallest grammar-size: 4\r\nNumber of smallest grammars: 2\r\nlog4j:WARN No appenders could be found for logger (at.logic.algorithms.cutIntroduction.CutIntroduction$).\r\nlog4j:WARN Please initialize the log4j system properly.\r\nlog4j:WARN See http://logging.apache.org/log4j/1.2/faq.html#noconfig for more info.\r\n\r\nGrammar chosen: {List(tuple1(s(α_0)), tuple1(α_0))} o {Set(List(0), List(s(s(0))))}\r\n\r\nMinimized cut formula: ∀x.(P(s(s(x)))∨¬P(x))\r\n\r\nWarning: Axiom not uniquely specified, possible candidates:  A21   ∀x:ι.=(bm(x:ι, 0:ι):ι, x:ι): o, A20   ∀x:ι.=(bm(0:ι, x:ι):ι, 0:ι): o\r\nWarning: Axiom not uniquely specified, possible candidates:  A35   ∀x:ι.∀y:ι.(<(+(x:ι, 1:ι):ι, +(y:ι, 1:ι):ι): o⊃<(x:ι, y:ι): o), A17   ∀x:ι.∀z:ι.∀y:ι.(<(+(x:ι, z:ι):ι, +(y:ι, z:ι):ι): o⊃<(x:ι, y:ι): o)\r\nUser specified sub works!{ Y  ->  (\\lambda x ( - ((x + 1) \\< x))) }\r\nWarning: Axiom not uniquely specified, possible candidates:  IND   ∀Y:(ι->ο).((Y(0:ι): o∧∀n:ι.(Y(n:ι): o⊃Y(+(n:ι, 1:ι):ι): o))⊃∀n:ι.Y(n:ι): o), IND   ∀Y:(ι->ο).((Y(0:ι): o∧∀n:ι.(Y(n:ι): o⊃Y(+(n:ι, 1:ι):ι): o))⊃∀n:ι.Y(n:ι): o)\r\nWarning: Axiom not uniquely specified, possible candidates:  A32   ∀x:ι.∀y:ι.(<(x:ι, y:ι): o⊃<(+(x:ι, 1:ι):ι, +(y:ι, 1:ι):ι): o), A36   ∀x:ι.∀z:ι.∀y:ι.(<(x:ι, y:ι): o⊃<(+(x:ι, z:ι):ι, +(y:ι, z:ι):ι): o)\r\nUser specified sub works!{ Y  ->  (\\lambda x (x \\< (x + 1))) }\r\nWarning: Axiom not uniquely specified, possible candidates:  IND   ∀Y:(ι->ο).((Y(0:ι): o∧∀n:ι.(Y(n:ι): o⊃Y(+(n:ι, 1:ι):ι): o))⊃∀n:ι.Y(n:ι): o), IND   ∀Y:(ι->ο).((Y(0:ι): o∧∀n:ι.(Y(n:ι): o⊃Y(+(n:ι, 1:ι):ι): o))⊃∀n:ι.Y(n:ι): o)\r\nwrong sub found! ((exists x_{16} (MON(h, 0) & NOCC(h, 0, \\sigma))) & (all n ((exists x_{17} (MON(h, n) & NOCC(h, n, \\sigma))) -> (exists x_{18} (MON(h, (n + 1)) & NOCC(h, (n + 1), \\sigma)))))) -> (all n (exists x_{19} (MON(h, n) & NOCC(h, n, \\sigma))))  for  ((exists h (MON(h, 0) & NOCC(h, 0, \\sigma))) & (all n ((exists h (MON(h, n) & NOCC(h, n, \\sigma))) -> (exists h (MON(h, (n + 1)) & NOCC(h, (n + 1), \\sigma)))))) -> (all n (exists h (MON(h, n) & NOCC(h, n, \\sigma))))  sub={ h  ->  h } ax= ((exists h (MON(h, 0) & NOCC(h, 0, \\sigma))) & (all n ((exists h (MON(h, n) & NOCC(h, n, \\sigma))) -> (exists h (MON(h, (n + 1)) & NOCC(h, (n + 1), \\sigma)))))) -> (all n (exists h (MON(h, n) & NOCC(h, n, \\sigma))))\r\nUser specified sub works!{ Y  ->  (\\lambda x (exists h (MON(h, x) & NOCC(h, x, \\sigma)))) }\r\nTests run: 12, Failures: 0, Errors: 1, Skipped: 2, Time elapsed: 8.468 sec \\<<< FAILURE! - in at.logic.integration_tests.MiscTest\r\nThe system should::Construct proof with expansion sequent extracted from proof 2/2(at.logic.integration_tests.MiscTest)  Time elapsed: 0.11 sec  \\<<< ERROR!\r\nat.logic.calculi.lk.base.LKUnaryRuleCreationException: Could not create lk rule c:l from parent P(0), (P(0)⊃P(s(0))) :- P(s(0)) with auxiliary formulas P(0)\r\n    at at.logic.calculi.lk.propositionalRules.ContractionLeftRule$.apply(propositionalRules.scala:266)\r\n    at at.logic.algorithms.lk.CleanStructuralRules$.cleanStructuralRules(elimination.scala:49)\r\n    at at.logic.algorithms.lk.CleanStructuralRules$.cleanStructuralRules(elimination.scala:43)\r\n    at at.logic.algorithms.lk.CleanStructuralRules$.cleanStructuralRules(elimination.scala:43)\r\n    at at.logic.algorithms.lk.CleanStructuralRules$.cleanStructuralRules(elimination.scala:43)\r\n    at at.logic.algorithms.lk.CleanStructuralRules$.cleanStructuralRules(elimination.scala:53)\r\n    at at.logic.algorithms.lk.CleanStructuralRules$.cleanStructuralRules(elimination.scala:53)\r\n    at at.logic.algorithms.lk.CleanStructuralRules$.cleanStructuralRules(elimination.scala:234)\r\n    at at.logic.algorithms.lk.CleanStructuralRules$.cleanStructuralRules(elimination.scala:43)\r\n    at at.logic.algorithms.lk.CleanStructuralRules$.cleanStructuralRules(elimination.scala:43)\r\n    at at.logic.algorithms.lk.CleanStructuralRules$.cleanStructuralRules(elimination.scala:43)\r\n    at at.logic.algorithms.lk.CleanStructuralRules$.cleanStructuralRules(elimination.scala:43)\r\n    at at.logic.algorithms.lk.CleanStructuralRules$.cleanStructuralRules(elimination.scala:43)\r\n    at at.logic.algorithms.lk.CleanStructuralRules$.cleanStructuralRules(elimination.scala:53)\r\n    at at.logic.algorithms.lk.CleanStructuralRules$.cleanStructuralRules(elimination.scala:114)\r\n    at at.logic.algorithms.lk.CleanStructuralRules$.cleanStructuralRules(elimination.scala:43)\r\n    at at.logic.algorithms.lk.CleanStructuralRules$.cleanStructuralRules(elimination.scala:114)\r\n    at at.logic.algorithms.lk.CleanStructuralRules$.cleanStructuralRules(elimination.scala:43)\r\n    at at.logic.algorithms.lk.CleanStructuralRules$.cleanStructuralRules(elimination.scala:114)\r\n    at at.logic.algorithms.lk.CleanStructuralRules$.cleanStructuralRules(elimination.scala:43)\r\n    at at.logic.algorithms.lk.CleanStructuralRules$.cleanStructuralRules(elimination.scala:114)\r\n    at at.logic.algorithms.lk.CleanStructuralRules$.cleanStructuralRules(elimination.scala:43)\r\n    at at.logic.algorithms.lk.CleanStructuralRules$.apply(elimination.scala:23)\r\n    at at.logic.algorithms.lk.solve$.startProving(solve.scala:66)\r\n    at at.logic.algorithms.lk.solve$.expansionProofToLKProof(solve.scala:55)\r\n    at at.logic.integration_tests.MiscTest$$anonfun$1$$anonfun$apply$42.apply(MiscTest.scala:259)\r\n    at at.logic.integration_tests.MiscTest$$anonfun$1$$anonfun$apply$42.apply(MiscTest.scala:255)\r\n    at org.apache.maven.surefire.junit4.JUnit4Provider.execute(JUnit4Provider.java:264)\r\n    at org.apache.maven.surefire.junit4.JUnit4Provider.executeTestSet(JUnit4Provider.java:153)\r\n    at org.apache.maven.surefire.junit4.JUnit4Provider.invoke(JUnit4Provider.java:124)\r\n    at org.apache.maven.surefire.booter.ForkedBooter.invokeProviderInSameClassLoader(ForkedBooter.java:200)\r\n    at org.apache.maven.surefire.booter.ForkedBooter.runSuitesInProcess(ForkedBooter.java:153)\r\n    at org.apache.maven.surefire...\n\n_Original issue: http://code.google.com/p/gapt/issues/detail?id=264_"},"comment":{"url":"https://api.github.com/repos/newca12/gapt/issues/comments/71635169","html_url":"https://github.com/newca12/gapt/issues/264#issuecomment-71635169","issue_url":"https://api.github.com/repos/newca12/gapt/issues/264","id":71635169,"user":{"login":"newca12","id":543542,"avatar_url":"https://avatars.githubusercontent.com/u/543542?v=3","gravatar_id":"","url":"https://api.github.com/users/newca12","html_url":"https://github.com/newca12","followers_url":"https://api.github.com/users/newca12/followers","following_url":"https://api.github.com/users/newca12/following{/other_user}","gists_url":"https://api.github.com/users/newca12/gists{/gist_id}","starred_url":"https://api.github.com/users/newca12/starred{/owner}{/repo}","subscriptions_url":"https://api.github.com/users/newca12/subscriptions","organizations_url":"https://api.github.com/users/newca12/orgs","repos_url":"https://api.github.com/users/newca12/repos","events_url":"https://api.github.com/users/newca12/events{/privacy}","received_events_url":"https://api.github.com/users/newca12/received_events","type":"User","site_admin":false},"created_at":"2015-01-27T11:53:09Z","updated_at":"2015-01-27T11:53:09Z","body":"_From [stefan.hetzl](https://code.google.com/u/stefan.hetzl/) on April 12, 2014 23:25:01_\n\n**Status:** Fixed  \n"}}