<commit_before>#!/usr/bin/env python

'''
smc [OPTIONS] PNML FORMULA

The Simple Model Checker is a bounded CTL model checker

PNML is the path to a PNML file
FORMULA is the path to an XML file containing formulas (MCC 2015 format)

And OPTIONS is zero or more of the following options

 --max-depth=N
   Maximum length of a firing sequence that will be explored when
   constructing the bounded fragment of the state space that the model
   checker uses to evaluate each formula.

 --max-states=N
   Limit on the number of markings that the initial fragment of the
   reachability graph considered by this tool will have.

 --mcc15-stop-after=N
   Stop verifying formulas from the formula file FORMULA after having found
   N formulas for which the tool was unable to decide

 --help
   Prints this message
'''

try :
    import os
    import sys
    import time
    import argparse
    import networkx
    import xml.etree.ElementTree
except Exception, e:
    print 'ERROR!'
    print 'It seems that your python installation is missing some package.'
    print 'This tool requires, among others, argparse, and networkx'
    print 'The runtime reported the following error:\n\n', str (e)
    print 'You might want to use "easy_install --user PACKAGE"'
    sys.exit (1)
finally :
    if sys.version_info < (2, 7, 0) or sys.version_info >= (3, 0, 0) :
        print ("")
        print ("*** ERROR ***")
        print ("This tool relies on Python 2.7!!")
        print ("Install Python 2.7 or modify the first line of the file 'smc.py' so that it calls Python 2.7")
        print ("")
        sys.exit (1)

import ptnet

class BoundedSearch :

    # outcome of the CTL verification algorithm
    RESULT_SAT   = 'SAT'
    RESULT_UNSAT = 'UNSAT'
    RESULT_UNDEF = '?'

    def __init__ (self, net) :
        self.net = net
        self.max_depth = 3
        self.max_states = 9000
        self.states = networkx.DiGraph ()
        self.init_state = net.m0
        self.__new_mark = 0
        self.__state_space_built = False

        self.stats_nr_states = 0
        self.stats_nr_states_fe = 0
        self.stats_nr_edges = 0
        self.stats_depth = 0
        self.stats_stop_reason = "'full state space'"

    def new_mark (self) :
        self.__new_mark += 1
        return self.__new_mark

    def find_and_insert (self, marking) :
        try :
            return self.states.node[marking]['org']
        except KeyError :
            self.states.add_node (marking, org=marking)
            return marking

    def build_state_space (self) :

        if self.__state_space_built : return

        # enable structural marking equality, rather than just checking the pointer id()
        ptnet.Marking.frozen_eq = False

        assert (self.init_state == self.net.m0)
        curr_depth = 0
        self.find_and_insert (self.init_state)
        layer = list ([self.init_state])
        next_layer = list ()

        # bread-first search on the state space
        print "smc: constructing state space"
        print "smc: limits: maximum depth:", self.max_depth
        print "smc: limits: maximum nr. of states:", self.max_states
        while (len (self.states) < self.max_states
                and curr_depth < self.max_depth
                and len (layer) >= 1) :
            print 'smc: build: so far', len(self.states), 'markings found'
            print 'smc: build: expanding', len (layer), 'markings at depth', curr_depth
            for marking in layer :
                #print 'smc: build: expanding marking', repr (marking)
                if (marking.fully_expanded) : continue
                make_fully_expanded = True
                for t in self.net.enabled (marking) :
                    #print "smc: firing transition %s" % str (t)
                    new_marking = self.net.fire (marking, t)
                    new_canon_marking = self.find_and_insert (new_marking)
                    #print 'smc: build: - adding edge to', repr (new_canon_marking), 'trans', repr (t)
                    self.states.add_edge (marking, new_canon_marking, trans=t)
                    if not new_canon_marking.fully_expanded : next_layer.append (new_canon_marking)
                    if len (self.states) >= self.max_states :
                        make_fully_expanded = False
                        break
                if make_fully_expanded :
                    marking.fully_expanded = True
                    self.stats_nr_states_fe += 1
                else :
                    curr_depth -= 1 # avoids bad reporting of reason 
                    break
            curr_depth += 1
            layer = next_layer
            next_layer = list ()

        self.__state_space_built = True
        self.stats_nr_states = self.states.number_of_nodes ()
        self.stats_nr_edges = self.states.number_of_edges ()
        self.stats_depth = curr_depth
        if curr_depth >= self.max_depth :
            self.stats_stop_reason = "'exceeded depth'"
        if len (self.states) >= self.max_states :
            self.stats_stop_reason = "'exceeded number of states'"

        print "smc: done,", \
            self.stats_nr_states, "states,", \
            self.stats_nr_states - self.stats_nr_states_fe, "not fully expanded,", \
            self.stats_nr_edges, "edges,", \
            self.stats_depth, "complete steps deep"
        print "smc: state-space construction terminated due to", self.stats_stop_reason
<commit_msg>smc: bug fixed: prevented state space construction<commit_after>#!/usr/bin/env python

