HierInvAutomataTool { public static void main(String[] args) throws IOException { Log.ensureInitalization(); if (args.length != 1) { Log.error("0xEE742 Please specify only one single path to the input model."); return; } Log.info("HierInvAutomata DSL Tool", "HierIAT"); Log.info("------------------", "HierIAT"); String model = args[0]; ASTAutomaton ast = parse(model); Log.info(model + " parsed successfully!", "HierIAT"); Log.info("=== 2: HierInvAutomatonCheapVisit =============", "HierIAT"); HierInvAutomataCheapVisit acv1 = new HierInvAutomataCheapVisit(); ast.accept(acv1); }  static void main(String[] args); static ASTAutomaton parse(String model);  }
@Test public void executePingPong() throws IOException { HierInvAutomataTool.main(new String[] { "src/test/resources/example/PingPongInv.aut" }); Log.printFindings(); assertEquals(0, Log.getFindings().size()); List<String> p = LogStub.getPrints(); assertEquals(59, p.size()); assertTrue(p.get(0), p.get(0).matches(".*.INFO. HierIAT HierInvAutomata DSL Tool.*\n")); String res = String.join("",p).replaceAll("[\r\n]", " "); assertTrue(res, res.matches(".*state Pung <<final>> .. &&. &&. &&. true v1 ] ! false ] v2 ] ]].*")); assertTrue(res, res.matches(".*Pong - returnBall > Ping;.*")); }
@Test public void executeSimple12() throws IOException { HierInvAutomataTool.main(new String[] { "src/test/resources/example/Simple12Inv.aut" }); Log.printFindings(); assertEquals(0, Log.getFindings().size()); List<String> p = LogStub.getPrints(); assertTrue(p.size() > 10 ); }
@Test public void executeHierarchyPingPong() throws IOException { HierInvAutomataTool.main(new String[] { "src/test/resources/example/Hierarchy12Inv.aut" }); Log.printFindings(); assertEquals(0, Log.getFindings().size()); List<String> p = LogStub.getPrints(); assertTrue(p.size() > 10 ); }