[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