FilesExpand file tree

 master

/

parse_modules.py

Copy path

Blame

More file actions

Blame

More file actions

Latest commit

 

History

History

History

87 lines (77 loc) · 3.16 KB

 master

/

parse_modules.py

Copy path

Top

File metadata and controls

• Code
• Blame

87 lines (77 loc) · 3.16 KB

Raw

Copy raw file

Download raw file

Open symbols panel

Edit and raw actions

1

2

3

4

5

6

7

8

9

10

11

12

13

14

15

16

17

18

19

20

21

22

23

24

25

26

27

28

29

30

31

32

33

34

35

36

37

38

39

40

41

42

43

44

45

46

47

48

49

50

51

52

53

54

55

56

57

58

59

60

61

62

63

64

65

66

67

68

69

70

71

72

73

74

75

76

77

78

79

80

81

82

83

84

85

86

"""

Parse all modules in the manifest with SANY.

"""

from argparse import ArgumentParser

from concurrent.futures import ThreadPoolExecutor

import logging

from os import cpu_count

from os.path import join, dirname, normpath, pathsep

import subprocess

import tla_utils

parser = ArgumentParser(description='Parses all TLA+ modules in the tlaplus/examples repo using SANY.')

parser.add_argument('--tools_jar_path', help='Path to the tla2tools.jar file', required=True)

parser.add_argument('--apalache_path', help='Path to the Apalache directory', required=True)

parser.add_argument('--tlapm_lib_path', help='Path to the TLA+ proof manager module directory; .tla files should be in this directory', required=True)

parser.add_argument('--community_modules_jar_path', help='Path to the CommunityModules-deps.jar file', required=True)

parser.add_argument('--manifest_path', help='Path to the tlaplus/examples manifest.json file', required=True)

parser.add_argument('--skip', nargs='+', help='Space-separated list of .tla modules to skip parsing', required=False, default=[])

parser.add_argument('--only', nargs='+', help='If provided, only parse models in this space-separated list', required=False, default=[])

parser.add_argument('--verbose', help='Set logging output level to debug', action='store_true')

args = parser.parse_args()

logging.basicConfig(level = logging.DEBUG if args.verbose else logging.INFO)

tools_jar_path = normpath(args.tools_jar_path)

apalache_jar_path = normpath(join(args.apalache_path, 'lib', 'apalache.jar'))

tlaps_modules = normpath(args.tlapm_lib_path)

community_modules = normpath(args.community_modules_jar_path)

manifest_path = normpath(args.manifest_path)

examples_root = dirname(manifest_path)

skip_modules = args.skip

only_modules = args.only

def parse_module(path):

"""

Parse the given module using SANY.

"""

logging.info(path)

# Jar paths must go first

search_paths = pathsep.join([

tools_jar_path,

apalache_jar_path,

dirname(path),

community_modules,

tlaps_modules

])

sany = subprocess.run([

'java',

'-cp', search_paths,

'tla2sany.SANY',

'-error-codes',

path

],

stdout=subprocess.PIPE,

stderr=subprocess.STDOUT,

text=True

)

output = ' '.join(sany.args) + '\n' + sany.stdout

if 0 == sany.returncode:

logging.debug(output)

return True

else:

logging.error(output)

return False

manifest = tla_utils.load_json(manifest_path)

# List of all modules to parse and whether they should use TLAPS imports

modules = [

tla_utils.from_cwd(examples_root, module['path'])

for spec in manifest['specifications']

for module in spec['modules']

if module['path'] not in skip_modules

and (only_modules == [] or module['path'] in only_modules)

]

for path in skip_modules:

logging.info(f'Skipping {path}')

# Parse specs in parallel

thread_count = cpu_count() if not args.verbose else 1

logging.info(f'Parsing using {thread_count} threads')

with ThreadPoolExecutor(thread_count) as executor:

results = executor.map(parse_module, modules)

exit(0 if all(results) else 1)