دو نام Node برای گره های اتصال برای منبع فعلی تعیین کنید. اولین گره در یک جفت نشان دهنده پایانه مرجع مثبت است که از آنجا جریان از طریق منبع به گره دوم می گذرد.
سه نوع شرط وجود دارد، ولتاژ کنترل شده ، جریان کنترل شده و عبارت سفارشی . برای هر نوع شرط دو شرط وجود دارد، یکی برای روشن کردن و دیگری برای خاموش کردن. شرط شرط درست است اگر عبارت On شرط بزرگتر از صفر باشد، در حالی که شرط خاموش اگر شرط خاموش کمتر از صفر باشد درست است.
لیست حالت اولیه سه گزینه دارد، استفاده در شرط ، استفاده از شرط خاموش و عبارت بولی . دو گزینه قبلی به این معنی است که سوئیچ یک حالت اولیه مطابق با شرایط روشن یا خاموش خواهد داشت. گزینه سوم باعث می شود که حالت اولیه سوئیچ با عبارت بولی سفارشی مطابقت داشته باشد. جدا کردن حالت‌های روشن، خاموش و اولیه سوئیچ را انعطاف‌پذیرتر می‌کند و می‌تواند از سوئیچ‌های سبک Schmitt-trigger و چفت‌های مختلف پشتیبانی کند.
برای کلید کنترل شده ولتاژ ، لازم است دو گره مشخص شود که ولتاژ sens.v را که وضعیت سوئیچ به آن بستگی دارد، تعیین می کند. شرایط باید به عنوان تابعی از این متغیر نوشته شود. به طور مشابه، برای سوئیچ کنترل شده Current ، لازم است یک دستگاه دو پین مشخص شود که حس فعلی را که وضعیت سوئیچ به آن بستگی دارد، تعریف کند.
هنگامی که سوئیچ در حالت روشن است دارای مقاومت غیر صفر است که توسط عبارت مقاومت روشن مشخص شده است . برای حالت خاموش هیچ جریانی از کلید عبور نمی کند (مقاومت بی نهایت). همچنین یک زمان انتقال برای روشن و خاموش شدن سوئیچ توسط عبارت Switching time تنظیم شده است . سوئیچ یک رویداد ضمنی را راه اندازی می کند که یک متغیر حالت گسسته (با پسوند _state ) را به روز می کند.
