torxakis / torxakis Goto Github PK

TorXakis can run in 3 different modes: stepper, tester and simulator. Command files that use these modes should be named accordingly.

DisPro txscmd files are named as "_Sut" but they should have been "_Tester" since they include tester commands.

We don't know how consistent our examples are about this. It should be reviewed and fixed wherever necessary.

Testing a spec + test purpose makes them go out of sync, as the 'ivstat' of the channels in the test purpose are one higher than the 'ivstat' of the channels in the model during the same testing step (based on observing the currently printed debugging info). This causes the conjunction of the model and test purpose channels (menuConjunct in CoreUtils.hs) to be empty, as "ctoffs1 == ctoffs2" is then never true. Only happens after the first input (for which this issue does not occur). TorXakis then thus always waits for outputs, instead of providing an input allowed by both model and test purpose. I attached a simple model which shows the issue with 'tester Model Purp Sut', 'test 10'

DoubleStimulusResponse.txt

(This issue was found after the quick fix for issue #44 which I mentioned in the comments, so there is a small chance that it is caused by a wrong fix for #44).

Currently the SMT solver to be used is hard-wired in TxsCore at txsInit. We need to make this configurable when starting TorXakis.

Blocks #28.

Every file in the TorXakis repository should contain the copyright notice.
I noticed that all *.yaml files do not contain a copyright notice.
Are these the only ones?
Please add copyright notice + include in copyright check (test\copyright\Copyright.java)

We need to get an idea on the percentage of code covered by our unit tests, and its evolution on time so that we can track the improvements. Coveralls provides integration with Travis, so we can use this.

Just triggers DatChecker on the output file

First 3 steps are in test/Makefile

sys\server\src\TxsServer.hs

Line 252:

cmdStop :: String -> IOS.IOS ()
cmdStop _  =  do
     World.closeSockets
     modus <- gets IOS.modus
     if  IOS.isSimuled modus
       then do [(nmsut,valsut)] <- IOS.getParams ["param_Sut_deltaTime"]
               [(nmsim,valsim)] <- IOS.getParams ["param_Sim_deltaTime"]
==>            IOS.setParams [("param_Sut_deltaTime",valsim)]
==>            IOS.setParams [("param_Sim_deltaTime",valsut)]
…

Shown lines swap delta time values of sim and sut.

TXSSERVER RSP << MACK .....9: Act { { ( Job, [ JobData(-17,"gy,�txsserver.exe: : hPutChar: invalid argument (invalid character)

Z3 SMT log:
(($Job$1544$-1$1$ (JobData$JobData 1 "╠" (- 23) 70)))

To remove TxsDef, we need to remove DefNo first.

All the sockets and file descriptors should be properly closed, even in the presence of asynchronous exceptions.

strategy:

• Add -Werror to all cabal packages (ghc-options)
• Add -Wall to all files that have no warnings. I.e. add {-# OPTIONS -Wall #-}.
• Add -Wall to all packages (ghc-options) when all files can be compiled with -Wall.
  Of course, remove the -Wall options field from all files in the package.

Looks like in case of a failure due to #50, TorXakis server releases the port only after its parent process exits. If parent process launches another TorXakis server without exiting, then the port is stuck as occupied by a non-existing process.

To reproduce, checkout 6e450ce and run:

> %TXSREPO%\test\examps\LuckyPeople\TestLuckyPeople.bat %TXSREPO%

You will have to kill txsui.exe. Next time you run the same command, TorXakis server won't be able to start since the port is occupied.

Start PowerShell and run:

netstat -aon | findstr 9876

Output will be something like this:

TCP 0.0.0.0:9876 0.0.0.0:0 LISTENING 7676
TCP [::]:9876 [::]:0 LISTENING 7676

7676 is the supposed process Id in my case. But if you try to find it:

$> ps -Id 7676
ps : Cannot find a process with the process identifier 7676.

$>kill 7676
kill : Cannot find a process with the process identifier 7676.

Hlint warnings should be zero.

After adding instances for NFData to the different data-types in defs the compilation times went from 1 hour (which was already high) to 1.5 hours! This will hamper our development speed. Some action must be taken.

I see the following options:

• Use a memory structure that is input to the other compilation phases (in this way the parser does not depend on any other TorXakis package, and TorXakis is independent of the parser used).
• Split the parsers into smaller parsers.
• Use parse-combinators.

DisPro10-data, DisPro12-unique-id, DisPro12-unique-id_Wrong, DisPro12-unique-id_Right cases fail.

Dispro10:

TXS >> c:\Repos\TorXakis\examps\DispatchProcess\spec\DisPro10-data.txs
TXS << TXS >> Tester started
TXS << TXS >> .....1: IN: Act { { ( Job, [ JobData(28,"TM0t",46,71) ] ) } }
TXS >> .....2: IN: Act { { ( Job, [ JobData(32,"PP2",79,58) ] ) } }
TXS >> .....3: IN: Act { { ( Job, [ JobData(44,"KT4dh",56,43) ] ) } }
** TXS >> eval: ASF **
TXS >> .....4: OUT: Act { { ( Finish, [ ERROR ] ) } }
TXS >> Expected:
TXS >> [ ( { Finish[ $Finish$1420$2$1$ ] }, [], [ ( JobOut(32,4,1) == $Finish$1420$2$1$ ) ] ) ( { Finish[ $Finish$1420$2$1$ ] }, [], [ ( JobOut(28,5,1) == $Finish$1420$2$1$ ) ] ) ( { Finish[ $Finish$1420$2$1$ ] }, [ $Job2Proc$$$1393$49$2$1$ ], [ ( JobOut(32,4,1) == $Finish$1420$2$1$ ) ( JobData(44,"KT4dh",56,43) == $Job2Proc$$$1393$49$2$1$ ) ] ) ( { Finish[ $Finish$1420$2$1$ ] }, [ $Job2Proc$$$1393$50$2$1$ ], [ ( JobOut(32,4,1) == $Finish$1420$2$1$ ) ( JobData(44,"KT4dh",56,43) == $Job2Proc$$$1393$50$2$1$ ) ] ) ( { Finish[ $Finish$1420$2$1$ ] }, [ $Job2Proc$$$1393$51$2$1$ ], [ ( JobOut(32,4,1) == $Finish$1420$2$1$ ) ( JobData(44,"KT4dh",56,43) == $Job2Proc$$$1393$51$2$1$ ) ] ) ( { Finish[ $Finish$1420$2$1$ ] }, [ $Job2Proc$$$1393$52$2$1$ ], [ ( JobOut(28,5,1) == $Finish$1420$2$1$ ) ( JobData(44,"KT4dh",56,43) == $Job2Proc$$$1393$52$2$1$ ) ] ) ( { Finish[ $Finish$1420$2$1$ ] }, [ $Job2Proc$$$1393$53$2$1$ ], [ ( JobOut(28,5,1) == $Finish$1420$2$1$ ) ( JobData(44,"KT4dh",56,43) == $Job2Proc$$$1393$53$2$1$ ) ] ) ( { Finish[ $Finish$1420$2$1$ ] }, [ $Job2Proc$$$1393$54$2$1$ ], [ ( JobOut(28,5,1) == $Finish$1420$2$1$ ) ( JobData(44,"KT4dh",56,43) == $Job2Proc$$$1393$54$2$1$ ) ] ) ( { Finish[ $Finish$1420$2$1$ ] }, [], [ ( JobOut(32,3,1) == $Finish$1420$2$1$ ) ] ) ( { Finish[ $Finish$1420$2$1$ ] }, [], [ ( JobOut(28,5,1) == $Finish$1420$2$1$ ) ] ) ( { Finish[ $Finish$1420$2$1$ ] }, [ $Job2Proc$$$1393$57$2$1$ ], [ ( JobOut(32,3,1) == $Finish$1420$2$1$ ) ( JobData(44,"KT4dh",56,43) == $Job2Proc$$$1393$57$2$1$ ) ] ) ( { Finish[ $Finish$1420$2$1$ ] }, [ $Job2Proc$$$1393$58$2$1$ ], [ ( JobOut(32,3,1) == $Finish$1420$2$1$ ) ( JobData(44,"KT4dh",56,43) == $Job2Proc$$$1393$58$2$1$ ) ] ) ( { Finish[ $Finish$1420$2$1$ ] }, [ $Job2Proc$$$1393$60$2$1$ ], [ ( JobOut(32,3,1) == $Finish$1420$2$1$ ) ( JobData(44,"KT4dh",56,43) == $Job2Proc$$$1393$60$2$1$ ) ] ) ( { Finish[ $Finish$1420$2$1$ ] }, [ $Job2Proc$$$1393$61$2$1$ ], [ ( JobOut(28,5,1) == $Finish$1420$2$1$ ) ( JobData(44,"KT4dh",56,43) == $Job2Proc$$$1393$61$2$1$ ) ] ) ( { Finish[ $Finish$1420$2$1$ ] }, [ $Job2Proc$$$1393$62$2$1$ ], [ ( JobOut(28,5,1) == $Finish$1420$2$1$ ) ( JobData(44,"KT4dh",56,43) == $Job2Proc$$$1393$62$2$1$ ) ] ) ( { Finish[ $Finish$1420$2$1$ ] }, [ $Job2Proc$$$1393$63$2$1$ ], [ ( JobOut(28,5,1) == $Finish$1420$2$1$ ) ( JobData(44,"KT4dh",56,43) == $Job2Proc$$$1393$63$2$1$ ) ] ) ( { Finish[ $Finish$1420$2$1$ ] }, [], [ ( JobOut(32,2,1) == $Finish$1420$2$1$ ) ] ) ( { Finish[ $Finish$1420$2$1$ ] }, [], [ ( JobOut(28,5,1) == $Finish$1420$2$1$ ) ] ) ( { Finish[ $Finish$1420$2$1$ ] }, [ $Job2Proc$$$1393$65$2$1$ ], [ ( JobOut(32,2,1) == $Finish$1420$2$1$ ) ( JobData(44,"KT4dh",56,43) == $Job2Proc$$$1393$65$2$1$ ) ] ) ( { Finish[ $Finish$1420$2$1$ ] }, [ $Job2Proc$$$1393$67$2$1$ ], [ ( JobOut(32,2,1) == $Finish$1420$2$1$ ) ( JobData(44,"KT4dh",56,43) == $Job2Proc$$$1393$67$2$1$ ) ] ) ( { Finish[ $Finish$1420$2$1$ ] }, [ $Job2Proc$$$1393$69$2$1$ ], [ ( JobOut(32,2,1) == $Finish$1420$2$1$ ) ( JobData(44,"KT4dh",56,43) == $Job2Proc$$$1393$69$2$1$ ) ] ) ( { Finish[ $Finish$1420$2$1$ ] }, [ $Job2Proc$$$1393$70$2$1$ ], [ ( JobOut(28,5,1) == $Finish$1420$2$1$ ) ( JobData(44,"KT4dh",56,43) == $Job2Proc$$$1393$70$2$1$ ) ] ) ( { Finish[ $Finish$1420$2$1$ ] }, [ $Job2Proc$$$1393$71$2$1$ ], [ ( JobOut(28,5,1) == $Finish$1420$2$1$ ) ( JobData(44,"KT4dh",56,43) == $Job2Proc$$$1393$71$2$1$ ) ] ) ( { Finish[ $Finish$1420$2$1$ ] }, [ $Job2Proc$$$1393$72$2$1$ ], [ ( JobOut(28,5,1) == $Finish$1420$2$1$ ) ( JobData(44,"KT4dh",56,43) == $Job2Proc$$$1393$72$2$1$ ) ] ) ( { Finish[ $Finish$1420$2$1$ ] }, [], [ ( JobOut(32,1,1) == $Finish$1420$2$1$ ) ] ) ( { Finish[ $Finish$1420$2$1$ ] }, [], [ ( JobOut(28,5,1) == $Finish$1420$2$1$ ) ] ) ( { Finish[ $Finish$1420$2$1$ ] }, [ $Job2Proc$$$1393$74$2$1$ ], [ ( JobOut(32,1,1) == $Finish$1420$2$1$ ) ( JobData(44,"KT4dh",56,43) == $Job2Proc$$$1393$74$2$1$ ) ] ) ( { Finish[ $Finish$1420$2$1$ ] }, [ $Job2Proc$$$1393$76$2$1$ ], [ ( JobOut(32,1,1) == $Finish$1420$2$1$ ) ( JobData(44,"KT4dh",56,43) == $Job2Proc$$$1393$76$2$1$ ) ] ) ( { Finish[ $Finish$1420$2$1$ ] }, [ $Job2Proc$$$1393$78$2$1$ ], [ ( JobOut(32,1,1) == $Finish$1420$2$1$ ) ( JobData(44,"KT4dh",56,43) == $Job2Proc$$$1393$78$2$1$ ) ] ) ( { Finish[ $Finish$1420$2$1$ ] }, [ $Job2Proc$$$1393$79$2$1$ ], [ ( JobOut(28,5,1) == $Finish$1420$2$1$ ) ( JobData(44,"KT4dh",56,43) == $Job2Proc$$$1393$79$2$1$ ) ] ) ( { Finish[ $Finish$1420$2$1$ ] }, [ $Job2Proc$$$1393$80$2$1$ ], [ ( JobOut(28,5,1) == $Finish$1420$2$1$ ) ( JobData(44,"KT4dh",56,43) == $Job2Proc$$$1393$80$2$1$ ) ] ) ( { Finish[ $Finish$1420$2$1$ ] }, [ $Job2Proc$$$1393$81$2$1$ ], [ ( JobOut(28,5,1) == $Finish$1420$2$1$ ) ( JobData(44,"KT4dh",56,43) == $Job2Proc$$$1393$81$2$1$ ) ] ) ( { Finish[ $Finish$1420$2$1$ ] }, [], [ ( JobOut(32,3,1) == $Finish$1420$2$1$ ) ] ) ( { Finish[ $Finish$1420$2$1$ ] }, [], [ ( JobOut(28,4,1) == $Finish$1420$2$1$ ) ] ) ( { Finish[ $Finish$1420$2$1$ ] }, [ $Job2Proc$$$1393$84$2$1$ ], [ ( JobOut(32,3,1) == $Finish$1420$2$1$ ) ( JobData(44,"KT4dh",56,43) == $Job2Proc$$$1393$84$2$1$ ) ] ) ( { Finish[ $Finish$1420$2$1$ ] }, [ $Job2Proc$$$1393$85$2$1$ ], [ ( JobOut(32,3,1) == $Finish$1420$2$1$ ) ( JobData(44,"KT4dh",56,43) == $Job2Proc$$$1393$85$2$1$ ) ] ) ( { Finish[ $Finish$1420$2$1$ ] }, [ $Job2Proc$$$1393$86$2$1$ ], [ ( JobOut(28,4,1) == $Finish$1420$2$1$ ) ( JobData(44,"KT4dh",56,43) == $Job2Proc$$$1393$86$2$1$ ) ] ) ( { Finish[ $Finish$1420$2$1$ ] }, [ $Job2Proc$$$1393$87$2$1$ ], [ ( JobOut(28,4,1) == $Finish$1420$2$1$ ) ( JobData(44,"KT4dh",56,43) == $Job2Proc$$$1393$87$2$1$ ) ] ) ( { Finish[ $Finish$1420$2$1$ ] }, [ $Job2Proc$$$1393$89$2$1$ ], [ ( JobOut(32,3,1) == $Finish$1420$2$1$ ) ( JobData(44,"KT4dh",56,43) == $Job2Proc$$$1393$89$2$1$ ) ] ) ( { Finish[ $Finish$1420$2$1$ ] }, [ $Job2Proc$$$1393$90$2$1$ ], [ ( JobOut(28,4,1) == $Finish$1420$2$1$ ) ( JobData(44,"KT4dh",56,43) == $Job2Proc$$$1393$90$2$1$ ) ] ) ( { Finish[ $Finish$1420$2$1$ ] }, [], [ ( JobOut(32,2,1) == $Finish$1420$2$1$ ) ] ) ( { Finish[ $Finish$1420$2$1$ ] }, [], [ ( JobOut(28,4,1) == $Finish$1420$2$1$ ) ] ) ( { Finish[ $Finish$1420$2$1$ ] }, [ $Job2Proc$$$1393$92$2$1$ ], [ ( JobOut(32,2,1) == $Finish$1420$2$1$ ) ( JobData(44,"KT4dh",56,43) == $Job2Proc$$$1393$92$2$1$ ) ] ) ( { Finish[ $Finish$1420$2$1$ ] }, [ $Job2Proc$$$1393$94$2$1$ ], [ ( JobOut(32,2,1) == $Finish$1420$2$1$ ) ( JobData(44,"KT4dh",56,43) == $Job2Proc$$$1393$94$2$1$ ) ] ) ( { Finish[ $Finish$1420$2$1$ ] }, [ $Job2Proc$$$1393$95$2$1$ ], [ ( JobOut(28,4,1) == $Finish$1420$2$1$ ) ( JobData(44,"KT4dh",56,43) == $Job2Proc$$$1393$95$2$1$ ) ] ) ( { Finish[ $Finish$1420$2$1$ ] }, [ $Job2Proc$$$1393$96$2$1$ ], [ ( JobOut(28,4,1) == $Finish$1420$2$1$ ) ( JobData(44,"KT4dh",56,43) == $Job2Proc$$$1393$96$2$1$ ) ] ) ( { Finish[ $Finish$1420$2$1$ ] }, [ $Job2Proc$$$1393$98$2$1$ ], [ ( JobOut(32,2,1) == $Finish$1420$2$1$ ) ( JobData(44,"KT4dh",56,43) == $Job2Proc$$$1393$98$2$1$ ) ] ) ( { Finish[ $Finish$1420$2$1$ ] }, [ $Job2Proc$$$1393$99$2$1$ ], [ ( JobOut(28,4,1) == $Finish$1420$2$1$ ) ( JobData(44,"KT4dh",56,43) == $Job2Proc$$$1393$99$2$1$ ) ] ) ( { Finish[ $Finish$1420$2$1$ ] }, [], [ ( JobOut(32,1,1) == $Finish$1420$2$1$ ) ] ) ( { Finish[ $Finish$1420$2$1$ ] }, [], [ ( JobOut(28,4,1) == $Finish$1420$2$1$ ) ] ) ( { Finish[ $Finish$1420$2$1$ ] }, [ $Job2Proc$$$1393$101$2$1$ ], [ ( JobOut(32,1,1) == $Finish$1420$2$1$ ) ( JobData(44,"KT4dh",56,43) == $Job2Proc$$$1393$101$2$1$ ) ] ) ( { Finish[ $Finish$1420$2$1$ ] }, [ $Job2Proc$$$1393$103$2$1$ ], [ ( JobOut(32,1,1) == $Finish$1420$2$1$ ) ( JobData(44,"KT4dh",56,43) == $Job2Proc$$$1393$103$2$1$ ) ] ) ( { Finish[ $Finish$1420$2$1$ ] }, [ $Job2Proc$$$1393$104$2$1$ ], [ ( JobOut(28,4,1) == $Finish$1420$2$1$ ) ( JobData(44,"KT4dh",56,43) == $Job2Proc$$$1393$104$2$1$ ) ] ) ( { Finish[ $Finish$1420$2$1$ ] }, [ $Job2Proc$$$1393$105$2$1$ ], [ ( JobOut(28,4,1) == $Finish$1420$2$1$ ) ( JobData(44,"KT4dh",56,43) == $Job2Proc$$$1393$105$2$1$ ) ] ) ( { Finish[ $Finish$1420$2$1$ ] }, [ $Job2Proc$$$1393$107$2$1$ ], [ ( JobOut(32,1,1) == $Finish$1420$2$1$ ) ( JobData(44,"KT4dh",56,43) == $Job2Proc$$$1393$107$2$1$ ) ] ) ( { Finish[ $Finish$1420$2$1$ ] }, [ $Job2Proc$$$1393$108$2$1$ ], [ ( JobOut(28,4,1) == $Finish$1420$2$1$ ) ( JobData(44,"KT4dh",56,43) == $Job2Proc$$$1393$108$2$1$ ) ] ) ( { Finish[ $Finish$1420$2$1$ ] }, [], [ ( JobOut(32,5,1) == $Finish$1420$2$1$ ) ] ) ( { Finish[ $Finish$1420$2$1$ ] }, [], [ ( JobOut(28,4,1) == $Finish$1420$2$1$ ) ] ) ( { Finish[ $Finish$1420$2$1$ ] }, [ $Job2Proc$$$1393$112$2$1$ ], [ ( JobOut(28,4,1) == $Finish$1420$2$1$ ) ( JobData(44,"KT4dh",56,43) == $Job2Proc$$$1393$112$2$1$ ) ] ) ( { Finish[ $Finish$1420$2$1$ ] }, [ $Job2Proc$$$1393$113$2$1$ ], [ ( JobOut(28,4,1) == $Finish$1420$2$1$ ) ( JobData(44,"KT4dh",56,43) == $Job2Proc$$$1393$113$2$1$ ) ] ) ( { Finish[ $Finish$1420$2$1$ ] }, [ $Job2Proc$$$1393$114$2$1$ ], [ ( JobOut(28,4,1) == $Finish$1420$2$1$ ) ( JobData(44,"KT4dh",56,43) == $Job2Proc$$$1393$114$2$1$ ) ] ) ( { Finish[ $Finish$1420$2$1$ ] }, [ $Job2Proc$$$1393$115$2$1$ ], [ ( JobOut(32,5,1) == $Finish$1420$2$1$ ) ( JobData(44,"KT4dh",56,43) == $Job2Proc$$$1393$115$2$1$ ) ] ) ( { Finish[ $Finish$1420$2$1$ ] }, [ $Job2Proc$$$1393$116$2$1$ ], [ ( JobOut(32,5,1) == $Finish$1420$2$1$ ) ( JobData(44,"KT4dh",56,43) == $Job2Proc$$$1393$116$2$1$ ) ] ) ( { Finish[ $Finish$1420$2$1$ ] }, [ $Job2Proc$$$1393$117$2$1$ ], [ ( JobOut(32,5,1) == $Finish$1420$2$1$ ) ( JobData(44,"KT4dh",56,43) == $Job2Proc$$$1393$117$2$1$ ) ] ) ( { Finish[ $Finish$1420$2$1$ ] }, [], [ ( JobOut(32,2,1) == $Finish$1420$2$1$ ) ] ) ( { Finish[ $Finish$1420$2$1$ ] }, [], [ ( JobOut(28,3,1) == $Finish$1420$2$1$ ) ] ) ( { Finish[ $Finish$1420$2$1$ ] }, [ $Job2Proc$$$1393$119$2$1$ ], [ ( JobOut(32,2,1) == $Finish$1420$2$1$ ) ( JobData(44,"KT4dh",56,43) == $Job2Proc$$$1393$119$2$1$ ) ] ) ( { Finish[ $Finish$1420$2$1$ ] }, [ $Job2Proc$$$1393$120$2$1$ ], [ ( JobOut(28,3,1) == $Finish$1420$2$1$ ) ( JobData(44,"KT4dh",56,43) == $Job2Proc$$$1393$120$2$1$ ) ] ) ( { Finish[ $Finish$1420$2$1$ ] }, [ $Job2Proc$$$1393$122$2$1$ ], [ ( JobOut(32,2,1) == $Finish$1420$2$1$ ) ( JobData(44,"KT4dh",56,43) == $Job2Proc$$$1393$122$2$1$ ) ] ) ( { Finish[ $Finish$1420$2$1$ ] }, [ $Job2Proc$$$1393$123$2$1$ ], [ ( JobOut(28,3,1) == $Finish$1420$2$1$ ) ( JobData(44,"KT4dh",56,43) == $Job2Proc$$$1393$123$2$1$ ) ] ) ( { Finish[ $Finish$1420$2$1$ ] }, [ $Job2Proc$$$1393$125$2$1$ ], [ ( JobOut(32,2,1) == $Finish$1420$2$1$ ) ( JobData(44,"KT4dh",56,43) == $Job2Proc$$$1393$125$2$1$ ) ] ) ( { Finish[ $Finish$1420$2$1$ ] }, [ $Job2Proc$$$1393$126$2$1$ ], [ ( JobOut(28,3,1) == $Finish$1420$2$1$ ) ( JobData(44,"KT4dh",56,43) == $Job2Proc$$$1393$126$2$1$ ) ] ) ( { Finish[ $Finish$1420$2$1$ ] }, [], [ ( JobOut(32,1,1) == $Finish$1420$2$1$ ) ] ) ( { Finish[ $Finish$1420$2$1$ ] }, [], [ ( JobOut(28,3,1) == $Finish$1420$2$1$ ) ] ) ( { Finish[ $Finish$1420$2$1$ ] }, [ $Job2Proc$$$1393$128$2$1$ ], [ ( JobOut(32,1,1) == $Finish$1420$2$1$ ) ( JobData(44,"KT4dh",56,43) == $Job2Proc$$$1393$128$2$1$ ) ] ) ( { Finish[ $Finish$1420$2$1$ ] }, [ $Job2Proc$$$1393$129$2$1$ ], [ ( JobOut(28,3,1) == $Finish$1420$2$1$ ) ( JobData(44,"KT4dh",56,43) == $Job2Proc$$$1393$129$2$1$ ) ] ) ( { Finish[ $Finish$1420$2$1$ ] }, [ $Job2Proc$$$1393$131$2$1$ ], [ ( JobOut(32,1,1) == $Finish$1420$2$1$ ) ( JobData(44,"KT4dh",56,43) == $Job2Proc$$$1393$131$2$1$ ) ] ) ( { Finish[ $Finish$1420$2$1$ ] }, [ $Job2Proc$$$1393$132$2$1$ ], [ ( JobOut(28,3,1) == $Finish$1420$2$1$ ) ( JobData(44,"KT4dh",56,43) == $Job2Proc$$$1393$132$2$1$ ) ] ) ( { Finish[ $Finish$1420$2$1$ ] }, [ $Job2Proc$$$1393$134$2$1$ ], [ ( JobOut(32,1,1) == $Finish$1420$2$1$ ) ( JobData(44,"KT4dh",56,43) == $Job2Proc$$$1393$134$2$1$ ) ] ) ( { Finish[ $Finish$1420$2$1$ ] }, [ $Job2Proc$$$1393$135$2$1$ ], [ ( JobOut(28,3,1) == $Finish$1420$2$1$ ) ( JobData(44,"KT4dh",56,43) == $Job2Proc$$$1393$135$2$1$ ) ] ) ( { Finish[ $Finish$1420$2$1$ ] }, [], [ ( JobOut(32,4,1) == $Finish$1420$2$1$ ) ] ) ( { Finish[ $Finish$1420$2$1$ ] }, [], [ ( JobOut(28,3,1) == $Finish$1420$2$1$ ) ] ) ( { Finish[ $Finish$1420$2$1$ ] }, [ $Job2Proc$$$1393$138$2$1$ ], [ ( JobOut(28,3,1) == $Finish$1420$2$1$ ) ( JobData(44,"KT4dh",56,43) == $Job2Proc$$$1393$138$2$1$ ) ] ) ( { Finish[ $Finish$1420$2$1$ ] }, [ $Job2Proc$$$1393$139$2$1$ ], [ ( JobOut(28,3,1) == $Finish$1420$2$1$ ) ( JobData(44,"KT4dh",56,43) == $Job2Proc$$$1393$139$2$1$ ) ] ) ( { Finish[ $Finish$1420$2$1$ ] }, [ $Job2Proc$$$1393$140$2$1$ ], [ ( JobOut(32,4,1) == $Finish$1420$2$1$ ) ( JobData(44,"KT4dh",56,43) == $Job2Proc$$$1393$140$2$1$ ) ] ) ( { Finish[ $Finish$1420$2$1$ ] }, [ $Job2Proc$$$1393$141$2$1$ ], [ ( JobOut(32,4,1) == $Finish$1420$2$1$ ) ( JobData(44,"KT4dh",56,43) == $Job2Proc$$$1393$141$2$1$ ) ] ) ( { Finish[ $Finish$1420$2$1$ ] }, [ $Job2Proc$$$1393$143$2$1$ ], [ ( JobOut(32,4,1) == $Finish$1420$2$1$ ) ( JobData(44,"KT4dh",56,43) == $Job2Proc$$$1393$143$2$1$ ) ] ) ( { Finish[ $Finish$1420$2$1$ ] }, [ $Job2Proc$$$1393$144$2$1$ ], [ ( JobOut(28,3,1) == $Finish$1420$2$1$ ) ( JobData(44,"KT4dh",56,43) == $Job2Proc$$$1393$144$2$1$ ) ] ) ( { Finish[ $Finish$1420$2$1$ ] }, [], [ ( JobOut(32,5,1) == $Finish$1420$2$1$ ) ] ) ( { Finish[ $Finish$1420$2$1$ ] }, [], [ ( JobOut(28,3,1) == $Finish$1420$2$1$ ) ] ) ( { Finish[ $Finish$1420$2$1$ ] }, [ $Job2Proc$$$1393$147$2$1$ ], [ ( JobOut(28,3,1) == $Finish$1420$2$1$ ) ( JobData(44,"KT4dh",56,43) == $Job2Proc$$$1393$147$2$1$ ) ] ) ( { Finish[ $Finish$1420$2$1$ ] }, [ $Job2Proc$$$1393$148$2$1$ ], [ ( JobOut(28,3,1) == $Finish$1420$2$1$ ) ( JobData(44,"KT4dh",56,43) == $Job2Proc$$$1393$148$2$1$ ) ] ) ( { Finish[ $Finish$1420$2$1$ ] }, [ $Job2Proc$$$1393$150$2$1$ ], [ ( JobOut(28,3,1) == $Finish$1420$2$1$ ) ( JobData(44,"KT4dh",56,43) == $Job2Proc$$$1393$150$2$1$ ) ] ) ( { Finish[ $Finish$1420$2$1$ ] }, [ $Job2Proc$$$1393$151$2$1$ ], [ ( JobOut(32,5,1) == $Finish$1420$2$1$ ) ( JobData(44,"KT4dh",56,43) == $Job2Proc$$$1393$151$2$1$ ) ] ) ( { Finish[ $Finish$1420$2$1$ ] }, [ $Job2Proc$$$1393$152$2$1$ ], [ ( JobOut(32,5,1) == $Finish$1420$2$1$ ) ( JobData(44,"KT4dh",56,43) == $Job2Proc$$$1393$152$2$1$ ) ] ) ( { Finish[ $Finish$1420$2$1$ ] }, [ $Job2Proc$$$1393$153$2$1$ ], [ ( JobOut(32,5,1) == $Finish$1420$2$1$ ) ( JobData(44,"KT4dh",56,43) == $Job2Proc$$$1393$153$2$1$ ) ] ) ( { Finish[ $Finish$1420$2$1$ ] }, [], [ ( JobOut(32,1,1) == $Finish$1420$2$1$ ) ] ) ( { Finish[ $Finish$1420$2$1$ ] }, [], [ ( JobOut(28,2,1) == $Finish$1420$2$1$ ) ] ) ( { Finish[ $Finish$1420$2$1$ ] }, [ $Job2Proc$$$1393$155$2$1$ ], [ ( JobOut(32,1,1) == $Finish$1420$2$1$ ) ( JobData(44,"KT4dh",56,43) == $Job2Proc$$$1393$155$2$1$ ) ] ) ( { Finish[ $Finish$1420$2$1$ ] }, [ $Job2Proc$$$1393$156$2$1$ ], [ ( JobOut(28,2,1) == $Finish$1420$2$1$ ) ( JobData(44,"KT4dh",56,43) == $Job2Proc$$$1393$156$2$1$ ) ] ) ( { Finish[ $Finish$1420$2$1$ ] }, [ $Job2Proc$$$1393$158$2$1$ ], [ ( JobOut(32,1,1) == $Finish$1420$2$1$ ) ( JobData(44,"KT4dh",56,43) == $Job2Proc$$$1393$158$2$1$ ) ] ) ( { Finish[ $Finish$1420$2$1$ ] }, [ $Job2Proc$$$1393$159$2$1$ ], [ ( JobOut(28,2,1) == $Finish$1420$2$1$ ) ( JobData(44,"KT4dh",56,43) == $Job2Proc$$$1393$159$2$1$ ) ] ) ( { Finish[ $Finish$1420$2$1$ ] }, [ $Job2Proc$$$1393$161$2$1$ ], [ ( JobOut(32,1,1) == $Finish$1420$2$1$ ) ( JobData(44,"KT4dh",56,43) == $Job2Proc$$$1393$161$2$1$ ) ] ) ( { Finish[ $Finish$1420$2$1$ ] }, [ $Job2Proc$$$1393$162$2$1$ ], [ ( JobOut(28,2,1) == $Finish$1420$2$1$ ) ( JobData(44,"KT4dh",56,43) == $Job2Proc$$$1393$162$2$1$ ) ] ) ( { Finish[ $Finish$1420$2$1$ ] }, [], [ ( JobOut(32,3,1) == $Finish$1420$2$1$ ) ] ) ( { Finish[ $Finish$1420$2$1$ ] }, [], [ ( JobOut(28,2,1) == $Finish$1420$2$1$ ) ] ) ( { Finish[ $Finish$1420$2$1$ ] }, [ $Job2Proc$$$1393$164$2$1$ ], [ ( JobOut(28,2,1) == $Finish$1420$2$1$ ) ( JobData(44,"KT4dh",56,43) == $Job2Proc$$$1393$164$2$1$ ) ] ) ( { Finish[ $Finish$1420$2$1$ ] }, [ $Job2Proc$$$1393$165$2$1$ ], [ ( JobOut(32,3,1) == $Finish$1420$2$1$ ) ( JobData(44,"KT4dh",56,43) == $Job2Proc$$$1393$165$2$1$ ) ] ) ( { Finish[ $Finish$1420$2$1$ ] }, [ $Job2Proc$$$1393$167$2$1$ ], [ ( JobOut(32,3,1) == $Finish$1420$2$1$ ) ( JobData(44,"KT4dh",56,43) == $Job2Proc$$$1393$167$2$1$ ) ] ) ( { Finish[ $Finish$1420$2$1$ ] }, [ $Job2Proc$$$1393$168$2$1$ ], [ ( JobOut(28,2,1) == $Finish$1420$2$1$ ) ( JobData(44,"KT4dh",56,43) == $Job2Proc$$$1393$168$2$1$ ) ] ) ( { Finish[ $Finish$1420$2$1$ ] }, [ $Job2Proc$$$1393$170$2$1$ ], [ ( JobOut(32,3,1) == $Finish$1420$2$1$ ) ( JobData(44,"KT4dh",56,43) == $Job2Proc$$$1393$170$2$1$ ) ] ) ( { Finish[ $Finish$1420$2$1$ ] }, [ $Job2Proc$$$1393$171$2$1$ ], [ ( JobOut(28,2,1) == $Finish$1420$2$1$ ) ( JobData(44,"KT4dh",56,43) == $Job2Proc$$$1393$171$2$1$ ) ] ) ( { Finish[ $Finish$1420$2$1$ ] }, [], [ ( JobOut(32,4,1) == $Finish$1420$2$1$ ) ] ) ( { Finish[ $Finish$1420$2$1$ ] }, [], [ ( JobOut(28,2,1) == $Finish$1420$2$1$ ) ] ) ( { Finish[ $Finish$1420$2$1$ ] }, [ $Job2Proc$$$1393$173$2$1$ ], [ ( JobOut(28,2,1) == $Finish$1420$2$1$ ) ( JobData(44,"KT4dh",56,43) == $Job2Proc$$$1393$173$2$1$ ) ] ) ( { Finish[ $Finish$1420$2$1$ ] }, [ $Job2Proc$$$1393$175$2$1$ ], [ ( JobOut(28,2,1) == $Finish$1420$2$1$ ) ( JobData(44,"KT4dh",56,43) == $Job2Proc$$$1393$175$2$1$ ) ] ) ( { Finish[ $Finish$1420$2$1$ ] }, [ $Job2Proc$$$1393$176$2$1$ ], [ ( JobOut(32,4,1) == $Finish$1420$2$1$ ) ( JobData(44,"KT4dh",56,43) == $Job2Proc$$$1393$176$2$1$ ) ] ) ( { Finish[ $Finish$1420$2$1$ ] }, [ $Job2Proc$$$1393$177$2$1$ ], [ ( JobOut(32,4,1) == $Finish$1420$2$1$ ) ( JobData(44,"KT4dh",56,43) == $Job2Proc$$$1393$177$2$1$ ) ] ) ( { Finish[ $Finish$1420$2$1$ ] }, [ $Job2Proc$$$1393$179$2$1$ ], [ ( JobOut(32,4,1) == $Finish$1420$2$1$ ) ( JobData(44,"KT4dh",56,43) == $Job2Proc$$$1393$179$2$1$ ) ] ) ( { Finish[ $Finish$1420$2$1$ ] }, [ $Job2Proc$$$1393$180$2$1$ ], [ ( JobOut(28,2,1) == $Finish$1420$2$1$ ) ( JobData(44,"KT4dh",56,43) == $Job2Proc$$$1393$180$2$1$ ) ] ) ( { Finish[ $Finish$1420$2$1$ ] }, [], [ ( JobOut(32,5,1) == $Finish$1420$2$1$ ) ] ) ( { Finish[ $Finish$1420$2$1$ ] }, [], [ ( JobOut(28,2,1) == $Finish$1420$2$1$ ) ] ) ( { Finish[ $Finish$1420$2$1$ ] }, [ $Job2Proc$$$1393$182$2$1$ ], [ ( JobOut(28,2,1) == $Finish$1420$2$1$ ) ( JobData(44,"KT4dh",56,43) == $Job2Proc$$$1393$182$2$1$ ) ] ) ( { Finish[ $Finish$1420$2$1$ ] }, [ $Job2Proc$$$1393$184$2$1$ ], [ ( JobOut(28,2,1) == $Finish$1420$2$1$ ) ( JobData(44,"KT4dh",56,43) == $Job2Proc$$$1393$184$2$1$ ) ] ) ( { Finish[ $Finish$1420$2$1$ ] }, [ $Job2Proc$$$1393$186$2$1$ ], [ ( JobOut(28,2,1) == $Finish$1420$2$1$ ) ( JobData(44,"KT4dh",56,43) == $Job2Proc$$$1393$186$2$1$ ) ] ) ( { Finish[ $Finish$1420$2$1$ ] }, [ $Job2Proc$$$1393$187$2$1$ ], [ ( JobOut(32,5,1) == $Finish$1420$2$1$ ) ( JobData(44,"KT4dh",56,43) == $Job2Proc$$$1393$187$2$1$ ) ] ) ( { Finish[ $Finish$1420$2$1$ ] }, [ $Job2Proc$$$1393$188$2$1$ ], [ ( JobOut(32,5,1) == $Finish$1420$2$1$ ) ( JobData(44,"KT4dh",56,43) == $Job2Proc$$$1393$188$2$1$ ) ] ) ( { Finish[ $Finish$1420$2$1$ ] }, [ $Job2Proc$$$1393$189$2$1$ ], [ ( JobOut(32,5,1) == $Finish$1420$2$1$ ) ( JobData(44,"KT4dh",56,43) == $Job2Proc$$$1393$189$2$1$ ) ] ) ( { Finish[ $Finish$1420$2$1$ ] }, [], [ ( JobOut(32,2,1) == $Finish$1420$2$1$ ) ] ) ( { Finish[ $Finish$1420$2$1$ ] }, [], [ ( JobOut(28,1,1) == $Finish$1420$2$1$ ) ] ) ( { Finish[ $Finish$1420$2$1$ ] }, [ $Job2Proc$$$1393$191$2$1$ ], [ ( JobOut(32,2,1) == $Finish$1420$2$1$ ) ( JobData(44,"KT4dh",56,43) == $Job2Proc$$$1393$191$2$1$ ) ] ) ( { Finish[ $Finish$1420$2$1$ ] }, [ $Job2Proc$$$1393$192$2$1$ ], [ ( JobOut(28,1,1) == $Finish$1420$2$1$ ) ( JobData(44,"KT4dh",56,43) == $Job2Proc$$$1393$192$2$1$ ) ] ) ( { Finish[ $Finish$1420$2$1$ ] }, [ $Job2Proc$$$1393$194$2$1$ ], [ ( JobOut(32,2,1) == $Finish$1420$2$1$ ) ( JobData(44,"KT4dh",56,43) == $Job2Proc$$$1393$194$2$1$ ) ] ) ( { Finish[ $Finish$1420$2$1$ ] }, [ $Job2Proc$$$1393$195$2$1$ ], [ ( JobOut(28,1,1) == $Finish$1420$2$1$ ) ( JobData(44,"KT4dh",56,43) == $Job2Proc$$$1393$195$2$1$ ) ] ) ( { Finish[ $Finish$1420$2$1$ ] }, [ $Job2Proc$$$1393$197$2$1$ ], [ ( JobOut(32,2,1) == $Finish$1420$2$1$ ) ( JobData(44,"KT4dh",56,43) == $Job2Proc$$$1393$197$2$1$ ) ] ) ( { Finish[ $Finish$1420$2$1$ ] }, [ $Job2Proc$$$1393$198$2$1$ ], [ ( JobOut(28,1,1) == $Finish$1420$2$1$ ) ( JobData(44,"KT4dh",56,43) == $Job2Proc$$$1393$198$2$1$ ) ] ) ( { Finish[ $Finish$1420$2$1$ ] }, [], [ ( JobOut(32,3,1) == $Finish$1420$2$1$ ) ] ) ( { Finish[ $Finish$1420$2$1$ ] }, [], [ ( JobOut(28,1,1) == $Finish$1420$2$1$ ) ] ) ( { Finish[ $Finish$1420$2$1$ ] }, [ $Job2Proc$$$1393$200$2$1$ ], [ ( JobOut(28,1,1) == $Finish$1420$2$1$ ) ( JobData(44,"KT4dh",56,43) == $Job2Proc$$$1393$200$2$1$ ) ] ) ( { Finish[ $Finish$1420$2$1$ ] }, [ $Job2Proc$$$1393$201$2$1$ ], [ ( JobOut(32,3,1) == $Finish$1420$2$1$ ) ( JobData(44,"KT4dh",56,43) == $Job2Proc$$$1393$201$2$1$ ) ] ) ( { Finish[ $Finish$1420$2$1$ ] }, [ $Job2Proc$$$1393$203$2$1$ ], [ ( JobOut(32,3,1) == $Finish$1420$2$1$ ) ( JobData(44,"KT4dh",56,43) == $Job2Proc$$$1393$203$2$1$ ) ] ) ( { Finish[ $Finish$1420$2$1$ ] }, [ $Job2Proc$$$1393$204$2$1$ ], [ ( JobOut(28,1,1) == $Finish$1420$2$1$ ) ( JobData(44,"KT4dh",56,43) == $Job2Proc$$$1393$204$2$1$ ) ] ) ( { Finish[ $Finish$1420$2$1$ ] }, [ $Job2Proc$$$1393$206$2$1$ ], [ ( JobOut(32,3,1) == $Finish$1420$2$1$ ) ( JobData(44,"KT4dh",56,43) == $Job2Proc$$$1393$206$2$1$ ) ] ) ( { Finish[ $Finish$1420$2$1$ ] }, [ $Job2Proc$$$1393$207$2$1$ ], [ ( JobOut(28,1,1) == $Finish$1420$2$1$ ) ( JobData(44,"KT4dh",56,43) == $Job2Proc$$$1393$207$2$1$ ) ] ) ( { Finish[ $Finish$1420$2$1$ ] }, [], [ ( JobOut(32,4,1) == $Finish$1420$2$1$ ) ] ) ( { Finish[ $Finish$1420$2$1$ ] }, [], [ ( JobOut(28,1,1) == $Finish$1420$2$1$ ) ] ) ( { Finish[ $Finish$1420$2$1$ ] }, [ $Job2Proc$$$1393$209$2$1$ ], [ ( JobOut(28,1,1) == $Finish$1420$2$1$ ) ( JobData(44,"KT4dh",56,43) == $Job2Proc$$$1393$209$2$1$ ) ] ) ( { Finish[ $Finish$1420$2$1$ ] }, [ $Job2Proc$$$1393$211$2$1$ ], [ ( JobOut(28,1,1) == $Finish$1420$2$1$ ) ( JobData(44,"KT4dh",56,43) == $Job2Proc$$$1393$211$2$1$ ) ] ) ( { Finish[ $Finish$1420$2$1$ ] }, [ $Job2Proc$$$1393$212$2$1$ ], [ ( JobOut(32,4,1) == $Finish$1420$2$1$ ) ( JobData(44,"KT4dh",56,43) == $Job2Proc$$$1393$212$2$1$ ) ] ) ( { Finish[ $Finish$1420$2$1$ ] }, [ $Job2Proc$$$1393$213$2$1$ ], [ ( JobOut(32,4,1) == $Finish$1420$2$1$ ) ( JobData(44,"KT4dh",56,43) == $Job2Proc$$$1393$213$2$1$ ) ] ) ( { Finish[ $Finish$1420$2$1$ ] }, [ $Job2Proc$$$1393$215$2$1$ ], [ ( JobOut(32,4,1) == $Finish$1420$2$1$ ) ( JobData(44,"KT4dh",56,43) == $Job2Proc$$$1393$215$2$1$ ) ] ) ( { Finish[ $Finish$1420$2$1$ ] }, [ $Job2Proc$$$1393$216$2$1$ ], [ ( JobOut(28,1,1) == $Finish$1420$2$1$ ) ( JobData(44,"KT4dh",56,43) == $Job2Proc$$$1393$216$2$1$ ) ] ) ( { Finish[ $Finish$1420$2$1$ ] }, [], [ ( JobOut(32,5,1) == $Finish$1420$2$1$ ) ] ) ( { Finish[ $Finish$1420$2$1$ ] }, [], [ ( JobOut(28,1,1) == $Finish$1420$2$1$ ) ] ) ( { Finish[ $Finish$1420$2$1$ ] }, [ $Job2Proc$$$1393$218$2$1$ ], [ ( JobOut(28,1,1) == $Finish$1420$2$1$ ) ( JobData(44,"KT4dh",56,43) == $Job2Proc$$$1393$218$2$1$ ) ] ) ( { Finish[ $Finish$1420$2$1$ ] }, [ $Job2Proc$$$1393$220$2$1$ ], [ ( JobOut(28,1,1) == $Finish$1420$2$1$ ) ( JobData(44,"KT4dh",56,43) == $Job2Proc$$$1393$220$2$1$ ) ] ) ( { Finish[ $Finish$1420$2$1$ ] }, [ $Job2Proc$$$1393$222$2$1$ ], [ ( JobOut(28,1,1) == $Finish$1420$2$1$ ) ( JobData(44,"KT4dh",56,43) == $Job2Proc$$$1393$222$2$1$ ) ] ) ( { Finish[ $Finish$1420$2$1$ ] }, [ $Job2Proc$$$1393$223$2$1$ ], [ ( JobOut(32,5,1) == $Finish$1420$2$1$ ) ( JobData(44,"KT4dh",56,43) == $Job2Proc$$$1393$223$2$1$ ) ] ) ( { Finish[ $Finish$1420$2$1$ ] }, [ $Job2Proc$$$1393$224$2$1$ ], [ ( JobOut(32,5,1) == $Finish$1420$2$1$ ) ( JobData(44,"KT4dh",56,43) == $Job2Proc$$$1393$224$2$1$ ) ] ) ( { Finish[ $Finish$1420$2$1$ ] }, [ $Job2Proc$$$1393$225$2$1$ ], [ ( JobOut(32,5,1) == $Finish$1420$2$1$ ) ( JobData(44,"KT4dh",56,43) == $Job2Proc$$$1393$225$2$1$ ) ] ) ( { Finish[ $Finish$1420$2$1$ ] }, [], [ ( JobOut(44,3,1) == $Finish$1420$2$1$ ) ] ) ( { Finish[ $Finish$1420$2$1$ ] }, [], [ ( JobOut(32,4,1) == $Finish$1420$2$1$ ) ] ) ( { Finish[ $Finish$1420$2$1$ ] }, [], [ ( JobOut(28,5,1) == $Finish$1420$2$1$ ) ] ) ( { Finish[ $Finish$1420$2$1$ ] }, [], [ ( JobOut(44,2,1) == $Finish$1420$2$1$ ) ] ) ( { Finish[ $Finish$1420$2$1$ ] }, [], [ ( JobOut(32,4,1) == $Finish$1420$2$1$ ) ] ) ( { Finish[ $Finish$1420$2$1$ ] }, [], [ ( JobOut(28,5,1) == $Finish$1420$2$1$ ) ] ) ( { Finish[ $Finish$1420$2$1$ ] }, [], [ ( JobOut(44,1,1) == $Finish$1420$2$1$ ) ] ) ( { Finish[ $Finish$1420$2$1$ ] }, [], [ ( JobOut(32,4,1) == $Finish$1420$2$1$ ) ] ) ( { Finish[ $Finish$1420$2$1$ ] }, [], [ ( JobOut(28,5,1) == $Finish$1420$2$1$ ) ] ) ( { Finish[ $Finish$1420$2$1$ ] }, [], [ ( JobOut(44,2,1) == $Finish$1420$2$1$ ) ] ) ( { Finish[ $Finish$1420$2$1$ ] }, [], [ ( JobOut(32,3,1) == $Finish$1420$2$1$ ) ] ) ( { Finish[ $Finish$1420$2$1$ ] }, [], [ ( JobOut(28,5,1) == $Finish$1420$2$1$ ) ] ) ( { Finish[ $Finish$1420$2$1$ ] }, [], [ ( JobOut(44,1,1) == $Finish$1420$2$1$ ) ] ) ( { Finish[ $Finish$1420$2$1$ ] }, [], [ ( JobOut(32,3,1) == $Finish$1420$2$1$ ) ] ) ( { Finish[ $Finish$1420$2$1$ ] }, [], [ ( JobOut(28,5,1) == $Finish$1420$2$1$ ) ] ) ( { Finish[ $Finish$1420$2$1$ ] }, [], [ ( JobOut(44,4,1) == $Finish$1420$2$1$ ) ] ) ( { Finish[ $Finish$1420$2$1$ ] }, [], [ ( JobOut(32,3,1) == $Finish$1420$2$1$ ) ] ) ( { Finish[ $Finish$1420$2$1$ ] }, [], [ ( JobOut(28,5,1) == $Finish$1420$2$1$ ) ] ) ( { Finish[ $Finish$1420$2$1$ ] }, [], [ ( JobOut(44,1,1) == $Finish$1420$2$1$ ) ] ) ( { Finish[ $Finish$1420$2$1$ ] }, [], [ ( JobOut(32,2,1) == $Finish$1420$2$1$ ) ] ) ( { Finish[ $Finish$1420$2$1$ ] }, [], [ ( JobOut(28,5,1) == $Finish$1420$2$1$ ) ] ) ( { Finish[ $Finish$1420$2$1$ ] }, [], [ ( JobOut(44,3,1) == $Finish$1420$2$1$ ) ] ) ( { Finish[ $Finish$1420$2$1$ ] }, [], [ ( JobOut(32,2,1) == $Finish$1420$2$1$ ) ] ) ( { Finish[ $Finish$1420$2$1$ ] }, [], [ ( JobOut(28,5,1) == $Finish$1420$2$1$ ) ] ) ( { Finish[ $Finish$1420$2$1$ ] }, [], [ ( JobOut(44,4,1) == $Finish$1420$2$1$ ) ] ) ( { Finish[ $Finish$1420$2$1$ ] }, [], [ ( JobOut(32,2,1) == $Finish$1420$2$1$ ) ] ) ( { Finish[ $Finish$1420$2$1$ ] }, [], [ ( JobOut(28,5,1) == $Finish$1420$2$1$ ) ] ) ( { Finish[ $Finish$1420$2$1$ ] }, [], [ ( JobOut(44,2,1) == $Finish$1420$2$1$ ) ] ) ( { Finish[ $Finish$1420$2$1$ ] }, [], [ ( JobOut(32,1,1) == $Finish$1420$2$1$ ) ] ) ( { Finish[ $Finish$1420$2$1$ ] }, [], [ ( JobOut(28,5,1) == $Finish$1420$2$1$ ) ] ) ( { Finish[ $Finish$1420$2$1$ ] }, [], [ ( JobOut(44,3,1) == $Finish$1420$2$1$ ) ] ) ( { Finish[ $Finish$1420$2$1$ ] }, [], [ ( JobOut(32,1,1) == $Finish$1420$2$1$ ) ] ) ( { Finish[ $Finish$1420$2$1$ ] }, [], [ ( JobOut(28,5,1) == $Finish$1420$2$1$ ) ] ) ( { Finish[ $Finish$1420$2$1$ ] }, [], [ ( JobOut(44,4,1) == $Finish$1420$2$1$ ) ] ) ( { Finish[ $Finish$1420$2$1$ ] }, [], [ ( JobOut(32,1,1) == $Finish$1420$2$1$ ) ] ) ( { Finish[ $Finish$1420$2$1$ ] }, [], [ ( JobOut(28,5,1) == $Finish$1420$2$1$ ) ] ) ( { Finish[ $Finish$1420$2$1$ ] }, [], [ ( JobOut(44,2,1) == $Finish$1420$2$1$ ) ] ) ( { Finish[ $Finish$1420$2$1$ ] }, [], [ ( JobOut(32,3,1) == $Finish$1420$2$1$ ) ] ) ( { Finish[ $Finish$1420$2$1$ ] }, [], [ ( JobOut(28,4,1) == $Finish$1420$2$1$ ) ] ) ( { Finish[ $Finish$1420$2$1$ ] }, [], [ ( JobOut(44,1,1) == $Finish$1420$2$1$ ) ] ) ( { Finish[ $Finish$1420$2$1$ ] }, [], [ ( JobOut(32,3,1) == $Finish$1420$2$1$ ) ] ) ( { Finish[ $Finish$1420$2$1$ ] }, [], [ ( JobOut(28,4,1) == $Finish$1420$2$1$ ) ] ) ( { Finish[ $Finish$1420$2$1$ ] }, [], [ ( JobOut(44,5,1) == $Finish$1420$2$1$ ) ] ) ( { Finish[ $Finish$1420$2$1$ ] }, [], [ ( JobOut(32,3,1) == $Finish$1420$2$1$ ) ] ) ( { Finish[ $Finish$1420$2$1$ ] }, [], [ ( JobOut(28,4,1) == $Finish$1420$2$1$ ) ] ) ( { Finish[ $Finish$1420$2$1$ ] }, [], [ ( JobOut(44,1,1) == $Finish$1420$2$1$ ) ] ) ( { Finish[ $Finish$1420$2$1$ ] }, [], [ ( JobOut(32,2,1) == $Finish$1420$2$1$ ) ] ) ( { Finish[ $Finish$1420$2$1$ ] }, [], [ ( JobOut(28,4,1) == $Finish$1420$2$1$ ) ] ) ( { Finish[ $Finish$1420$2$1$ ] }, [], [ ( JobOut(44,3,1) == $Finish$1420$2$1$ ) ] ) ( { Finish[ $Finish$1420$2$1$ ] }, [], [ ( JobOut(32,2,1) == $Finish$1420$2$1$ ) ] ) ( { Finish[ $Finish$1420$2$1$ ] }, [], [ ( JobOut(28,4,1) == $Finish$1420$2$1$ ) ] ) ( { Finish[ $Finish$1420$2$1$ ] }, [], [ ( JobOut(44,5,1) == $Finish$1420$2$1$ ) ] ) ( { Finish[ $Finish$1420$2$1$ ] }, [], [ ( JobOut(32,2,1) == $Finish$1420$2$1$ ) ] ) ( { Finish[ $Finish$1420$2$1$ ] }, [], [ ( JobOut(28,4,1) == $Finish$1420$2$1$ ) ] ) ( { Finish[ $Finish$1420$2$1$ ] }, [], [ ( JobOut(44,2,1) == $Finish$1420$2$1$ ) ] ) ( { Finish[ $Finish$1420$2$1$ ] }, [], [ ( JobOut(32,1,1) == $Finish$1420$2$1$ ) ] ) ( { Finish[ $Finish$1420$2$1$ ] }, [], [ ( JobOut(28,4,1) == $Finish$1420$2$1$ ) ] ) ( { Finish[ $Finish$1420$2$1$ ] }, [], [ ( JobOut(44,3,1) == $Finish$1420$2$1$ ) ] ) ( { Finish[ $Finish$1420$2$1$ ] }, [], [ ( JobOut(32,1,1) == $Finish$1420$2$1$ ) ] ) ( { Finish[ $Finish$1420$2$1$ ] }, [], [ ( JobOut(28,4,1) == $Finish$1420$2$1$ ) ] ) ( { Finish[ $Finish$1420$2$1$ ] }, [], [ ( JobOut(44,5,1) == $Finish$1420$2$1$ ) ] ) ( { Finish[ $Finish$1420$2$1$ ] }, [], [ ( JobOut(32,1,1) == $Finish$1420$2$1$ ) ] ) ( { Finish[ $Finish$1420$2$1$ ] }, [], [ ( JobOut(28,4,1) == $Finish$1420$2$1$ ) ] ) ( { Finish[ $Finish$1420$2$1$ ] }, [], [ ( JobOut(44,3,1) == $Finish$1420$2$1$ ) ] ) ( { Finish[ $Finish$1420$2$1$ ] }, [], [ ( JobOut(28,4,1) == $Finish$1420$2$1$ ) ] ) ( { Finish[ $Finish$1420$2$1$ ] }, [], [ ( JobOut(32,5,1) == $Finish$1420$2$1$ ) ] ) ( { Finish[ $Finish$1420$2$1$ ] }, [], [ ( JobOut(44,2,1) == $Finish$1420$2$1$ ) ] ) ( { Finish[ $Finish$1420$2$1$ ] }, [], [ ( JobOut(28,4,1) == $Finish$1420$2$1$ ) ] ) ( { Finish[ $Finish$1420$2$1$ ] }, [], [ ( JobOut(32,5,1) == $Finish$1420$2$1$ ) ] ) ( { Finish[ $Finish$1420$2$1$ ] }, [], [ ( JobOut(44,1,1) == $Finish$1420$2$1$ ) ] ) ( { Finish[ $Finish$1420$2$1$ ] }, [], [ ( JobOut(28,4,1) == $Finish$1420$2$1$ ) ] ) ( { Finish[ $Finish$1420$2$1$ ] }, [], [ ( JobOut(32,5,1) == $Finish$1420$2$1$ ) ] ) ( { Finish[ $Finish$1420$2$1$ ] }, [], [ ( JobOut(44,1,1) == $Finish$1420$2$1$ ) ] ) ( { Finish[ $Finish$1420$2$1$ ] }, [], [ ( JobOut(32,2,1) == $Finish$1420$2$1$ ) ] ) ( { Finish[ $Finish$1420$2$1$ ] }, [], [ ( JobOut(28,3,1) == $Finish$1420$2$1$ ) ] ) ( { Finish[ $Finish$1420$2$1$ ] }, [], [ ( JobOut(44,4,1) == $Finish$1420$2$1$ ) ] ) ( { Finish[ $Finish$1420$2$1$ ] }, [], [ ( JobOut(32,2,1) == $Finish$1420$2$1$ ) ] ) ( { Finish[ $Finish$1420$2$1$ ] }, [], [ ( JobOut(28,3,1) == $Finish$1420$2$1$ ) ] ) ( { Finish[ $Finish$1420$2$1$ ] }, [], [ ( JobOut(44,5,1) == $Finish$1420$2$1$ ) ] ) ( { Finish[ $Finish$1420$2$1$ ] }, [], [ ( JobOut(32,2,1) == $Finish$1420$2$1$ ) ] ) ( { Finish[ $Finish$1420$2$1$ ] }, [], [ ( JobOut(28,3,1) == $Finish$1420$2$1$ ) ] ) ( { Finish[ $Finish$1420$2$1$ ] }, [], [ ( JobOut(44,2,1) == $Finish$1420$2$1$ ) ] ) ( { Finish[ $Finish$1420$2$1$ ] }, [], [ ( JobOut(32,1,1) == $Finish$1420$2$1$ ) ] ) ( { Finish[ $Finish$1420$2$1$ ] }, [], [ ( JobOut(28,3,1) == $Finish$1420$2$1$ ) ] ) ( { Finish[ $Finish$1420$2$1$ ] }, [], [ ( JobOut(44,4,1) == $Finish$1420$2$1$ ) ] ) ( { Finish[ $Finish$1420$2$1$ ] }, [], [ ( JobOut(32,1,1) == $Finish$1420$2$1$ ) ] ) ( { Finish[ $Finish$1420$2$1$ ] }, [], [ ( JobOut(28,3,1) == $Finish$1420$2$1$ ) ] ) ( { Finish[ $Finish$1420$2$1$ ] }, [], [ ( JobOut(44,5,1) == $Finish$1420$2$1$ ) ] ) ( { Finish[ $Finish$1420$2$1$ ] }, [], [ ( JobOut(32,1,1) == $Finish$1420$2$1$ ) ] ) ( { Finish[ $Finish$1420$2$1$ ] }, [], [ ( JobOut(28,3,1) == $Finish$1420$2$1$ ) ] ) ( { Finish[ $Finish$1420$2$1$ ] }, [], [ ( JobOut(44,2,1) == $Finish$1420$2$1$ ) ] ) ( { Finish[ $Finish$1420$2$1$ ] }, [], [ ( JobOut(28,3,1) == $Finish$1420$2$1$ ) ] ) ( { Finish[ $Finish$1420$2$1$ ] }, [], [ ( JobOut(32,4,1) == $Finish$1420$2$1$ ) ] ) ( { Finish[ $Finish$1420$2$1$ ] }, [], [ ( JobOut(44,1,1) == $Finish$1420$2$1$ ) ] ) ( { Finish[ $Finish$1420$2$1$ ] }, [], [ ( JobOut(28,3,1) == $Finish$1420$2$1$ ) ] ) ( { Finish[ $Finish$1420$2$1$ ] }, [], [ ( JobOut(32,4,1) == $Finish$1420$2$1$ ) ] ) ( { Finish[ $Finish$1420$2$1$ ] }, [], [ ( JobOut(44,5,1) == $Finish$1420$2$1$ ) ] ) ( { Finish[ $Finish$1420$2$1$ ] }, [], [ ( JobOut(32,4,1) == $Finish$1420$2$1$ ) ] ) ( { Finish[ $Finish$1420$2$1$ ] }, [], [ ( JobOut(28,3,1) == $Finish$1420$2$1$ ) ] ) ( { Finish[ $Finish$1420$2$1$ ] }, [], [ ( JobOut(44,2,1) == $Finish$1420$2$1$ ) ] ) ( { Finish[ $Finish$1420$2$1$ ] }, [], [ ( JobOut(28,3,1) == $Finish$1420$2$1$ ) ] ) ( { Finish[ $Finish$1420$2$1$ ] }, [], [ ( JobOut(32,5,1) == $Finish$1420$2$1$ ) ] ) ( { Finish[ $Finish$1420$2$1$ ] }, [], [ ( JobOut(44,1,1) == $Finish$1420$2$1$ ) ] ) ( { Finish[ $Finish$1420$2$1$ ] }, [], [ ( JobOut(28,3,1) == $Finish$1420$2$1$ ) ] ) ( { Finish[ $Finish$1420$2$1$ ] }, [], [ ( JobOut(32,5,1) == $Finish$1420$2$1$ ) ] ) ( { Finish[ $Finish$1420$2$1$ ] }, [], [ ( JobOut(44,4,1) == $Finish$1420$2$1$ ) ] ) ( { Finish[ $Finish$1420$2$1$ ] }, [], [ ( JobOut(28,3,1) == $Finish$1420$2$1$ ) ] ) ( { Finish[ $Finish$1420$2$1$ ] }, [], [ ( JobOut(32,5,1) == $Finish$1420$2$1$ ) ] ) ( { Finish[ $Finish$1420$2$1$ ] }, [], [ ( JobOut(44,3,1) == $Finish$1420$2$1$ ) ] ) ( { Finish[ $Finish$1420$2$1$ ] }, [], [ ( JobOut(32,1,1) == $Finish$1420$2$1$ ) ] ) ( { Finish[ $Finish$1420$2$1$ ] }, [], [ ( JobOut(28,2,1) == $Finish$1420$2$1$ ) ] ) ( { Finish[ $Finish$1420$2$1$ ] }, [], [ ( JobOut(44,4,1) == $Finish$1420$2$1$ ) ] ) ( { Finish[ $Finish$1420$2$1$ ] }, [], [ ( JobOut(32,1,1) == $Finish$1420$2$1$ ) ] ) ( { Finish[ $Finish$1420$2$1$ ] }, [], [ ( JobOut(28,2,1) == $Finish$1420$2$1$ ) ] ) ( { Finish[ $Finish$1420$2$1$ ] }, [], [ ( JobOut(44,5,1) == $Finish$1420$2$1$ ) ] ) ( { Finish[ $Finish$1420$2$1$ ] }, [], [ ( JobOut(32,1,1) == $Finish$1420$2$1$ ) ] ) ( { Finish[ $Finish$1420$2$1$ ] }, [], [ ( JobOut(28,2,1) == $Finish$1420$2$1$ ) ] ) ( { Finish[ $Finish$1420$2$1$ ] }, [], [ ( JobOut(44,1,1) == $Finish$1420$2$1$ ) ] ) ( { Finish[ $Finish$1420$2$1$ ] }, [], [ ( JobOut(28,2,1) == $Finish$1420$2$1$ ) ] ) ( { Finish[ $Finish$1420$2$1$ ] }, [], [ ( JobOut(32,3,1) == $Finish$1420$2$1$ ) ] ) ( { Finish[ $Finish$1420$2$1$ ] }, [], [ ( JobOut(44,4,1) == $Finish$1420$2$1$ ) ] ) ( { Finish[ $Finish$1420$2$1$ ] }, [], [ ( JobOut(32,3,1) == $Finish$1420$2$1$ ) ] ) ( { Finish[ $Finish$1420$2$1$ ] }, [], [ ( JobOut(28,2,1) == $Finish$1420$2$1$ ) ] ) ( { Finish[ $Finish$1420$2$1$ ] }, [], [ ( JobOut(44,5,1) == $Finish$1420$2$1$ ) ] ) ( { Finish[ $Finish$1420$2$1$ ] }, [], [ ( JobOut(32,3,1) == $Finish$1420$2$1$ ) ] ) ( { Finish[ $Finish$1420$2$1$ ] }, [], [ ( JobOut(28,2,1) == $Finish$1420$2$1$ ) ] ) ( { Finish[ $Finish$1420$2$1$ ] }, [], [ ( JobOut(44,1,1) == $Finish$1420$2$1$ ) ] ) ( { Finish[ $Finish$1420$2$1$ ] }, [], [ ( JobOut(28,2,1) == $Finish$1420$2$1$ ) ] ) ( { Finish[ $Finish$1420$2$1$ ] }, [], [ ( JobOut(32,4,1) == $Finish$1420$2$1$ ) ] ) ( { Finish[ $Finish$1420$2$1$ ] }, [], [ ( JobOut(44,3,1) == $Finish$1420$2$1$ ) ] ) ( { Finish[ $Finish$1420$2$1$ ] }, [], [ ( JobOut(28,2,1) == $Finish$1420$2$1$ ) ] ) ( { Finish[ $Finish$1420$2$1$ ] }, [], [ ( JobOut(32,4,1) == $Finish$1420$2$1$ ) ] ) ( { Finish[ $Finish$1420$2$1$ ] }, [], [ ( JobOut(44,5,1) == $Finish$1420$2$1$ ) ] ) ( { Finish[ $Finish$1420$2$1$ ] }, [], [ ( JobOut(32,4,1) == $Finish$1420$2$1$ ) ] ) ( { Finish[ $Finish$1420$2$1$ ] }, [], [ ( JobOut(28,2,1) == $Finish$1420$2$1$ ) ] ) ( { Finish[ $Finish$1420$2$1$ ] }, [], [ ( JobOut(44,1,1) == $Finish$1420$2$1$ ) ] ) ( { Finish[ $Finish$1420$2$1$ ] }, [], [ ( JobOut(28,2,1) == $Finish$1420$2$1$ ) ] ) ( { Finish[ $Finish$1420$2$1$ ] }, [], [ ( JobOut(32,5,1) == $Finish$1420$2$1$ ) ] ) ( { Finish[ $Finish$1420$2$1$ ] }, [], [ ( JobOut(44,3,1) == $Finish$1420$2$1$ ) ] ) ( { Finish[ $Finish$1420$2$1$ ] }, [], [ ( JobOut(28,2,1) == $Finish$1420$2$1$ ) ] ) ( { Finish[ $Finish$1420$2$1$ ] }, [], [ ( JobOut(32,5,1) == $Finish$1420$2$1$ ) ] ) ( { Finish[ $Finish$1420$2$1$ ] }, [], [ ( JobOut(44,4,1) == $Finish$1420$2$1$ ) ] ) ( { Finish[ $Finish$1420$2$1$ ] }, [], [ ( JobOut(28,2,1) == $Finish$1420$2$1$ ) ] ) ( { Finish[ $Finish$1420$2$1$ ] }, [], [ ( JobOut(32,5,1) == $Finish$1420$2$1$ ) ] ) ( { Finish[ $Finish$1420$2$1$ ] }, [], [ ( JobOut(44,3,1) == $Finish$1420$2$1$ ) ] ) ( { Finish[ $Finish$1420$2$1$ ] }, [], [ ( JobOut(32,2,1) == $Finish$1420$2$1$ ) ] ) ( { Finish[ $Finish$1420$2$1$ ] }, [], [ ( JobOut(28,1,1) == $Finish$1420$2$1$ ) ] ) ( { Finish[ $Finish$1420$2$1$ ] }, [], [ ( JobOut(44,4,1) == $Finish$1420$2$1$ ) ] ) ( { Finish[ $Finish$1420$2$1$ ] }, [], [ ( JobOut(32,2,1) == $Finish$1420$2$1$ ) ] ) ( { Finish[ $Finish$1420$2$1$ ] }, [], [ ( JobOut(28,1,1) == $Finish$1420$2$1$ ) ] ) ( { Finish[ $Finish$1420$2$1$ ] }, [], [ ( JobOut(44,5,1) == $Finish$1420$2$1$ ) ] ) ( { Finish[ $Finish$1420$2$1$ ] }, [], [ ( JobOut(32,2,1) == $Finish$1420$2$1$ ) ] ) ( { Finish[ $Finish$1420$2$1$ ] }, [], [ ( JobOut(28,1,1) == $Finish$1420$2$1$ ) ] ) ( { Finish[ $Finish$1420$2$1$ ] }, [], [ ( JobOut(44,2,1) == $Finish$1420$2$1$ ) ] ) ( { Finish[ $Finish$1420$2$1$ ] }, [], [ ( JobOut(28,1,1) == $Finish$1420$2$1$ ) ] ) ( { Finish[ $Finish$1420$2$1$ ] }, [], [ ( JobOut(32,3,1) == $Finish$1420$2$1$ ) ] ) ( { Finish[ $Finish$1420$2$1$ ] }, [], [ ( JobOut(44,4,1) == $Finish$1420$2$1$ ) ] ) ( { Finish[ $Finish$1420$2$1$ ] }, [], [ ( JobOut(32,3,1) == $Finish$1420$2$1$ ) ] ) ( { Finish[ $Finish$1420$2$1$ ] }, [], [ ( JobOut(28,1,1) == $Finish$1420$2$1$ ) ] ) ( { Finish[ $Finish$1420$2$1$ ] }, [], [ ( JobOut(44,5,1) == $Finish$1420$2$1$ ) ] ) ( { Finish[ $Finish$1420$2$1$ ] }, [], [ ( JobOut(32,3,1) == $Finish$1420$2$1$ ) ] ) ( { Finish[ $Finish$1420$2$1$ ] }, [], [ ( JobOut(28,1,1) == $Finish$1420$2$1$ ) ] ) ( { Finish[ $Finish$1420$2$1$ ] }, [], [ ( JobOut(44,2,1) == $Finish$1420$2$1$ ) ] ) ( { Finish[ $Finish$1420$2$1$ ] }, [], [ ( JobOut(28,1,1) == $Finish$1420$2$1$ ) ] ) ( { Finish[ $Finish$1420$2$1$ ] }, [], [ ( JobOut(32,4,1) == $Finish$1420$2$1$ ) ] ) ( { Finish[ $Finish$1420$2$1$ ] }, [], [ ( JobOut(44,3,1) == $Finish$1420$2$1$ ) ] ) ( { Finish[ $Finish$1420$2$1$ ] }, [], [ ( JobOut(28,1,1) == $Finish$1420$2$1$ ) ] ) ( { Finish[ $Finish$1420$2$1$ ] }, [], [ ( JobOut(32,4,1) == $Finish$1420$2$1$ ) ] ) ( { Finish[ $Finish$1420$2$1$ ] }, [], [ ( JobOut(44,5,1) == $Finish$1420$2$1$ ) ] ) ( { Finish[ $Finish$1420$2$1$ ] }, [], [ ( JobOut(32,4,1) == $Finish$1420$2$1$ ) ] ) ( { Finish[ $Finish$1420$2$1$ ] }, [], [ ( JobOut(28,1,1) == $Finish$1420$2$1$ ) ] ) ( { Finish[ $Finish$1420$2$1$ ] }, [], [ ( JobOut(44,2,1) == $Finish$1420$2$1$ ) ] ) ( { Finish[ $Finish$1420$2$1$ ] }, [], [ ( JobOut(28,1,1) == $Finish$1420$2$1$ ) ] ) ( { Finish[ $Finish$1420$2$1$ ] }, [], [ ( JobOut(32,5,1) == $Finish$1420$2$1$ ) ] ) ( { Finish[ $Finish$1420$2$1$ ] }, [], [ ( JobOut(44,3,1) == $Finish$1420$2$1$ ) ] ) ( { Finish[ $Finish$1420$2$1$ ] }, [], [ ( JobOut(28,1,1) == $Finish$1420$2$1$ ) ] ) ( { Finish[ $Finish$1420$2$1$ ] }, [], [ ( JobOut(32,5,1) == $Finish$1420$2$1$ ) ] ) ( { Finish[ $Finish$1420$2$1$ ] }, [], [ ( JobOut(44,4,1) == $Finish$1420$2$1$ ) ] ) ( { Finish[ $Finish$1420$2$1$ ] }, [], [ ( JobOut(28,1,1) == $Finish$1420$2$1$ ) ] ) ( { Finish[ $Finish$1420$2$1$ ] }, [], [ ( JobOut(32,5,1) == $Finish$1420$2$1$ ) ] ) ]
TXS >> FAIL: Act { { ( Finish, [ ERROR ] ) } }

Started TorXakis for the example adder with PAdder.txs model definition.
Ran following commands:

tester Adder Purp1 Sut
test 4

Got error:
Test.hs:(421,38)-(426,23): Non-exhaustive patterns in record update

Failing code:
(421,38)-(426,23):

then modify $ \env -> env
       { IOC.behtrie  = (IOC.behtrie env) ++
                        [ ( IOC.curstate env, act, (IOC.maxstate env)+1 ) ]
       , IOC.curstate = (IOC.maxstate env)+1
       , IOC.maxstate = (IOC.maxstate env)+1
       }

Error log: txs.9876.err.log.txt

TXS << param param_Sut_deltaTime 4000
TXS >> param_Sut_deltaTime = 4000
TXS << tester Model Sut
txsui: <socket: 584>: hGetLine: failed (No error)

stepper and simulator work fine. If param is not assigned, tester also works fine.
Tried with Adder and CustomersOrders examples.

Development acceptance tests should be ran with

stack test

Benchmarks should be run with stack:

stack bench

As a user I would like to experiment with Echo, and replace the String by another Type.
Currently, this results in parse errors.

When toString and fromString are used at the right places in Sim and Sut, this works immediately.

error message:
txsserver.exe: TXS TxsDefs vname: This should not happen 1 ..

Ident.vname is called with an Ident which is not an IdVar.
Probably, from TxsShow.pshow, where is written: pshow = vname,
which goes wrong for any Ident which is not an IdVar.
Why is Ident an instance of Variable?

TxsEnv contains:

data  EnvC  =  Noning   { params    :: ParamCore.Params              -- parameters
                        , unid      :: Int                           -- last used unique number
                        }
             | Initing  { smts      :: Map.Map String SMTData.SmtEnv -- named smt solver envs
                        , tdefs     :: TxsDefs.TxsDefs               -- TorXakis definitions
                        , sigs      :: Sigs.Sigs TxsDefs.VarId       -- TorXakis signatures
                        , params    :: ParamCore.Params              -- parameters
                        ...

TxsCore only works on TxsDefs.
If Sigs are needed, TxsCore is WRONG.

SMTInternal.hs - L41:

cmdCVC4 = proc "cvc4-2017-06-13-win32-opt"

We should parametrize this.

When I start
torxakisPort 2345 Echo.txs
together with a tester,

I get

TXS >>  TorXakis :: Model-Based Testing

TXS >>  txsserver starting: "LT322844.asml.com" : 2345
TXS >>  Solver initialized : Z3 [4.5.1 - build hashcode 66e61b8a31a0]
TXS >>  TxsCore initialized
TXS >>  input files parsed:
TXS >>  Echo.txs
TXS <<  simulator Model Sim
TXS >>  Simulator started
TXS <<  sim 100
txsui: <socket: 316>: hGetLine: failed (No error)

The content of .txs.2345.err.log is

TXSSERVER >>  Starting  .....

TXSSERVER CMD >>  START
TXSSERVER RSP <<  MACK txsserver starting:  "LT322844.asml.com" : 2345
TXSSERVER RSP <<  PACK START
TXSSERVER CMD >>  INIT Echo.txs
TXSSERVER RSP <<  MACK Solver initialized : Z3 [4.5.1 - build hashcode 66e61b8a31a0]
TXSSERVER RSP <<  MACK TxsCore initialized
TXSSERVER RSP <<  MACK input files parsed:
TXSSERVER RSP <<  MACK Echo.txs
TXSSERVER RSP <<  PACK INIT
TXSSERVER CMD >>  SIMULATOR Model Sim
TXSSERVER RSP <<  MACK Simulator started
TXSSERVER RSP <<  PACK SIMULATOR
TXSSERVER CMD >>  SIM 100
txsserver.exe: user error (Pattern match failure in do expression at src\Sim.hs: 111:11-37)

Note this issue would have been found when all examples are checked in the DevelopmentAcceptanceTest

Parsing Ark.txs is OK.

Z3: Can't start stepper. It continues searching for a long time. Longer than I'm willing to wait.

CVC4: Stepper starts. The first step is a ship with no rooms, no animals and positive capacity. It looks like a valid step but can't be executed.

TXS >> .....1: Act { { ( Out, [ C_AT_2581(C_AT_2582(C_T_loadType(C_AT_2580(CNil_T_roomType)),C_T_maxReproductionAgeType(C_AT_2584(CNil_T_animal_speciesType)),22)) ] ) } }
TXS >> cannot do action
TXS >> FAIL: Act { { ( Out, [ C_AT_2581(C_AT_2582(C_T_loadType(C_AT_2580(CNil_T_roomType)),C_T_maxReproductionAgeType(C_AT_2584(CNil_T_animal_speciesType)),22)) ] ) } }

Building the individual packages with stack does not work since the stack.yaml configuration is outdated. A problem seems to be that the packages section point to non-existing directories.

If the stack.yaml files are not needed I'd propose to remove this, since this will confuse stack aware IDE's like Intero or ghc-mod.

If they are needed we need to correct them, and find a workaround for IDE integration.

We don't have a license.txt file, we have a LICENSE file.

While generating a string for a step, TorXakis server reports following error:
txsserver.exe: : hPutChar: invalid argument (invalid character)

In this case, z3 provided the following solution:
(($Job$1544$7$1$ (JobData$JobData (- 421764852866273537) "ÇÇ`Ç\x00" 531 (- 1386))))

And here's what TorXakis server does with this solution:
TXSSERVER RSP << MACK .....9: Act { { ( Job, [ JobData(-421764852866273537,"txsserver.exe: : hPutChar: invalid argument (invalid character)

We expect TorXakis to be able to handle such a string.

I have a model, a sut and a test purpose in PAdder.txs:

MODELDEF  Adder ::=
    CHAN IN    Action
    CHAN OUT   Result
    BEHAVIOUR  adder [ Action, Result ] ( )
ENDDEF

PURPDEF  Purp1 ::=
        CHAN IN    Action
        CHAN OUT   Result

        GOAL m7  ::=  Action !Plus(4,7)   >->  Result ?r  >->
                      Action !Minus(4,7)  >->  Result ?r  >->  HIT
ENDDEF

CNECTDEF  Sut ::=
        CLIENTSOCK

        CHAN  OUT  Action                        HOST "localhost"  PORT 7890
        ENCODE     Action ? opn              ->  ! toString(opn)

        CHAN  IN   Result                        HOST "localhost"  PORT 7890
        DECODE     Result ! fromString(s)   <-   ? s

ENDDEF

When I try to test with TorXakis:

TXS >>  input files parsed:
TXS >>  ..\..\..\examps\adder\PAdder.txs
TXS <<  tester Adder Purp1 Sut
TXS >>  Tester started
TXS <<  test
TXS >>  No test output with test purpose
TXS >>  No Verdict
TXS <<  test 1
TXS >>  .....1: OUT: No Output (Quiescence)
TXS >>  PASS
TXS <<  test 1
txsui: <socket: 564>: hGetLine: failed (No error)

Looking at the test purpose, I expect to always have an input of Plus(4,7) as the first test step. When I input only "test" then the tool also says "No test output with test purpose".
Is this a bug? What is going here?