Inconsistent with document description

[dejavu6]

Hello, I have encountered the following problems:

First question:
The content of my source file is:

   import torch
   import torch.nn as nn

  class Net(nn.Module):
      def __init__(self):
          super(Net, self).__init__()
          self.layers = nn.Sequential(
              nn.Linear(28 * 28, 120),
              nn.ReLU(),
              nn.Linear(80, 10))
  
      def a(self):
          pass

    if __name__ == "__main__":
        n = Net()

But when I execute the command, I get the following results:

There should be a problem with defining shape in this model.

Second question:
I used it https://github.com/pytorch/examples/blob/master/mnist/main.py , but the command is stuck and no result is returned. As follows:

[MerHS]

Question 1.

PyTea does not check a network which is not executed, analogous to the real PyTorch.
Since your code will not raise an error (i.e. will not crash) as the forward is not called, PyTea does not inform you an error.

Question 2.

PyTea uses given default command-line options defined in argparse methods. The default epoch count is set to 14 from main.py, so PyTea analyzes complete 14 loops of training. (From our paper, every benchmark is tested with a single epoch)

Please make pyteaconfig.json in the directory of the main script is placed. Its content should be like below:

{
    "pythonCmdArgs": {
        "epochs": 1
    }
}

With this setting, the result from my laptop is shown below:

$ time python bin/pytea.py test/test.py
node /Users/kinetc/work/pytea/bin/index.js test/test.py   --resultPath=/var/folders/28/s29mmm495w9_syn5tb9gws1h0000gn/T/tmppsdvzwid/constraint.json
analyzer starts!

------------- constraint generator result -------------

success path #1

REDUCED HEAP: (size: 6073 values)
  nn => [530]{ <46 attrs>, {}, {} }
  F => [563]{ <23 attrs>, {}, {} }
  transforms => [2318]{ <17 attrs>, {}, {} }
  train => train$TMP$(args, model, device, train_loader, optimizer, epoch)
  print_function => print$TMP$(value)
  test => test$TMP$(model, device, test_loader)
  StepLR => [1200]{ { __call__ => StepLR$__call__($args, $kwargs), __init__ => StepLR$__init__(self, $args, $kwargs), __mro__ => Loc(1204), __name__ => "StepLR", __new__ => StepLR$__new__(cls) }, {}, {} }
  optim => [1175]{ { Adadelta => Loc(1181), Adam => Loc(1180), LBFGS => Loc(1177), Optimizer => Loc(1178), SGD => Loc(1179), lr_scheduler => Loc(1182) }, {}, {} }
  main => main$TMP$()
  datasets => [2246]{ { CIFAR10 => Loc(2250), CIFAR100 => Loc(2249), ImageFolder => Loc(2248), MNIST => Loc(2251) }, {}, {} }
  Net => [2442]{ { __call__ => Net$__call__(), __init__ => Net$__init__(self), __mro__ => Loc(2447), __name__ => "Net", __new__ => Net$__new__(cls), forward => Net$forward(self, x) }, {}, {} }

LOGS:


CONSTRAINTS:
1: (0 <= for$ident_I4) - [59:28 - 59:39] (/Users/kinetc/work/pytea/test/test.py:59:28)
2: (for$ident_I4 <= 10) - [59:28 - 59:39] (/Users/kinetc/work/pytea/test/test.py:59:28)
3: (0 <= MNIST_Class_I5) - [31:17 - 31:62] (/Users/kinetc/work/pytea/bin/dist/pylib/torchvision/datasets/mnist.py:31:17)
4: (MNIST_Class_I5 <= 9) - [31:17 - 31:62] (/Users/kinetc/work/pytea/bin/dist/pylib/torchvision/datasets/mnist.py:31:17)

<OVERALL: total 1 paths>
potential success path #: 1
potential unreachable path #: 0
immediate failed path #: 0

PROCESS TIMES:
  Translate library scripts: 1.9556s
  Translate project scripts: 0.0070s
  Running builtin libraries: 0.2691s
  Running entry file: 0.8259s
  printing results: 0.0065s

------------- z3 result -------------
<OVERALL: total 1 paths>
  Valid paths (no constraint error): 1
python bin/pytea.py test/test.py  4.87s user 0.24s system 128% cpu 3.984 total

[dejavu6]

Thank you for your answer. I tried. It's true. It solved my question