[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]
some help needed in running tlc in distributed mode
Hello,
I am trying run TLC in distributed mode on AWS, and
- I have created a specification 'model' using Toolbox in directory 'tangled '
- I have successfully run it locally as 'Model_1'
- I have created two EC2 instances myInstance and myInstance2
I have read the instructions in https://tla.msr-inria.inria.fr/tlatoolbox/doc/model/distributed-mode.html#help, and tried the following
- copy specification && model && all related Toolbox stuff to master node myInstance:
scp tanged/ myInstance:/tmp -F ssh/config.aws
- copy tla2tool.jar to master node:
scp -F ~/java/tla/tla2tools.jar myInstance:/tmp/
on master instance:
- launch server as instructed 'distributed-mode.html#help':
cd /tmp && java -cp tla2tools.jar tlc2.tool.distrid.TLCServer tangled/model.toolbox/Model_1/MC
Observation 1:
- netstat -tulp shows that port 10997 is being listened, distributed-mode.html#help' talks about 10997
on slave instance (myInstance2)
- access master machine port 10997 successfully with telnet 172.31.15.118 10997
Observation 2:
- running wget http://172.31.15.118:10997/tla2tools.jar fails, and returns "HTTP request sent, awaiting response... No data received...Retrying"
Taking a peek at the code 'org.lamport.tla.toolbox.jcloud.CloudDistributedTLCJob'
Observation 3:
- Toolbox creates environment e.g.
mkdir /mnt/tlc/ && "
chmod 777 /mnt/tlc/ && "
ln -s /tmp/MC.out /var/www/html/MC.out
ln -s /tmp/MC.err /var/www/html/MC.err
...
Questions:
- Are the instructions in https://tla.msr-inria.inria.fr/tlatoolbox/doc/model/distributed-mode.html#help valid?
- If yes: what could be wrong with my setup?
- If no: what instructions I should follow in order to be able to run TLC using tla2tools.jar from command line?
BR,
Jukka