<commit_before>// Copyright (c) 2003 Compaq Corporation.  All rights reserved.
// Portions Copyright (c) 2003 Microsoft Corporation.  All rights reserved.
// Last modified on Mon 30 Apr 2007 at 15:29:56 PST by lamport
//      modified on Thu Jan 10 11:22:26 PST 2002 by yuanyu

package tlc2.tool;

import java.io.PrintWriter;

import tla2sany.modanalyzer.SpecObj;
import tla2sany.semantic.SemanticNode;
import tlc2.TLCGlobals;
import tlc2.tool.liveness.LiveCheck1;
import tlc2.tool.liveness.LiveException;
import tlc2.util.ObjLongTable;
import tlc2.util.RandomGenerator;
import util.FileUtil;
import util.FilenameToStream;
import util.ToolIO;

public class Simulator implements Cancelable{

    /* Constructors  */
    /**
     * SZ Feb 20, 2009: added the possibility to pass the SpecObject, this is compatibility constructor
     * @deprecated use {@link Simulator#Simulator(String, String, String, boolean, int, long, RandomGenerator, long, boolean, FilenameToStream, SpecObj)} instead
     * and pass the <code>null</code> as SpecObj
     */
    public Simulator(String specFile, String configFile, String traceFile, boolean deadlock, int traceDepth,
            long traceNum, RandomGenerator rng, long seed, boolean preprocess, FilenameToStream resolver)
    {
        this(specFile, configFile, traceFile, deadlock, traceDepth, traceNum, rng, seed, preprocess, resolver, null);
    }
    
    // SZ Feb 20, 2009: added the possibility to pass the SpecObject    
    public Simulator(String specFile, String configFile, String traceFile,
		   boolean deadlock, int traceDepth, long traceNum,
		   RandomGenerator rng, long seed, boolean preprocess, FilenameToStream resolver, SpecObj specObj) {
    int lastSep = specFile.lastIndexOf(FileUtil.separatorChar);
    String specDir = (lastSep == -1) ? "" : specFile.substring(0, lastSep+1);
    specFile = specFile.substring(lastSep+1);
    this.tool = new Tool(specDir, specFile, configFile, resolver);
    // SZ Feb 24, 2009: setup the user directory
    ToolIO.setUserDir(specDir);

    this.tool.init(preprocess, specObj);   // parse and process the spec

    this.checkDeadlock = deadlock;
    this.checkLiveness = !this.tool.livenessIsTrue();
    this.actions = this.tool.getActions();
    this.invariants = this.tool.getInvariants();
    this.impliedActions = this.tool.getImpliedActions();
    this.numOfGenStates = 0;
    if (traceDepth != -1) {<commit_msg>fixed the NPE<commit_after>// Copyright (c) 2003 Compaq Corporation.  All rights reserved.
// Portions Copyright (c) 2003 Microsoft Corporation.  All rights reserved.
// Last modified on Mon 30 Apr 2007 at 15:29:56 PST by lamport
//      modified on Thu Jan 10 11:22:26 PST 2002 by yuanyu

package tlc2.tool;

import java.io.PrintWriter;

import tla2sany.modanalyzer.SpecObj;
import tla2sany.semantic.SemanticNode;
import tlc2.TLCGlobals;
import tlc2.tool.liveness.LiveCheck1;
import tlc2.tool.liveness.LiveException;
import tlc2.util.ObjLongTable;
import tlc2.util.RandomGenerator;
import util.FileUtil;
import util.FilenameToStream;
import util.ToolIO;

public class Simulator implements Cancelable{

    /* Constructors  */
    /**
     * SZ Feb 20, 2009: added the possibility to pass the SpecObject, this is compatibility constructor
     * @deprecated use {@link Simulator#Simulator(String, String, String, boolean, int, long, RandomGenerator, long, boolean, FilenameToStream, SpecObj)} instead
     * and pass the <code>null</code> as SpecObj
     */
    public Simulator(String specFile, String configFile, String traceFile, boolean deadlock, int traceDepth,
            long traceNum, RandomGenerator rng, long seed, boolean preprocess, FilenameToStream resolver)
    {
        this(specFile, configFile, traceFile, deadlock, traceDepth, traceNum, rng, seed, preprocess, resolver, null);
    }
    
    // SZ Feb 20, 2009: added the possibility to pass the SpecObject    
    public Simulator(String specFile, String configFile, String traceFile,
		   boolean deadlock, int traceDepth, long traceNum,
		   RandomGenerator rng, long seed, boolean preprocess, FilenameToStream resolver, SpecObj specObj) {
    int lastSep = specFile.lastIndexOf(FileUtil.separatorChar);
    String specDir = (lastSep == -1) ? "" : specFile.substring(0, lastSep+1);
    specFile = specFile.substring(lastSep+1);

    // SZ Feb 24, 2009: setup the user directory
    // SZ Mar 5, 2009: removed it again because of the bug in simulator
    // ToolIO.setUserDir(specDir);
    
    this.tool = new Tool(specDir, specFile, configFile, resolver);

    this.tool.init(preprocess, specObj);   // parse and process the spec

    this.checkDeadlock = deadlock;
    this.checkLiveness = !this.tool.livenessIsTrue();
    this.actions = this.tool.getActions();
    this.invariants = this.tool.getInvariants();
    this.impliedActions = this.tool.getImpliedActions();
    this.numOfGenStates = 0;
    if (traceDepth != -1) {
{'fraction_non_alphanumeric': 0.09477323571283303, 'fraction_numerical': 0.027455765710799267, 'mean_word_length': 3.9676767676767675, 'pattern_counts': {'":': 0, '<': 7, '<?xml version=': 0, '>': 7, 'https://': 0, 'lorem ipsum': 0, 'www.': 0, 'xml': 0}, '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': '4026011', 'n_tokens_mistral': 1593, 'n_tokens_neox': 1467, 'n_words': 455}