'''
smc [OPTIONS] PNML FORMULA

The Simple Model Checker is a bounded CTL model checker

PNML is the path to a PNML file
FORMULA is the path to an XML file containing formulas (MCC 2015 format)

And OPTIONS is zero or more of the following options

 --max-depth=N
   Maximum length of a firing sequence that will be explored when
   constructing the bounded fragment of the state space that the model
   checker uses to evaluate each formula.

 --max-states=N
   Limit on the number of markings that the initial fragment of the
   reachability graph considered by this tool will have.

 --mcc15-stop-after=N
   Stop verifying formulas from the formula file FORMULA after having found
   N formulas for which the tool was unable to decide

 --help
   Prints this message
'''

try :
    import os
    import sys
    import time
    import argparse
    import networkx
    import xml.etree.ElementTree
except Exception, e:
    print 'ERROR!'
    print 'It seems that your python installation is missing some package.'
    print 'This tool requires, among others, argparse, and networkx'
    print 'The runtime reported the following error:\n\n', str (e)
    print 'You might want to use "easy_install --user PACKAGE"'
    sys.exit (1)
finally :
    if sys.version_info < (2, 7, 0) or sys.version_info >= (3, 0, 0) :
        print ("")
        print ("*** ERROR ***")
        print ("This tool relies on Python 2.7!!")
        print ("Install Python 2.7 or modify the first line of the file 'smc.py' so that it calls Python 2.7")
        print ("")
        sys.exit (1)

import ptnet

class BoundedSearch :

    # outcome of the CTL verification algorithm
    RESULT_SAT   = 'SAT'
    RESULT_UNSAT = 'UNSAT'
    RESULT_UNDEF = '?'

    def __init__ (self, net) :
        self.net = net
        self.max_depth = 3
        self.max_states = 9000
        self.states = networkx.DiGraph ()
        self.init_state = net.m0.clone ()
        self.__new_mark = 0
        self.__state_space_built = False

        self.stats_nr_states = 0
        self.stats_nr_states_fe = 0
        self.stats_nr_edges = 0
        self.stats_depth = 0
        self.stats_stop_reason = "'full state space'"

    def new_mark (self) :
        self.__new_mark += 1
        return self.__new_mark

    def find_and_insert (self, marking) :
        try :
            return self.states.node[marking]['org']
        except KeyError :
            self.states.add_node (marking, org=marking)
            return marking

    def build_state_space (self) :

        if self.__state_space_built : return

        # enable structural marking equality, rather than just checking the pointer id()
        ptnet.Marking.frozen_eq = False

        assert (self.init_state == self.net.m0)
        curr_depth = 0
        self.find_and_insert (self.init_state)
        layer = list ([self.init_state])
        next_layer = list ()

        # bread-first search on the state space
        print "smc: -----"
        print "smc: constructing state space"
        print "smc: limits: maximum depth:", self.max_depth
        print "smc: limits: maximum nr. of states:", self.max_states
        while (len (self.states) < self.max_states
                and curr_depth < self.max_depth
                and len (layer) >= 1) :
            print 'smc: build: so far', len(self.states), 'markings found'
            print 'smc: build: expanding', len (layer), 'markings at depth', curr_depth
            for marking in layer :
                #print 'smc: build: expanding marking', repr (marking)
                if (marking.fully_expanded) : continue
                make_fully_expanded = True
                for t in self.net.enabled (marking) :
                    #print "smc: firing transition %s" % str (t)
                    new_marking = self.net.fire (marking, t)
                    new_canon_marking = self.find_and_insert (new_marking)
                    #print 'smc: build: - adding edge to', repr (new_canon_marking), 'trans', repr (t)
                    self.states.add_edge (marking, new_canon_marking, trans=t)
                    if not new_canon_marking.fully_expanded : next_layer.append (new_canon_marking)
                    if len (self.states) >= self.max_states :
                        make_fully_expanded = False
                        break
                if make_fully_expanded :
                    marking.fully_expanded = True
                    self.stats_nr_states_fe += 1
                else :
                    curr_depth -= 1 # avoids bad reporting of reason 
                    break
            curr_depth += 1
            layer = next_layer
            next_layer = list ()

        self.__state_space_built = True
        self.stats_nr_states = self.states.number_of_nodes ()
        self.stats_nr_edges = self.states.number_of_edges ()
        self.stats_depth = curr_depth
        if curr_depth >= self.max_depth :
            self.stats_stop_reason = "'exceeded depth'"
        if len (self.states) >= self.max_states :
            self.stats_stop_reason = "'exceeded number of states'"

        print "smc: build: done,", \
            self.stats_nr_states, "states,", \
            self.stats_nr_states - self.stats_nr_states_fe, "not fully expanded,", \
            self.stats_nr_edges, "edges,", \
            self.stats_depth, "complete steps deep"
        print "smc: state-space construction terminated due to", self.stats_stop_reason

{'fraction_non_alphanumeric': 0.08321194464675892, 'fraction_numerical': 0.006919155134741442, 'mean_word_length': 2.0943661971830987, 'pattern_counts': {'":': 0, '<': 9, '<?xml version=': 0, '>': 13, 'https://': 0, 'lorem ipsum': 0, 'www.': 0, 'xml': 2}, 'pii_count': 0, 'substrings_counts': 0, 'word_list_counts': {'cursed_substrings.json': 0, 'profanity_word_list.json': 0, 'sexual_word_list.json': 0, 'zh_pornsignals.json': 0}}
{'dir': 'git-commits-cleaned', 'id': '700878', 'n_tokens_mistral': 3292, 'n_tokens_neox': 3105, 'n_words': 1019}