<SYSTEM_TASK:>
Given the following text description, write Python code to implement the functionality described below step by step
<END_TASK>
<USER_TASK:>
Description:
 Formulas & Automata generators
The spot.gen package contains the functions used to generate the patterns produced by genltl and genaut.
Step1:  LTL patterns
Generation of LTL formulas is done via the ltl_pattern() function.  This takes two arguments
Step2:  To see the list of supported patterns, the easiest way is to look at the --help output of genltl.  The above pattern for instance is attached to option --ccj-beta-prime.  The name of the pattern identifier is the same using capital letters, underscores, and an LTL_ prefix.  If a pattern has multiple aliased options in genltl, the first one used for the identifier (e.g., genltl accept both --dac-patterns and --spec-patterns as synonyms to denote the patterns of spot.gen.LTL_DAC_PATTERNS).
Multiple patterns can be generated using the ltl_patterns() function.  It's arguments should be either can be
Step3:  Automata patterns
We currently have only a couple of generators of automata
Step4:  Multiple automata can be generated using the aut_patterns() function, which works similarly to ltl_patterns().
<ASSISTANT_TASK:>
Python Code:
import spot
import spot.gen as sg
spot.setup()
from IPython.display import display
Explanation: Formulas & Automata generators
The spot.gen package contains the functions used to generate the patterns produced by genltl and genaut.
End of explanation
sg.ltl_pattern(sg.LTL_AND_GF, 3)
sg.ltl_pattern(sg.LTL_CCJ_BETA_PRIME, 4)
Explanation: LTL patterns
Generation of LTL formulas is done via the ltl_pattern() function.  This takes two arguments: a pattern id, and a pattern size (or index if the id refers to a list).
End of explanation
for f in sg.ltl_patterns((sg.LTL_GH_R, 3), (sg.LTL_AND_FG, 1, 3), sg.LTL_EH_PATTERNS):
    display(f)
Explanation: To see the list of supported patterns, the easiest way is to look at the --help output of genltl.  The above pattern for instance is attached to option --ccj-beta-prime.  The name of the pattern identifier is the same using capital letters, underscores, and an LTL_ prefix.  If a pattern has multiple aliased options in genltl, the first one used for the identifier (e.g., genltl accept both --dac-patterns and --spec-patterns as synonyms to denote the patterns of spot.gen.LTL_DAC_PATTERNS).
Multiple patterns can be generated using the ltl_patterns() function.  It's arguments should be either can be:
  - pairs of the form (id, n): in this case the pattern id with size/index n is returned,
  - triplets of the form (id, min, max): in this case the patterns are output for all n between min and max included,
  - an integer id: then this is equivalent to (id, 1, 10) if the pattern has now upper bound, or (id, 1, upper) if the patter id has an upper bound upper.  This is mostly used when the pattern id correspond to a hard-coded list of formulas.
Here is an example showing these three types of arguments:
End of explanation
display(sg.aut_pattern(sg.AUT_KS_NCA, 3).show('.a'),
        sg.aut_pattern(sg.AUT_L_DSA, 3).show('.a'),
        sg.aut_pattern(sg.AUT_L_NBA, 3).show('.a'))
Explanation: Automata patterns
We currently have only a couple of generators of automata:
End of explanation
for aut in sg.aut_patterns(sg.AUT_KS_NCA):
    print(aut.num_states())
Explanation: Multiple automata can be generated using the aut_patterns() function, which works similarly to ltl_patterns().
End of explanation
<END_TASK>