← Back to branch summary

~verifypn-stub/verifypn/upper-bounds

« back to all changes in this revision

Viewing changes to VerifyPN.cpp

enables reductions for CTL

Show diffs side-by-side

added added

removed removed

Lines of Context:
VerifyPN.cpp
656
656
 
657
657
        if(alldone) return SuccessCode;
658
658
    }
659
 
 
 
659
    
 
660
    //--------------------- Apply Net Reduction ---------------//
 
661
        
 
662
    if ( (options.enablereduction == 1 || options.enablereduction == 2) 
 
663
         && std::all_of(queries.begin(), queries.end(), [](auto& a){ return !a->containsNext(); })) {
 
664
        // Compute how many times each place appears in the query
 
665
        builder.startTimer();
 
666
        builder.reduce(queries, results, options.enablereduction, options.trace, nullptr, options.reductionTimeout);
 
667
        printer.setReducer(builder.getReducer());        
 
668
    }
 
669
    
 
670
    printStats(builder, options);
 
671
    
 
672
    auto net = std::unique_ptr<PetriNet>(builder.makePetriNet());
 
673
    
 
674
    for(auto& q : queries)
 
675
    {
 
676
        q->indexPlaces(builder.getPlaceNames());
 
677
    }
 
678
    
660
679
    //----------------------- Verify CTL queries -----------------------//
661
680
    std::vector<size_t> ctl_ids;
662
681
    for(size_t i = 0; i < queries.size(); ++i)
670
689
    if (ctl_ids.size() > 0) {
671
690
        options.isctl=true;
672
691
        PetriEngine::Reachability::Strategy reachabilityStrategy=options.strategy;
673
 
        std::unique_ptr<PetriNet> ctlnet(builder.makePetriNet());
 
692
 
674
693
        // Assign indexes
675
 
        if(queries.size() == 0 || contextAnalysis(builder, ctlnet.get(), queries) != ContinueCode)  return ErrorCode;
 
694
        if(queries.size() == 0 || contextAnalysis(builder, net.get(), queries) != ContinueCode)  return ErrorCode;
676
695
        if(options.strategy == DEFAULT) options.strategy = PetriEngine::Reachability::DFS;
677
696
        if(options.strategy != PetriEngine::Reachability::DFS){
678
697
            fprintf(stdout, "Search strategy was changed to DFS as the CTL engine is called.\n");
679
698
            options.strategy = PetriEngine::Reachability::DFS;
680
699
        }
681
 
        v = CTLMain(ctlnet.get(),
 
700
        v = CTLMain(net.get(),
682
701
            options.ctlalgorithm,
683
702
            options.strategy,
684
703
            options.gamemode,
687
706
            querynames,
688
707
            queries,
689
708
            ctl_ids);
690
 
                
 
709
 
691
710
        if (std::find(results.begin(), results.end(), ResultPrinter::Unknown) == results.end()) {
692
711
            return v;
693
712
        }
695
714
        options.strategy=reachabilityStrategy;
696
715
    }
697
716
    options.isctl=false;
698
 
    //--------------------- Apply Net Reduction ---------------//
699
 
        
700
 
    if (options.enablereduction == 1 || options.enablereduction == 2) {
701
 
        // Compute how many times each place appears in the query
702
 
        builder.startTimer();
703
 
        std::unique_ptr<PetriNet> net(builder.makePetriNet(false));
704
 
        builder.reduce(queries, results, options.enablereduction, options.trace, net.get(), options.reductionTimeout);
705
 
        printer.setReducer(builder.getReducer());        
706
 
    }
707
 
    
708
 
    printStats(builder, options);
709
 
    
710
 
    std::unique_ptr<PetriNet> net(builder.makePetriNet());
711
 
    
712
 
    for(auto& q : queries)
713
 
    {
714
 
        q->indexPlaces(builder.getPlaceNames());
715
 
    }
716
717
    
717
718
    //----------------------- Siphon Trap ------------------------//
718
719