Open-Source Projects: Issueshttps://forge.ispras.ru/https://forge.ispras.ru/favicon.ico?16490126692020-02-22T15:51:39ZOpen-Source Projects
Redmine Retrascope - Task #10133 (New): use '-coi' model checker optionhttps://forge.ispras.ru/issues/101332020-02-22T15:51:39ZSergey Smolovsmolov@ispras.ru
<p>The NuSMV model checker has the followingcommand line option:<br /><pre>
-coi
enables cone of influence reduction
</pre></p>
<p>and so does nuXmv. This option can help in SMV model checking.</p>
<p>Try to enable it in our configuration scripts for NuSMV\nuXmv and check the results.</p> Retrascope Test Suite - Bug #9901 (New): initializationError in some tests after Jenkins updatehttps://forge.ispras.ru/issues/99012019-11-01T08:32:54ZSergey Smolovsmolov@ispras.ru
<p>JDK 11 is used by Jenkins now. It could be the cause of several JUnit test cases falling. Here is an example log:<br /><pre>
java.lang.Exception: The inner class ru.ispras.retrascope.engine.hldd.printer.smv.formula.sample.vcegar.VcegarPjIcram1SmvFormulaPrinterTestCase$TestCase is not static.
at org.junit.runners.BlockJUnit4ClassRunner.validateNoNonStaticInnerClass(BlockJUnit4ClassRunner.java:113)
at org.junit.runners.BlockJUnit4ClassRunner.collectInitializationErrors(BlockJUnit4ClassRunner.java:102)
at org.junit.runners.ParentRunner.validate(ParentRunner.java:355)
at org.junit.runners.ParentRunner.<init>(ParentRunner.java:76)
at org.junit.runners.BlockJUnit4ClassRunner.<init>(BlockJUnit4ClassRunner.java:57)
at org.junit.internal.builders.JUnit4Builder.runnerForClass(JUnit4Builder.java:10)
at org.junit.runners.model.RunnerBuilder.safeRunnerForClass(RunnerBuilder.java:59)
at org.junit.internal.builders.AllDefaultPossibilitiesBuilder.runnerForClass(AllDefaultPossibilitiesBuilder.java:26)
at org.junit.runners.model.RunnerBuilder.safeRunnerForClass(RunnerBuilder.java:59)
at org.junit.internal.requests.ClassRequest.getRunner(ClassRequest.java:26)
at org.gradle.api.internal.tasks.testing.junit.JUnitTestClassExecutor.runTestClass(JUnitTestClassExecutor.java:78)
at org.gradle.api.internal.tasks.testing.junit.JUnitTestClassExecutor.execute(JUnitTestClassExecutor.java:58)
at org.gradle.api.internal.tasks.testing.junit.JUnitTestClassExecutor.execute(JUnitTestClassExecutor.java:38)
at org.gradle.api.internal.tasks.testing.junit.AbstractJUnitTestClassProcessor.processTestClass(AbstractJUnitTestClassProcessor.java:66)
at org.gradle.api.internal.tasks.testing.SuiteTestClassProcessor.processTestClass(SuiteTestClassProcessor.java:51)
at jdk.internal.reflect.GeneratedMethodAccessor2.invoke(Unknown Source)
at java.base/jdk.internal.reflect.DelegatingMethodAccessorImpl.invoke(DelegatingMethodAccessorImpl.java:43)
at java.base/java.lang.reflect.Method.invoke(Method.java:566)
at org.gradle.internal.dispatch.ReflectionDispatch.dispatch(ReflectionDispatch.java:35)
at org.gradle.internal.dispatch.ReflectionDispatch.dispatch(ReflectionDispatch.java:24)
at org.gradle.internal.dispatch.ContextClassLoaderDispatch.dispatch(ContextClassLoaderDispatch.java:32)
at org.gradle.internal.dispatch.ProxyDispatchAdapter$DispatchingInvocationHandler.invoke(ProxyDispatchAdapter.java:93)
at com.sun.proxy.$Proxy5.processTestClass(Unknown Source)
at org.gradle.api.internal.tasks.testing.worker.TestWorker.processTestClass(TestWorker.java:117)
at jdk.internal.reflect.GeneratedMethodAccessor1.invoke(Unknown Source)
at java.base/jdk.internal.reflect.DelegatingMethodAccessorImpl.invoke(DelegatingMethodAccessorImpl.java:43)
at java.base/java.lang.reflect.Method.invoke(Method.java:566)
at org.gradle.internal.dispatch.ReflectionDispatch.dispatch(ReflectionDispatch.java:35)
at org.gradle.internal.dispatch.ReflectionDispatch.dispatch(ReflectionDispatch.java:24)
at org.gradle.internal.remote.internal.hub.MessageHubBackedObjectConnection$DispatchWrapper.dispatch(MessageHubBackedObjectConnection.java:155)
at org.gradle.internal.remote.internal.hub.MessageHubBackedObjectConnection$DispatchWrapper.dispatch(MessageHubBackedObjectConnection.java:137)
at org.gradle.internal.remote.internal.hub.MessageHub$Handler.run(MessageHub.java:404)
at org.gradle.internal.concurrent.ExecutorPolicy$CatchAndRecordFailures.onExecute(ExecutorPolicy.java:63)
at org.gradle.internal.concurrent.ManagedExecutorImpl$1.run(ManagedExecutorImpl.java:46)
at java.base/java.util.concurrent.ThreadPoolExecutor.runWorker(ThreadPoolExecutor.java:1128)
at java.base/java.util.concurrent.ThreadPoolExecutor$Worker.run(ThreadPoolExecutor.java:628)
at org.gradle.internal.concurrent.ThreadFactoryImpl$ManagedThreadRunnable.run(ThreadFactoryImpl.java:55)
at java.base/java.lang.Thread.run(Thread.java:834)
</pre></p> Retrascope Test Suite - Bug #9275 (New): vcegar/pj_icram: too big arrays https://forge.ispras.ru/issues/92752018-09-11T15:09:56ZMikhail Lebedevlebedev@ispras.ru
<p>vcegar/pj_icram designs <code>icram_3.v</code>, <code>icram_4.v</code> and <code>icram_5.v</code> contain too big arrays that <code>nuXmv</code> model checker can't handle:<br /><pre><code>
`define ic_size 2047 // icram_3.v
`define ic_size 4093 // icram_4.v
`define ic_size 8191 // icram_5.v
...
reg [7:0] ic_ram [`ic_size:0];
</code></pre><br />Moreover, Retrascope's cgaa-hldd-transformer engine can't handle <code>icram_4.v</code> and <code>icram_5.v</code> (needs too much memory and time to build HLDDs).<br />These designs will be temporarily excluded from the HLDD-based tests.</p> Retrascope Test Suite - Bug #9071 (Open): ru.ispras.retrascope.engine.hldd.printer.smv.Texas97Hld...https://forge.ispras.ru/issues/90712018-07-05T21:47:24ZSergey Smolovsmolov@ispras.ru
<pre><code class="text syntaxhl" data-language="text">java.lang.IllegalArgumentException: Unknown operation 'FUNCTION'
at ru.ispras.fortress.expression.printer.MapBasedPrinter$ExprTreeVisitor.onOperationBegin(MapBasedPrinter.java:78)
at ru.ispras.retrascope.engine.hldd.printer.smv.utils.SmvExprPrinter$Visitor.onOperationBegin(SmvExprPrinter.java:302)
at ru.ispras.fortress.expression.ExprTreeWalker.visitOperation(ExprTreeWalker.java:139)
at ru.ispras.fortress.expression.ExprTreeWalker.visitNode(ExprTreeWalker.java:123)
at ru.ispras.fortress.expression.ExprTreeWalker.visitOperation(ExprTreeWalker.java:160)
at ru.ispras.fortress.expression.ExprTreeWalker.visitNode(ExprTreeWalker.java:123)
at ru.ispras.fortress.expression.ExprTreeWalker.visitOperation(ExprTreeWalker.java:160)
at ru.ispras.fortress.expression.ExprTreeWalker.visitNode(ExprTreeWalker.java:123)
at ru.ispras.fortress.expression.ExprTreeWalker.visit(ExprTreeWalker.java:93)
at ru.ispras.fortress.expression.printer.MapBasedPrinter.toString(MapBasedPrinter.java:307)
at ru.ispras.retrascope.engine.hldd.printer.smv.HlddSmvVisitor.getExprDescription(HlddSmvVisitor.java:140)
at ru.ispras.retrascope.engine.hldd.printer.smv.HlddSmvVisitor.onAssignment(HlddSmvVisitor.java:318)
at ru.ispras.retrascope.model.hldd.HlddWalker.visitNode(HlddWalker.java:138)
at ru.ispras.retrascope.model.hldd.HlddWalker.visitNode(HlddWalker.java:131)
at ru.ispras.retrascope.model.hldd.HlddWalker.visit(HlddWalker.java:104)
at ru.ispras.retrascope.model.hldd.HlddWalker.visitNode(HlddWalker.java:123)
at ru.ispras.retrascope.model.hldd.HlddWalker.visitRoot(HlddWalker.java:89)
at ru.ispras.retrascope.model.hldd.HlddWalker.visitHldd(HlddWalker.java:79)
at ru.ispras.retrascope.model.hldd.HlddWalker.visitProcess(HlddWalker.java:68)
at ru.ispras.retrascope.model.basis.walker.ModelWalker.visitModule(ModelWalker.java:270)
at ru.ispras.retrascope.model.basis.walker.ModelWalker.visitModel(ModelWalker.java:242)
at ru.ispras.retrascope.model.basis.walker.ModelWalker.start(ModelWalker.java:132)
at ru.ispras.retrascope.engine.hldd.printer.smv.HlddSmvPrinter.start(HlddSmvPrinter.java:65)
at ru.ispras.retrascope.basis.Engine.start(Engine.java:217)
at ru.ispras.retrascope.basis.ToolChain.start(ToolChain.java:111)
at ru.ispras.retrascope.basis.Engine.start(Engine.java:217)
at ru.ispras.retrascope.Retrascope$ToolRun.start(Retrascope.java:215)
at ru.ispras.retrascope.Retrascope.main(Retrascope.java:456)
at ru.ispras.retrascope.Retrascope.main(Retrascope.java:373)
at ru.ispras.retrascope.util.ToolTest.runTest(ToolTest.java:81)
at ru.ispras.retrascope.basis.SingleTest.runTest(SingleTest.java:85)
at ru.ispras.retrascope.basis.BenchmarkTest.runTest(BenchmarkTest.java:60)
</code></pre> Retrascope - Task #6446 (New): Promela translator to CFG representation (no buffers)https://forge.ispras.ru/issues/64462015-11-24T12:56:49ZSergey Smolovsmolov@ispras.ru
<p>Implement a translator for Promela descriptions to CFG representation.<br />First version may not support buffers.</p> Retrascope - Task #5504 (New): add channels between EFSMshttps://forge.ispras.ru/issues/55042014-12-16T11:45:34ZSergey Smolovsmolov@ispras.ru
<p>The EFSMs that are living in the same EfsmModel container should be able to interact with each other by messages.<br />These messages incapsulate events.</p> Retrascope - Task #4892 (New): Анализ набора блок-схем на взаимные блокировкиhttps://forge.ispras.ru/issues/48922014-05-05T07:55:05ZAlexander Kamkinaskamkin@gmail.com
<p>Возможно, эта модель удобнее EFSM. Нужно дополнительное исследование.</p> Retrascope - Feature #4057 (New): Механизм поиска взаимных блокировокhttps://forge.ispras.ru/issues/40572013-04-02T09:25:00ZIgor Melnichenkosuomi-47@ya.ru
<p>Реализация механизма, позволяющего находить взаимные блокировки в EFSM.</p>