← Back to branch summary

~verifypn-stub/verifypn/inhibitor-por-error

« back to all changes in this revision

Viewing changes to VerifyPN.cpp

  • Committer: Jiri Srba
  • Date: 2017-12-04 14:08:47 UTC
  • mfrom: (181.5.10 initrw2)
  • Revision ID: srba.jiri@gmail.com-20171204140847-b0u8hwd0vrcbk52r
merged in branch lp:~verifypn-stub/verifypn/initrw additing initial marking rewriting test

Show diffs side-by-side

added added

removed removed

Lines of Context:
VerifyPN.cpp
568
568
            
569
569
            int preSize=queries[i]->formulaSize();
570
570
            negstat_t stats;            
 
571
            EvaluationContext context(qm0, qnet);
571
572
            if(options.printstatistics)
572
573
            {
573
574
                std::cout << "\nQuery before reduction: ";
578
579
                std::cout << std::endl;
579
580
            }
580
581
            
581
 
            queries[i] = queries[i]->pushNegation(false, stats);
 
582
            queries[i] = queries[i]->pushNegation(stats, context, false, false);
582
583
 
583
584
            if(options.printstatistics)
584
585
            {
586
587
                stats.print(std::cout);
587
588
                std::cout << std::endl;
588
589
            }
 
590
 
589
591
            try {
590
592
                negstat_t stats;            
591
 
                queries[i] = (queries[i]->simplify(simplificationContext)).formula->pushNegation(false, stats);
 
593
                queries[i] = (queries[i]->simplify(simplificationContext)).formula->pushNegation(stats, context, false, false);
592
594
                if(options.printstatistics)
593
595
                {
594
596
                    std::cout << "RWSTATS POST:";
596
598
                    std::cout << std::endl;
597
599
                }
598
600
                queries[i].get()->setInvariant(isInvariant);
 
601
                std::cout << "RWSTATS POST:";
 
602
                stats.print(std::cout);
 
603
                std::cout << std::endl;
599
604
            } catch (std::bad_alloc& ba){
600
605
                std::cerr << "Query reduction failed." << std::endl;
601
606
                std::cerr << "Exception information: " << ba.what() << std::endl;