class_docstr: A first order model is a domain *D* of discourse and a valuation *V*.
  
  A domain *D* is a set, and a valuation *V* is a map that associates
  expressions with values in the model.
  The domain of *V* should be a subset of *D*.
  
  Construct a new ``Model``.
  
  :type domain: set
  :param domain: A set of entities representing the domain of discourse of the model.
  :type valuation: Valuation
  :param valuation: the valuation of the model.
  :param prop: If this is set, then we are building a propositional    model and don't require the domain of *V* to be subset of *D*.
class_docstr_tok: ["A","first","order","model","is","a","domain","*","D","*","of","discourse","and","a","valuation","*","V","*",".","A","domain","*","D","*","is","a","set",",","and","a","valuation","*","V","*","is","a","map","that","associates","expressions","with","values","in","the","model",".","The","domain","of","*","V","*","should","be","a","subset","of","*","D","*",".","Construct","a","new","``","Model","``",".",":","type","domain",":","set",":","param","domain",":","A","set","of","entities","representing","the","domain","of","discourse","of","the","model",".",":","type","valuation",":","Valuation",":","param","valuation",":","the","valuation","of","the","model",".",":","param","prop",":","If","this","is","set",",","then","we","are","building","a","propositional","model","and","do","n't","require","the","domain","of","*","V","*","to","be","subset","of","*","D","*","."]
docstr: Generate the entities from the model's domain that satisfy an open formula.
  
  :param parsed: an open formula
  :type parsed: Expression
  :param varex: the relevant free individual variable in ``parsed``.
  :type varex: VariableExpression or str
  :param g: a variable assignment
  :type g:  Assignment
  :return: a set of the entities that satisfy ``parsed``.
docstr_tok: ["Generate","the","entities","from","the","model","'s","domain","that","satisfy","an","open","formula",".",":","param","parsed",":","an","open","formula",":","type","parsed",":","Expression",":","param","varex",":","the","relevant","free","individual","variable","in","``","parsed","``",".",":","type","varex",":","VariableExpression","or","str",":","param","g",":","a","variable","assignment",":","type","g",":","Assignment",":","return",":","a","set","of","the","entities","that","satisfy","``","parsed","``","."]
code: def satisfiers(self, parsed, varex, g, trace=None, nesting=0):
      """
      Generate the entities from the model's domain that satisfy an open formula.
  
      :param parsed: an open formula
      :type parsed: Expression
      :param varex: the relevant free individual variable in ``parsed``.
      :type varex: VariableExpression or str
      :param g: a variable assignment
      :type g:  Assignment
      :return: a set of the entities that satisfy ``parsed``.
      """
  
      spacer = "   "
      indent = spacer + (spacer * nesting)
      candidates = []
  
      if isinstance(varex, str):
          var = Variable(varex)
      else:
          var = varex
  
      if var in parsed.free():
          if trace:
              print()
              print(
                  (spacer * nesting)
                  + f"Open formula is '{parsed}' with assignment {g}"
              )
          for u in self.domain:
              new_g = g.copy()
              new_g.add(var.name, u)
              if trace and trace > 1:
                  lowtrace = trace - 1
              else:
                  lowtrace = 0
              value = self.satisfy(parsed, new_g, lowtrace)
  
              if trace:
                  print(indent + "(trying assignment %s)" % new_g)
  
              # parsed == False under g[u/var]?
              if value == False:
                  if trace:
                      print(
                          indent
                          + f"value of '{parsed}' under {new_g} is False"
                      )
  
              # so g[u/var] is a satisfying assignment
              else:
                  candidates.append(u)
                  if trace:
                      print(
                          indent
                          + f"value of '{parsed}' under {new_g} is {value}"
                      )
  
          result = {c for c in candidates}
      # var isn't free in parsed
      else:
          raise Undefined(f"{var.name} is not free in {parsed}")
  
      return result
  
imports: import inspect
  import re
  import sys
  import textwrap
  from pprint import pformat
  from nltk.decorators import decorator
  from nltk.sem.logic import AbstractVariableExpression, AllExpression, AndExpression, ApplicationExpression, EqualityExpression, ExistsExpression, Expression, IffExpression, ImpExpression, IndividualVariableExpression, IotaExpression, LambdaExpression, NegatedExpression, OrExpression, Variable, is_indvar
label_desc: Use image node_id 7 for calling the Model obj's underlying member method code with example usage: obj.satisfiers(parsed, varex, g, trace, nesting) and returns: result